Typer Novembre 2024

typer@iro.umontreal.ca

2 participants
3 discussions

residues-elab
by Stefan Monnier 13 Nov '24

13 Nov '24

Salut Maxim, Commentaires et questions: > In elaboration, check residues only under certain conditions. > > * src/elab.ml: > In `infer_and_generalize_def`, only check for residues if the definition > contains no uninstantiated metavariables in an outer scope. Also, > restrict analysis to residues created for this particular definiton > (hence the `pre_residues` parameter). > > * src/unification.ml: > Change `check_no_residues` to run on a given list instead of all current > residues, and remove residues from the list once an error has been > logged. [ FWIW, le format que j'utilise habituellement dans Typer est celui du "GNU Coding Standard": https://www.gnu.org/prep/standards/html_node/Change-Logs.html C'était écrit à l'origine pour les fichiers ChangeLog plutot que pour les "commit message" des systèmes de contrôle de révision, donc il y a un petit peu d'ajustement à faire. ] > +let check_def_residues (e : lexp) > + (t : lexp) > + (scope_level : scope_level) > + (pre_residues : Unif.residue_list) = > + let (_, e_free_mv) = OL.fv e in > + let (_, t_free_mv) = OL.fv t in > + let (free_mv_map, _) = OL.mv_set_union e_free_mv t_free_mv in > + (* Only check residues if no metavariables appear outside of this > + * definition's scope level. *) > + if IMap.for_all > + (fun _ (mv_scope_level, _, _, _) -> > + mv_scope_level >= scope_level) > + free_mv_map > + then > + let this_def_residues = Unif.filter_residues pre_residues in > + Unif.raise_errors_on_residues (location e) this_def_residues Hmm... ça correspond pas tout à fait à l'idée que j'avais. Je pensais plutôt qcch comme: for all (_, e1, e2) in !current_residues do let (_, e1_free_mv) = OL.fv e1 in let (_, e2_free_mv) = OL.fv e2 in (* Check if the reside includes vars which can still be instantiated *) if IMap.for_all (fun _ (mv_scope_level, _, _, _) -> mv_scope_level > scope_level) free_mv_map then Unif.raise_errors_on_residues ... else ; (* All good: there's still hope to resolve this later. *) Et ma question est: si je comprends bien tu as testé que le code passe, maintenant, mais je ne vois plus de test que `current_residues` est vide "eventually". Est-on sûr qu'on ne va pas des fois accepter du code alors qu'il reste des résidus insatisfaits? Stefan

1 0

[Git][monnier/typer][main] 2 commits: Miscellanious bug fixes and code cleanups.
by Stefan (＠monnier) 12 Nov '24

12 Nov '24

Stefan pushed to branch main at Stefan / Typer Commits: 9c6d2169 by Maxim Bernard at 2024-10-31T15:26:08-04:00 Miscellanious bug fixes and code cleanups. * typer.ml: Flush standard output when loading file (otherwise line is not printed at the right time) and update copyright years. * typer.sh: Fix with right executable path. * src/fmt.ml: Flush standand output after printing lexp. * src/sexp.ml: Remove obsolete `location` function, since it's now in src/ir.ml. * src/unification.ml: Add rule in unification of sort levels for unifying lub with level zero. In default case of unifying two sort levels, return a residue instead of an impossible constraint. * src/lexp.ml: In `subst_eq`, support comparing identity substitution with `Cons`. * All files: Replace `Sexp.location` with `sexp_location` following changes in sexp.ml. - - - - - 5bf23466 by Stefan Monnier at 2024-11-12T15:17:46-05:00 Merge remote-tracking branch 'gitlab/misc-fixes' - - - - - 15 changed files: - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/elexp.ml - src/eval.ml - src/fmt.ml - src/instargs.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml - src/sexp.ml - src/unification.ml - typer.ml - typer.sh Changes: ===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2021 Free Software Foundation, Inc. + * Copyright (C) 2016-2024 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -149,7 +149,6 @@ let register_builtin_csts () = OL.add_builtin_cst "Type0" 0 DB.type0; OL.add_builtin_cst "Type1" 0 DB.type1; OL.add_builtin_cst "Integer" 0 DB.type_integer; - OL.add_builtin_cst "Int" 0 DB.type_int; OL.add_builtin_cst "Float" 0 DB.type_float; OL.add_builtin_cst "String" 0 DB.type_string; OL.add_builtin_cst "Eq" 0 DB.type_eq; ===================================== src/debruijn.ml ===================================== @@ -441,7 +441,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc:(Sexp.location loc) ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name @@ -451,7 +451,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = with | Not_found -> fatal - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2023 Free Software Foundation, Inc. + * Copyright (C) 2011-2024 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -149,14 +149,14 @@ let log_proper_type_error var t s = match var with | (l, None) -> lexp_error - (Sexp.location l) + (sexp_location l) t "@[<v>Expression:@, @[<hov 2>%a@]@,of type :@, @[<hov 2>%a@]@,is not a proper type.@]" pp_print_clean_lexp t pp_print_clean_lexp s | (l, Some name) -> lexp_error - (Sexp.location l) + (sexp_location l) t "@[<v>Expression %s:@, @[<hov 2>%a@]@,of type :@, @[<hov 2>%a@]@,is not a proper type.@]" name @@ -208,7 +208,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = print_lexp_ctx (ectx_to_lctx ctx); print_newline () ) - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "Error while type-checking"; raise e in if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' @@ -216,7 +216,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = | e -> info ~print_action:(lexp_print_details lxp) - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) "@[<v>Exception while conversion-checking types:@, @[<hov 2>%a@]@,and:@, @[<hov 2>%a@]@]" pp_print_clean_lexp ltype pp_print_clean_lexp ltype'; @@ -225,7 +225,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype var else fatal - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) ("@[<v>Type check error (ctx_define error):" ^^ "@, @[<hov 2>%s = %a@]" ^^ "@,is not of type:" @@ -358,13 +358,13 @@ let sdform_define_operator (ctx : elab_context) loc sargs : elab_context = -> let level s = match s with | Symbol (_, "") -> None | Integer (_, n) -> Some (Z.to_int n) - | _ -> sexp_error (Sexp.location s) "Expecting an integer or ()"; None in + | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in let grm = ectx_get_grammar ctx in ectx_set_grammar (Grammar.add name (level l, level r) grm) ctx | [o; _; _] - -> sexp_error (Sexp.location o) "Expecting a string"; ctx + -> sexp_error (sexp_location o) "Expecting a string"; ctx | _ - -> sexp_error (Sexp.location loc) "define-operator expects 3 argument"; ctx + -> sexp_error (sexp_location loc) "define-operator expects 3 argument"; ctx let sform_dummy_ret ctx loc = let t = newMetatype (ectx_to_lctx ctx) dummy_scope_level loc in @@ -384,7 +384,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error (Sexp.location loc) {|The variable "%s" was not declared%s|} name relateds; + sexp_error (sexp_location loc) {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc) (* Turn metavar into plain vars after generalization. @@ -635,10 +635,10 @@ let rec sform_immediate ctx loc sargs ot = let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot | [_se] - -> sexp_error (Sexp.location loc) "Non-immediate passed to ##typer-immediate"; + -> sexp_error (sexp_location loc) "Non-immediate passed to ##typer-immediate"; sform_dummy_ret ctx loc | _ - -> sexp_error (Sexp.location loc) "Too many args to ##typer-immediate"; + -> sexp_error (sexp_location loc) "Too many args to ##typer-immediate"; sform_dummy_ret ctx loc @@ -680,7 +680,7 @@ and sform_identifier ctx loc sargs ot = (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for the metavar! *) - fatal ~loc:(Sexp.location loc) ("Bug in the elaboration of a metavar" + fatal ~loc:(sexp_location loc) ("Bug in the elaboration of a metavar" ^^ " repeated at a different scope level!") else let t = match ot with @@ -693,7 +693,7 @@ and sform_identifier ctx loc sargs ot = let idx = match lexp_lexp' mv with | Metavar (idx, _, _) -> idx - | _ -> fatal ~loc:(Sexp.location loc) "newMetavar returned a non-Metavar" in + | _ -> fatal ~loc:(sexp_location loc) "newMetavar returned a non-Metavar" in rmmap := SMap.add name (idx, sl) (!rmmap)); (mv, match ot with Some _ -> Checked | None -> Lazy) @@ -702,11 +702,11 @@ and sform_identifier ctx loc sargs ot = -> elab_varref ctx (loc, name) | [_se] - -> sexp_error (Sexp.location loc) "Non-symbol passed to ##typer-identifier"; + -> sexp_error (sexp_location loc) "Non-symbol passed to ##typer-identifier"; sform_dummy_ret ctx loc | _ - -> sexp_error (Sexp.location loc) "Too many args to ##typer-identifier"; + -> sexp_error (sexp_location loc) "Too many args to ##typer-identifier"; sform_dummy_ret ctx loc and elab_via head default ctx se ot = @@ -730,7 +730,7 @@ and elaborate ctx se ot = (* Rewrite IMM to `typer-immediate IMM`. *) | (Integer _ | Float _ | String _ | Block _) - -> let l = Sexp.location se in + -> let l = sexp_location se in elaborate ctx (Node (l, Symbol (l, "typer-immediate"), [se])) ot | Node (_, se, []) -> elaborate ctx se ot @@ -765,7 +765,7 @@ and elaborate ctx se ot = and infer (p : sexp) (ctx : elab_context): lexp * ltype = match elaborate ctx p None with - | (_, Checked) -> fatal ~loc:(Sexp.location p) "`infer` got Checked!" + | (_, Checked) -> fatal ~loc:(sexp_location p) "`infer` got Checked!" | (e, Lazy) -> (e, OL.get_type (ectx_to_lctx ctx) e) | (e, Inferred t) -> (e, t) @@ -778,7 +778,7 @@ and elab_special_form ctx f args ot = | _ -> lexp_error - (Sexp.location loc) + (sexp_location loc) f "@[<v>Unknown special-form:@, @[<hov 2>%a@]@]" pp_print_clean_lexp f; @@ -791,7 +791,7 @@ and elab_special_decl_form ctx f args = (* Special form. *) (get_special_decl_form name) ctx loc args | _ -> lexp_error - (Sexp.location loc) + (sexp_location loc) f "@[<v>Unknown special-decl-form:@, @[<hov 2>%a@]@]" pp_print_clean_lexp f; @@ -873,7 +873,7 @@ and unify_with_arrow ctx tloc lxp kind var aty match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error - (Sexp.location tloc) + (sexp_location tloc) lxp "@[<v>Type mismatch between:@, @[<hov 2>%a@]@,and:@, @[<hov 2>%a@]@]" pp_print_lexp t1 @@ -953,7 +953,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match Unif.unify actual expected (ectx_to_lctx ctx) with | (_::_) -> lexp_error - (Sexp.location loc) + (sexp_location loc) lctor "@[<v>Expected pattern of type:@, @[<hov 2>%a@]@,but got:@, @[<hov 2>%a@]@]" pp_print_clean_lexp expected @@ -991,7 +991,7 @@ and check_case rtype (loc, target, ppatterns) ctx = constructors | _ -> lexp_error - (Sexp.location target) + (sexp_location target) tlxp "@[<v>Can't \"case\" on objects of type@, @[<hov 2>%a@]@]" pp_print_clean_lexp tltp; @@ -1030,7 +1030,7 @@ and check_case rtype (loc, target, ppatterns) ctx = lbranches, Some (v, lexp) in let add_branch pctor pargs = - let loc = Sexp.location pctor in + let loc = sexp_location pctor in let lctor, _ct = infer pctor ctx in let rec inst_args ctx e = let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in @@ -1129,7 +1129,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) -> if Eval.constructor_p name ctx then - add_branch (Symbol (Sexp.location l, name)) [] + add_branch (Symbol (sexp_location l, name)) [] else add_default var (* A named default branch. *) | Ppatcons (_, pctor, pargs) -> add_branch pctor pargs in @@ -1156,17 +1156,17 @@ and elab_macro_call if !macro_tracing_enabled then (trace_macro - ~location:(Sexp.location location) + ~location:(sexp_location location) "@[<v>Expanding:@, @[<hov 2>%a@]@]" pp_print_clean_lexp func; List.iteri (fun i arg -> - arg |> string_of_sexp |> trace_macro ~location:(Sexp.location location) {|input %d: %s|} i) + arg |> string_of_sexp |> trace_macro ~location:(sexp_location location) {|input %d: %s|} i) args); let sxp = lexp_expand_macro location func args ctx (Some t) in if !macro_tracing_enabled - then trace_macro ~location:(Sexp.location location) "@[<v>Output:@,@[<hov>%s@]@]" (string_of_sexp sxp); + then trace_macro ~location:(sexp_location location) "@[<v>Output:@,@[<hov>%s@]@]" (string_of_sexp sxp); elaborate ctx sxp ot @@ -1220,7 +1220,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in let loc = match pending with - | (_, sarg)::_ -> Sexp.location sarg + | (_, sarg)::_ -> sexp_location sarg | _ -> assert false in lexp_error loc func {|Explicit actual args "%s" have no matching formal args.|} @@ -1338,15 +1338,15 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) let args = [macro; BI.o2v_list sargs] in (* FIXME: Make a proper `Var`. *) - let value = EV.eval_call (Sexp.location loc) (Evar ((dsinfo, Some "expand_macro"), 0)) + let value = EV.eval_call (sexp_location loc) (Evar ((dsinfo, Some "expand_macro"), 0)) ([], []) macro_expand args in match value with | Vcommand cmd -> (match cmd () with | Vsexp sxp -> sxp - | v -> value_fatal (Sexp.location loc) v "@[<v>Macro should return an IO sexp:@, @[<hov 2>%a@]@]" + | v -> value_fatal (sexp_location loc) v "@[<v>Macro should return an IO sexp:@, @[<hov 2>%a@]@]" pp_print_clean_lexp macro_funct) - | v -> value_fatal (Sexp.location loc) v "@[<v>Macro should return an IO:@, @[<hov 2>%a@]@]" + | v -> value_fatal (sexp_location loc) v "@[<v>Macro should return an IO:@, @[<hov 2>%a@]@]" pp_print_clean_lexp macro_funct @@ -1555,7 +1555,7 @@ and lexp_decls_1 head, [Symbol s; Node (location, - Symbol (Sexp.location d, "lambda_->_"), + Symbol (sexp_location d, "lambda_->_"), [sexp_u_list args location; body])])] nctx pending_decls pending_defs @@ -1579,7 +1579,7 @@ and lexp_decls_1 let sdecl' = lexp_expand_macro sxp lxp sargs nctx None in recur [sdecl'] nctx pending_decls pending_defs else ( - error ~loc:(Sexp.location sxp) "Invalid declaration syntax"; + error ~loc:(sexp_location sxp) "Invalid declaration syntax"; recur [] nctx pending_decls pending_defs ) @@ -1623,9 +1623,9 @@ and sform_declexpr ctx loc sargs _ot = | [e] when is_var e -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with | Some lxp -> (lxp, Lazy) - | None -> error ~loc:(Sexp.location loc) "no expr available"; + | None -> error ~loc:(sexp_location loc) "no expr available"; sform_dummy_ret ctx loc) - | _ -> error ~loc:(Sexp.location loc) "declexpr expects one argument"; + | _ -> error ~loc:(sexp_location loc) "declexpr expects one argument"; sform_dummy_ret ctx loc @@ -1633,7 +1633,7 @@ let sform_decltype ctx loc sargs _ot = match List.map (lexp_parse_sexp ctx) sargs with | [e] when is_var e -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) - | _ -> error ~loc:(Sexp.location loc) "decltype expects one argument"; + | _ -> error ~loc:(sexp_location loc) "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1648,21 +1648,21 @@ let sform_built_in ctx loc sargs ot = (* FIXME: This `L.clean` is one of the last remaining uses of the * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper - * memoization of push_susp and/or whnf). *) + * memoization of push_susp and/or whnf). *) -> let ltp' = Lexp.clean ltp in - let bi = mkBuiltin ((Sexp.location loc, name), ltp') in + let bi = mkBuiltin ((sexp_location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions) || List.mem name DB.builtin_axioms) then - sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; + sexp_error (sexp_location loc) {|Unknown built-in "%s"|} name; OL.add_builtin_cst name (DB.get_size ctx) bi; (bi, Checked) - | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; + | None -> error ~loc:(sexp_location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) - | true, _ -> error ~loc:(Sexp.location loc) "Wrong Usage of `Built-in`"; + | true, _ -> error ~loc:(sexp_location loc) "Wrong Usage of `Built-in`"; sform_dummy_ret ctx loc - | false, _ -> error ~loc:(Sexp.location loc) "Use of `Built-in` in user code"; + | false, _ -> error ~loc:(sexp_location loc) "Use of `Built-in` in user code"; sform_dummy_ret ctx loc let sform_datacons ctx loc sargs _ot = @@ -1671,9 +1671,9 @@ let sform_datacons ctx loc sargs _ot = -> let idt, _ = infer t ctx in (mkCons (idt, sym), Lazy) - | [_;_] -> sexp_error (Sexp.location loc) "Second arg of ##constr should be a symbol"; + | [_;_] -> sexp_error (sexp_location loc) "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc - | _ -> sexp_error (Sexp.location loc) "##constr requires two arguments"; + | _ -> sexp_error (sexp_location loc) "##constr requires two arguments"; sform_dummy_ret ctx loc let elab_colon_to_ak k = match k with @@ -1693,20 +1693,20 @@ let elab_typecons_arg arg : (arg_kind * vname * sexp option) = (arg, Some name), Some e) | Symbol (_l, name) -> (Anormal, (arg, Some name), None) | _ -> sexp_error ~print_action:(fun _ -> print_sexp arg; print_newline ()) - (Sexp.location arg) + (sexp_location arg) "Unrecognized formal arg"; (Anormal, (arg, None), None) let sform_typecons ctx loc sargs _ot = match sargs with - | [] -> sexp_error (Sexp.location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) + | [] -> sexp_error (sexp_location loc) "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (_, label, formals) -> (label, formals) | _ -> (formals, []) in let label = match label with | Symbol label -> label - | _ -> let loc = Sexp.location label in + | _ -> let loc = sexp_location label in sexp_error loc "Unrecognized inductive type name"; (loc, "<error>") in @@ -1735,7 +1735,7 @@ let sform_typecons ctx loc sargs _ot = (* This is a constructor with no args *) | Symbol s -> (s, [])::pcases - | _ -> sexp_error (Sexp.location case) + | _ -> sexp_error (sexp_location case) "Unrecognized constructor declaration"; pcases) constrs [] in @@ -1748,7 +1748,7 @@ let sform_hastype ctx loc sargs _ot = | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) - | _ -> sexp_error (Sexp.location loc) "##_:_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_:_ takes two arguments"; sform_dummy_ret ctx loc let sform_arrow kind ctx loc sargs _ot = @@ -1761,7 +1761,7 @@ let sform_arrow kind ctx loc sargs _ot = let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (st2, None) in (mkArrow (loc, kind, v, lt1, lt2), Lazy) - | _ -> sexp_error (Sexp.location loc) "##_->_ takes two arguments"; + | _ -> sexp_error (sexp_location loc) "##_->_ takes two arguments"; sform_dummy_ret ctx loc let rec sform_lambda kind ctx loc sargs ot = @@ -1770,7 +1770,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> let (arg, ost1) = match sarg with | Node (_, Symbol (_, "_:_"), [Symbol arg; st]) -> (elab_p_id arg, Some st) | Symbol arg -> (elab_p_id arg, None) - | _ -> sexp_error (Sexp.location sarg) + | _ -> sexp_error (sexp_location sarg) "Unrecognized lambda argument"; ((dsinfo, None), None) in @@ -1833,7 +1833,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> sexp_error - (Sexp.location loc) "##lambda_%s_ takes two arguments" + (sexp_location loc) "##lambda_%s_ takes two arguments" (match kind with | Anormal -> "->" | Aimplicit -> "=>" @@ -1845,7 +1845,7 @@ let rec sform_case ctx sinfo sargs ot = match sargs with -> let parse_case branch = match branch with | Node (_, Symbol (_, "_=>_"), [pat; code]) -> (pexp_p_pat pat, code) - | _ -> let l = (Sexp.location branch) in + | _ -> let l = (sexp_location branch) in sexp_error l "Unrecognized simple case branch"; (Ppatsym (se, None), Symbol (l, "?")) in let pcases = List.map parse_case scases in @@ -1857,10 +1857,10 @@ let rec sform_case ctx sinfo sargs ot = match sargs with (* In case there are no branches, pretend there was a | anyway. *) | [_e] - -> let loc = Sexp.location sinfo in + -> let loc = sexp_location sinfo in sform_case ctx sinfo [Node (loc, Symbol (loc, "_|_"), sargs)] ot | _ - -> sexp_error (Sexp.location sinfo) "Unrecognized case expression"; + -> sexp_error (sexp_location sinfo) "Unrecognized case expression"; sform_dummy_ret ctx sinfo let sform_letin ctx loc sargs ot = match sargs with @@ -1876,7 +1876,7 @@ let sform_letin ctx loc sargs ot = match sargs with | Inferred t -> Inferred (mkSusp t s) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) - | _ -> sexp_error (Sexp.location loc) "Unrecognized let_in_ expression"; + | _ -> sexp_error (sexp_location loc) "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc let sform_proj ctx loc sargs _ = @@ -1886,9 +1886,9 @@ let sform_proj ctx loc sargs _ = let e = mkProj (loc,ret,(loca,str)) in (e, Lazy) | [_;_] - -> sexp_error (Sexp.location loc) "Second argument is not a Symbol!"; + -> sexp_error (sexp_location loc) "Second argument is not a Symbol!"; sform_dummy_ret ctx loc - | _ -> sexp_error (Sexp.location loc) "Wrong arg number!"; + | _ -> sexp_error (sexp_location loc) "Wrong arg number!"; sform_dummy_ret ctx loc let rec infer_level ctx se : lexp = @@ -1899,7 +1899,7 @@ let rec infer_level ctx se : lexp = -> mkSortLevel (SLsucc (infer_level ctx se)) | Node (_, Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) - | _ -> let l = (Sexp.location se) in + | _ -> let l = (sexp_location se) in (sexp_error l "Unrecognized TypeLevel: %s" (string_of_sexp se); newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) se) @@ -1914,7 +1914,7 @@ let sform_type ctx loc sargs _ot = | [se] -> let l = infer_level ctx se in (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) - | _ -> (sexp_error (Sexp.location loc) "##Type_ expects one argument"; + | _ -> (sexp_error (sexp_location loc) "##Type_ expects one argument"; sform_dummy_ret ctx loc) let sform_debruijn ctx loc sargs _ot = @@ -1925,7 +1925,7 @@ let sform_debruijn ctx loc sargs _ot = sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy) - | _ -> (sexp_error (Sexp.location loc) "##DeBruijn expects one integer argument"; + | _ -> (sexp_error (sexp_location loc) "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc) (* Only print var info *) @@ -1961,7 +1961,7 @@ let sform_load usr_elctx loc sargs _ot = let pres = try prelex source with | Sys_error _ - -> error ~loc:(Sexp.location loc) {|Could not load "%s": file not found.|} file_name; [] + -> error ~loc:(sexp_location loc) {|Could not load "%s": file not found.|} file_name; [] in let sxps = lex default_stt pres in let _, elctx = lexp_p_decls [] sxps elctx @@ -1973,7 +1973,7 @@ let sform_load usr_elctx loc sargs _ot = read_file file_name usr_elctx else read_file file_name !sform_default_ectx - | _ -> (error ~loc:(Sexp.location loc) "argument to load should be one file name (String)"; + | _ -> (error ~loc:(sexp_location loc) "argument to load should be one file name (String)"; !sform_default_ectx) in (* get lexp_context *) ===================================== src/elexp.ml ===================================== @@ -36,11 +36,11 @@ module SMap = Util.SMap let rec location : elexp -> Source.Location.t = function | Eimm (l, _) -> l - | Evar ((l, _), _) -> Sexp.location l + | Evar ((l, _), _) -> sexp_location l | Eproj (l, _, _) -> l | Ebuiltin ((l, _)) -> l | Elet (l, _, _) -> l - | Elambda ((l, _), _) -> Sexp.location l + | Elambda ((l, _), _) -> sexp_location l | Ecall (f, _) -> location f | Econs (_, (l, _)) -> l | Ecase (l, _, _, _) -> l ===================================== src/eval.ml ===================================== @@ -488,7 +488,7 @@ and eval_var ctx lxp v = try get_rte_variable vname idx ctx with | _e -> Log.log_fatal - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "Variable: %s[%d] was not found\n%s" (maybename name) idx (trace_elexp lxp) ===================================== src/fmt.ml ===================================== @@ -537,7 +537,8 @@ and pp_print_lexp_decls (f : Format.formatter) (ldecls : ldecls list) : unit = ldecls and print_lexp (l : lexp) : unit = - Format.printf "%a" pp_print_lexp l + Format.printf "%a" pp_print_lexp l; + Format.print_flush () and string_of_lexp (l : lexp) : string = Format.asprintf "%a" pp_print_lexp l ===================================== src/instargs.ml ===================================== @@ -119,7 +119,7 @@ let search_instance : lexp option = Log.log_debug - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "@[<v>Resolving type:@, @[<hov 2>%a@]@]" L.pp_print_clean_lexp t; let lctx = DB.ectx_to_lctx ctx in @@ -141,7 +141,7 @@ let search_instance let var = L.mkVar ((sinfo, namopt), i) in let t' = L.mkSusp t' (S.shift (i + 1)) in let (e, t') = instantiate_implicit var t' ctx in - Log.log_debug ~loc:(Sexp.location sinfo) + Log.log_debug ~loc:(sexp_location sinfo) ("@[<v>Considering potential instance:" ^^ "@, @[<hov 2>%a@]" ^^ "@,of type:" @@ -164,7 +164,7 @@ let search_instance | Possible -> (match !log_skipped_uncertain_matches with | Some level -> - Log.log_msg ignore level ~loc:(Sexp.location sinfo) + Log.log_msg ignore level ~loc:(sexp_location sinfo) ("@[<v>Skipping potential instance:" ^^ "@, @[<hov 2>%a@]" ^^ "@,of type:@, @[<hov 2>%a@]" @@ -200,7 +200,7 @@ let search_instance | None -> None | Some (i, (vname, _, t'), e) -> let t' = L.mkSusp t' (S.shift (i + 1)) in - Log.log_debug ~loc:(Sexp.location sinfo) + Log.log_debug ~loc:(sexp_location sinfo) ("@[<v>Found instance for:" ^^ "@, @[<hov 2>%a@]" ^^ "@,at index %i:" @@ -236,7 +236,7 @@ let resolve_instances instantiate_implicit e = and cause an error. *) | None -> Log.log_info - ~loc:(Sexp.location sinfo) + ~loc:(sexp_location sinfo) "@[<v>No instance found for type:@, @[<hov 2>%a@]@]" L.pp_print_clean_lexp t; false) ===================================== src/lexer.ml ===================================== @@ -150,9 +150,9 @@ let lex_symbol in let location s = s - |> Sexp.location + |> sexp_location |> Source.Location.extend op_location - |> Source.Location.extend (Sexp.location left) + |> Source.Location.extend (sexp_location left) in let lf' = if prec' > prec ===================================== src/lexp.ml ===================================== @@ -426,13 +426,13 @@ let rec lexp_sinfo s = | Proj (l,_,_) -> l let location (e : lexp) : Source.Location.t = - Sexp.location (lexp_sinfo e) + sexp_location (lexp_sinfo e) (********* Normalizing a term *********) let vdummy = (dummy_sinfo, None) let sname (sinfo, n : vname) : symbol = - (Sexp.location sinfo, U.maybename n) + (sexp_location sinfo, U.maybename n) let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with @@ -636,6 +636,12 @@ and subst_eq s1 s2 = let o = o2 - o1 in eq e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) + | ((S.Identity n, S.Cons (e, s, o)) + | (S.Cons (e, s, o), S.Identity n)) + -> (* ↑n ≃ Var n · ↑(n+1), so unfold Identity when needed. *) + match lexp_lexp' e with + | Var (_, n') when n' == n + o + -> subst_eq (S.Identity (n + 1)) (S.mkShift s o) | _ -> false (* Print a clean version of an lexp. Should be preferred to `pp_print_lexp` ===================================== src/opslexp.ml ===================================== @@ -229,7 +229,7 @@ let rec lexp_whnf e (ctx : lexp_context) : lexp = -> let subst = S.cons (mk_eq_witness l e' ctx) (S.substitute e') in lexp_whnf (push_susp default subst) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:(Sexp.location l) + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with @@ -255,17 +255,17 @@ let rec lexp_whnf e (ctx : lexp_context) : lexp = _ -> []) in let rec getfield label args fields = match args, fields with - | _ , [] -> Log.log_error ~loc:(Sexp.location loc) + | _ , [] -> Log.log_error ~loc:(sexp_location loc) "Tuple does not have the field `%s`" label; e | (_, arg)::_, (_, (_, Some fn), _)::_ when fn = label -> (* Reduce to the argument corresponding to the field *) lexp_whnf arg ctx | _::args, _::fields -> getfield label args fields | [], _ -> (* This case should be impossible through typing *) - Log.log_fatal ~loc:(Sexp.location loc) + Log.log_fatal ~loc:(sexp_location loc) "Projected tuple has fewer arguments than fields" in getfield label (drop (List.length targs) args) fields - | _ -> Log.log_error ~loc:(Sexp.location loc) "Proj on a non-tuple in WHNF!"; e) + | _ -> Log.log_error ~loc:(sexp_location loc) "Proj on a non-tuple in WHNF!"; e) | _ -> e) (* Not a proj of a cons: don't reduce. *) | Metavar (idx, s, _) @@ -710,7 +710,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc:(Sexp.location loc) + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (U.maybename name) ; lookup_type ctx v @@ -743,7 +743,7 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc:(Sexp.location loc) "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(Lexp.location t1) "Not a proper type"; @@ -850,20 +850,20 @@ and check'' erased ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(Sexp.location l) + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" label; + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(Sexp.location l) "Can't Proj an erasable field: %s" + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -875,10 +875,10 @@ and check'' erased ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(Sexp.location l) + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; etype) + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) @@ -905,7 +905,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:(Sexp.location l) "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = @@ -936,10 +936,10 @@ and check'' erased ctx e = (mkCall (l, mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) vdefs fieldtypes | _ - -> log_tc_error ~loc:(Sexp.location l) "Wrong number of args to constructor!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (l, mkCons (it, (Sexp.location l, name)), + mkCall (l, mkCons (it, (sexp_location l, name)), List.map (fun (_, a) -> (Aerasable, a)) aargs) in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in @@ -953,7 +953,7 @@ and check'' erased ctx e = (match default with | Some (v, d) -> if diff <= 0 - then log_tc_warning ~loc:(Sexp.location l) "Redundant default clause"; + then log_tc_warning ~loc:(sexp_location l) "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = DB.set_sink 1 erased in let subst = S.shift 1 in @@ -966,8 +966,8 @@ and check'' erased ctx e = -> if diff > 0 then log_tc_error - ~loc:(Sexp.location l) "Non-exhaustive match: %d cases missing" diff) - | _,_ -> log_tc_error ~loc:(Sexp.location l) "Case on a non-inductive type!"); + ~loc:(sexp_location l) "Non-exhaustive match: %d cases missing" diff) + | _,_ -> log_tc_error ~loc:(sexp_location l) "Case on a non-inductive type!"); ret | Cons (t, (_l, name)) -> (match lexp'_whnf t ctx with @@ -996,7 +996,7 @@ and check'' erased ctx e = buildtype fargs with | Not_found - -> log_tc_error ~loc:(Sexp.location l) {|Constructor "%s" does not exist|} name; + -> log_tc_error ~loc:(sexp_location l) {|Constructor "%s" does not exist|} name; type_dummy) | _ -> log_tc_error ~loc:(Lexp.location e) @@ -1166,21 +1166,21 @@ and get_type ctx e = | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs -> mksubst (S.cons aarg s) fargs aargs - | _,_ -> (log_tc_error ~loc:(Sexp.location l) + | _,_ -> (log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with - | [] -> log_tc_error ~loc:(Sexp.location l) "Tuple has no field named: %s" + | [] -> log_tc_error ~loc:(sexp_location l) "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:(Sexp.location l) + else (log_tc_error ~loc:(sexp_location l) "Can't Proj an erasable field: %s" label; Lexp.impossible) | (_, vdef, _)::fieldtypes @@ -1192,10 +1192,10 @@ and get_type ctx e = getfieldtype (S.cons fieldref s) fieldtypes in getfieldtype s fieldtypes | Inductive _, _ - -> Log.log_error ~loc:(Sexp.location l) + -> Log.log_error ~loc:(sexp_location l) "Proj on an inductive type that's not a tuple!"; etype - | _,_ -> Log.log_error ~loc:(Sexp.location l) "Proj on a non-inductive type!" ; + | _,_ -> Log.log_error ~loc:(sexp_location l) "Proj on a non-inductive type!" ; etype) | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) @@ -1371,12 +1371,12 @@ let pos_of_label lctx label e : int = let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = match lexp_lexp' lxp with - | Imm (l, s) -> Eimm (Sexp.location l, s) + | Imm (l, s) -> Eimm (sexp_location l, s) | Builtin (v, _) -> Ebuiltin (v) | Var (v) -> Evar (v) | Proj (l, exp, label) -> let t = get_type lctx exp in - Eproj (Sexp.location l, erase_type lctx exp, pos_of_label lctx label t) + Eproj (sexp_location l, erase_type lctx exp, pos_of_label lctx label t) | Cons (ty, s) -> Econs (arity_of_cons lctx ty s, s) | Lambda (Aerasable, _, _, body) @@ -1388,7 +1388,7 @@ let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = | Let (l, decls, body) -> let lctx', edecls = clean_decls lctx decls in - Elet (Sexp.location l, edecls, erase_type lctx' body) + Elet (sexp_location l, edecls, erase_type lctx' body) | Call (_, fct, args) -> Ecall (erase_type lctx fct, List.filter_map (clean_arg lctx) args) @@ -1396,7 +1396,7 @@ let rec erase_type (lctx : lexp_context) (lxp: lexp) : elexp = | Case (location, target, _, branches, default) -> let etarget = erase_type lctx target in let ebranches = clean_branch_map lctx branches in - Ecase (Sexp.location location, etarget, ebranches, clean_default lctx default) + Ecase (sexp_location location, etarget, ebranches, clean_default lctx default) | Susp (l, s) -> erase_type lctx (L.push_susp l s) @@ -1445,7 +1445,7 @@ and clean_branch_map lctx cases = in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (Sexp.location l, eargs, erase_type lctx' (L.push_susp expr subst)) + (sexp_location l, eargs, erase_type lctx' (L.push_susp expr subst)) in SMap.map clean_branch cases @@ -1461,7 +1461,7 @@ let erase_type lctx lxp = IMap.iter (fun i (_, t, _, (l, n)) -> Format.printf "%s ?%s[%i] : @[<hov 2>%a@]@," - (Source.Location.to_string (Sexp.location l)) + (Source.Location.to_string (sexp_location l)) (Option.value ~default:"" n) i pp_print_clean_lexp t) @@ -1497,8 +1497,8 @@ let ctx2tup ctx nctx = match blocs with | [] -> let cons_name = "cons" in - let cons_label = (Sexp.location loc, cons_name) in - let type_label = (Sexp.location loc, "record") in + let cons_label = (sexp_location loc, cons_name) in + let type_label = (sexp_location loc, "record") in let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) ===================================== src/pexp.ml ===================================== @@ -36,7 +36,7 @@ type ppat = | Ppatcons of Source.Location.t * sexp * (symbol option * vname) list let pexp_pat_location : ppat -> Source.Location.t = function - | Ppatsym (l, _) -> Sexp.location l + | Ppatsym (l, _) -> sexp_location l | Ppatcons (l, _, _) -> l let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = @@ -49,7 +49,7 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) = | Anormal -> ":") in let ty = match t with Some e -> e | None -> Symbol (l, "_") in - let location = Source.Location.extend l (Sexp.location ty) in + let location = Source.Location.extend l (sexp_location ty) in Node (location, head, [Symbol s; ty]) let pexp_p_pat_arg (s : sexp) = match s with @@ -57,12 +57,12 @@ let pexp_p_pat_arg (s : sexp) = match s with | Node (_, Symbol (_, "_:=_"), [Symbol f; Symbol (_l,n)]) -> (Some f, (s, Some n)) | _ - -> let loc = Sexp.location s in + -> let loc = sexp_location s in pexp_error loc "Unknown pattern arg"; (None, (s, None)) let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp = - let pname = Symbol (Sexp.location l, match oname with None -> "_" | Some n -> n) in + let pname = Symbol (sexp_location l, match oname with None -> "_" | Some n -> n) in match okn with | None -> pname | Some ((l, _) as n) -> Node (l, Symbol (l, "_:=_"), [Symbol n; pname]) @@ -71,10 +71,10 @@ let pexp_p_pat (s : sexp) : ppat = match s with | Symbol (_l, n) -> Ppatsym (s, match n with "_" -> None | _ -> Some n) | Node (l, c, args) -> Ppatcons (l, c, List.map pexp_p_pat_arg args) | _ - -> let l = Sexp.location s in + -> let l = sexp_location s in pexp_error l "Unknown pattern"; Ppatsym (s, None) let pexp_u_pat (p : ppat) : sexp = match p with - | Ppatsym (l, None) -> Symbol (Sexp.location l, "_") - | Ppatsym (l, Some n) -> Symbol (Sexp.location l, n) + | Ppatsym (l, None) -> Symbol (sexp_location l, "_") + | Ppatsym (l, Some n) -> Symbol (sexp_location l, n) | Ppatcons (l, c, args) -> Node (l, c, List.map pexp_u_pat_arg args) ===================================== src/sexp.ml ===================================== @@ -52,22 +52,14 @@ module Sym = struct && name l = name r end -let location : sexp -> location = function - | Block (l, _) -> l - | Symbol (l, _) -> l - | String (l, _) -> l - | Integer (l, _) -> l - | Float (l, _) -> l - | Node (l, _, _) -> l - let symbol ~(location : Source.Location.t) (name : string) : sexp = Symbol (Sym.intern ~location name) let node (head : sexp) (tail : sexp list) : sexp = let location = List.fold_left - (fun l e -> Source.Location.extend l (location e)) - (location head) + (fun l e -> Source.Location.extend l (sexp_location e)) + (sexp_location head) tail in Node (location, head, tail) ===================================== src/unification.ml ===================================== @@ -626,7 +626,12 @@ and unify_sortlvl (matching : scope_level option) when OL.conv_p ctx l1 l2 (* Arbitrarily selected `l1` over `l2` *) -> unify' l1 (mkSortLevel other) ctx vs matching - | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) + | SLlub (l1, l2), SLz | SLz, SLlub (l1, l2) + (* In this case, both `l1` and `l2` must be `SLz` *) + -> (unify' l1 (mkSortLevel SLz) ctx vs matching) + @(unify' l2 (mkSortLevel SLz) ctx vs matching) + | _, _ -> (add_residue ctx sortlvl lxp; + [(CKresidual, ctx, sortlvl, lxp)])) | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)] (** Unify a Sort and a lexp ===================================== typer.ml ===================================== @@ -73,7 +73,7 @@ let repl_main argv = parse_args argv usage; print_string (Fmt.make_title " TYPER REPL "); - print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; + print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2024"; print_newline (); print_endline " %quit (%q) : leave REPL"; print_endline " %help (%h) : print help"; @@ -85,6 +85,7 @@ let repl_main argv = let load_file (ectx, i) file_name = printf " In[% 2d] >> %%readfile %s\n" i file_name; + flush stdout; Elab.process_file backend ectx file_name, i + 1 in let ectx, i = List.fold_left load_file (ectx, 0) (list_input_files ()) in ===================================== typer.sh ===================================== @@ -9,6 +9,6 @@ # complete-filenames is useful for "%readfile ..." command # history-no-dupes just make it faster to search history with up and down key -rlwrap --complete-filenames --history-no-dupes 1 ./_build/typer $* +rlwrap --complete-filenames --history-no-dupes 1 ./_build/default/typer.bc $* # if not specified history must be kept in "~/.typer_history" View it on GitLab: https://gitlab.com/monnier/typer/-/compare/10d4fafcb572a8cbe9ec22ecad2436de… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/10d4fafcb572a8cbe9ec22ecad2436de… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][main] Don't transform builtins' types into closed form.
by Stefan (＠monnier) 12 Nov '24

12 Nov '24

Stefan pushed to branch main at Stefan / Typer Commits: 10d4fafc by Maxim Bernard at 2024-10-29T18:10:32-04:00 Don't transform builtins' types into closed form. * src/opslexp.ml: Add DB offset to `lmap`, and use it in `get_builtin` to shift all DB indices accordingly. Add context parameter to `get_builtin` (used to compute shift). Make necessary adaptations in `check` and `fv` now that builtin types aren't in closed form. * src/lexp.ml: Make necessary adaptations in `mkSusp`, `push_susp` and `clean`. * src/inverse_subst.ml: Make necessary adaptations in `apply_inv_subst`. * src/builtin.ml: Remove `kind` parameter from `new_builtin_type` since it shouldn't be anything else than `type0` (especially with the hardcoded DB offset). Provide new argument to `add_builtin_cst`. * src/elab.ml: Remove obsolete argument from `new_builtin_type` calls. Provide new argument to `add_builtin_cst`. Make necessary adaptations in `meta_to_var`, `sform_identifier`, `sform_built_in` and `default_ectx`. In `sform_built_in`, remove transformation to closed form. - - - - - 5 changed files: - src/builtin.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml Changes: ===================================== src/builtin.ml ===================================== @@ -131,21 +131,28 @@ let v2o_list v = in v2o_list [] v -let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) in - OL.add_builtin_cst name t; +let new_builtin_type name = + let t = mkBuiltin ((dloc, name), DB.type0) in + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `DB.type0` doesn't + * reference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 t; t let register_builtin_csts () = - OL.add_builtin_cst "TypeLevel" DB.type_level; - OL.add_builtin_cst "TypeLevel_z" DB.level0; - OL.add_builtin_cst "Type" DB.type0; - OL.add_builtin_cst "Type0" DB.type0; - OL.add_builtin_cst "Type1" DB.type1; - OL.add_builtin_cst "Integer" DB.type_integer; - OL.add_builtin_cst "Float" DB.type_float; - OL.add_builtin_cst "String" DB.type_string; - OL.add_builtin_cst "Eq" DB.type_eq; - OL.add_builtin_cst "I" DB.type_interval + (* Although the current context may not be empty when adding these builtins, + * we still provide 0 as the types' DB offset, since none of these types + * reference any var/metavar, so the offset doesn't matter in these cases. *) + OL.add_builtin_cst "TypeLevel" 0 DB.type_level; + OL.add_builtin_cst "TypeLevel_z" 0 DB.level0; + OL.add_builtin_cst "Type" 0 DB.type0; + OL.add_builtin_cst "Type0" 0 DB.type0; + OL.add_builtin_cst "Type1" 0 DB.type1; + OL.add_builtin_cst "Integer" 0 DB.type_integer; + OL.add_builtin_cst "Int" 0 DB.type_int; + OL.add_builtin_cst "Float" 0 DB.type_float; + OL.add_builtin_cst "String" 0 DB.type_string; + OL.add_builtin_cst "Eq" 0 DB.type_eq; + OL.add_builtin_cst "I" 0 DB.type_interval let _ = register_builtin_csts () ===================================== src/elab.ml ===================================== @@ -118,15 +118,21 @@ type special_decl_forms_map = let special_forms : special_forms_map ref = ref SMap.empty let special_decl_forms : special_decl_forms_map ref = ref SMap.empty -let type_special_form = BI.new_builtin_type "Special-Form" type0 -let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form" type0 +let type_special_form = BI.new_builtin_type "Special-Form" +let type_special_decl_form = BI.new_builtin_type "Special-Decl-Form" let add_special_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_form)); special_forms := SMap.add name func (!special_forms) let add_special_decl_form (name, func) = - OL.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_decl_form)); + (* Although the current context may not be empty when adding this builtins, + * we still provide 0 as the type's DB offset, since `type_special_decl_form` + * doesn'treference any var/metavar, so the offset doesn't matter. *) + OL.add_builtin_cst name 0 (mkBuiltin ((dloc, name), type_special_decl_form)); special_decl_forms := SMap.add name func (!special_decl_forms) let get_special_form name = @@ -494,7 +500,7 @@ let meta_to_var ids (e : lexp) = | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, loop o t) | Var (n,i) -> if i < o then e else mkVar (n, i + count) | Proj (l, lxp, lbl) -> mkProj (l, loop o lxp, lbl) | Susp (e, s) -> loop o (push_susp e s) @@ -642,7 +648,7 @@ and sform_identifier ctx loc sargs ot = when String.length name >= 1 && String.get name 0 == '#' -> if String.length name > 2 && String.get name 1 == '#' then let name = string_sub name 2 (String.length name) in - try let e = OL.get_builtin name in + try let e = OL.get_builtin (ectx_to_lctx ctx) name in (e, Inferred (OL.get_type (ectx_to_lctx ctx) e)) with | Not_found @@ -1639,16 +1645,16 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - (* FIXME: This `L.clean` is basically the last remaining use of the - * function. It's not indispensible, tho it might still be useful for + (* FIXME: This `L.clean` is one of the last remaining uses of the + * function. It's not indispensible, tho it might still be useful for * performance of type-inference (at least until we have proper - * memoization of push_susp and/or whnf). *) - -> let ltp' = Lexp.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + * memoization of push_susp and/or whnf). *) + -> let ltp' = Lexp.clean ltp in let bi = mkBuiltin ((Sexp.location loc, name), ltp') in if not (SMap.mem name (!EV.builtin_functions) || List.mem name DB.builtin_axioms) then sexp_error (Sexp.location loc) {|Unknown built-in "%s"|} name; - OL.add_builtin_cst name bi; + OL.add_builtin_cst name (DB.get_size ctx) bi; (bi, Checked) | None -> error ~loc:(Sexp.location loc) "Built-in's type not provided by context!"; sform_dummy_ret ctx loc) @@ -2065,7 +2071,7 @@ let default_ectx (* Empty context *) let ectx = empty_elab_context in - let ectx = SMap.fold (fun key e ctx + let ectx = SMap.fold (fun key (_o, e) ctx -> if String.get key 0 = '-' then ctx else ctx_define ctx (dsinfo, Some key) e (OL.get_type (ectx_to_lctx ectx) e)) ===================================== src/inverse_subst.ml ===================================== @@ -271,7 +271,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (_l, (StypeOmega | StypeLevel)) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, apply_inv_subst t s) | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) | Proj (l,lxp,lbl) -> mkProj (l, apply_inv_subst lxp s, lbl) | Susp (e, s') -> apply_inv_subst (push_susp e s') s ===================================== src/lexp.ml ===================================== @@ -345,7 +345,7 @@ let rec mkSusp e s = * it just seemed like a good idea to do it eagerly when it's easy. *) match lexp_lexp' e with | Imm _ -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Susp (e, s') -> mkSusp_memo e (scompose s' s) | Var (l,v) -> slookup s l v | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) @@ -443,8 +443,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> mkSortLevel (mkSLlub' (push_susp e1 s, push_susp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (_, _) -> e - | Builtin _ -> e - + | Builtin (sym, t) -> mkBuiltin (sym, mkSusp t s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let rec loop s defs = match defs with @@ -512,7 +511,7 @@ let clean e = -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (_, _) -> e - | Builtin _ -> e + | Builtin (sym, t) -> mkBuiltin (sym, clean s t) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) ===================================== src/opslexp.ml ===================================== @@ -131,28 +131,21 @@ let rec lctx_to_subst lctx = (List.rev defs) in L.scompose s2 s1 -(* Map of lexp builtin elements accessible via (## <name>). *) -let lmap = ref (SMap.empty : lexp SMap.t) - -let add_builtin_cst (name : string) (e : lexp) +(* Map of lexp builtin elements accessible via (## <name>). + * Values are pairs consisting of : + * - the type's De Bruijn offset (i.e. the context's size when the builtin + * was added) + * - the builtin's type *) +let lmap = ref (SMap.empty : (S.db_offset * lexp) SMap.t) + +let add_builtin_cst (name : string) (offset : S.db_offset) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - lmap := SMap.add name e map - -let get_builtin (name) = SMap.find name !lmap - -(* Take an expression `e` that is "closed" relatively to context lctx - * and return an equivalent expression valid in the empty context. - * By "closed" I mean that it only refers to elements of the context which - * are LetDef. *) -let lexp_close lctx e = - (* There are many different ways to skin this cat. - * This is definitely not the best one: - * - it inlines all the definitions everywhere they're used - * - It turns the lctx (of O(log N) access time) into a subst - * (of O(N) access time) - * Oh well! *) - mkSusp e (lctx_to_subst lctx) + lmap := SMap.add name (offset, e) map + +let get_builtin (ctx : lexp_context) (name) = + let (offset, btl) = SMap.find name !lmap in + mkSusp btl (S.shift ((M.length ctx) - offset)) let type_dummy = DB.type_integer @@ -568,7 +561,7 @@ and mk_eq_witness sinfo e ctx = | _ -> Log.internal_error "" in (* FIXME: Doesn't `e` need a "shift" here? *) let fn = mkLambda (Aerasable, (sinfo, None), etype, e) in - mkCall (sinfo, get_builtin "Eq.eq", + mkCall (sinfo, get_builtin ctx "Eq.eq", [Aerasable, elevel; Aerasable, etype; Anormal, fn]) @@ -711,7 +704,7 @@ and check'' erased ctx e = * Log.internal_error "Reached unreachable sort!"; *) DB.sort_omega) | Builtin (_, t) - -> let _ = check_type DB.set_empty Myers.nil t in + -> let _ = check_type erased ctx t in t (* FIXME: Check recursive references. *) | Var (((loc, name), idx) as v) @@ -1065,7 +1058,7 @@ and fv (e : lexp) : (db_set * mv_set) = | SortLevel (SLlub (e1, e2)) -> fv_union (fv e1) (fv e2) | Sort (_, Stype e) -> fv e | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty - | Builtin _ -> fv_empty + | Builtin (_, t) -> fv t | Var (_, i) -> (DB.set_singleton i, mv_set_empty) | Proj (_, lxp, _) -> fv lxp | Susp (e, s) -> fv (push_susp e s) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/10d4fafcb572a8cbe9ec22ecad2436dee… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/10d4fafcb572a8cbe9ec22ecad2436dee… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Novembre 2024