[Typer] [Git][monnier/typer][main] 2 commits: Miscellanious bug fixes and code cleanups.

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@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@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/10d4fafcb572a8cbe9ec22ecad2436dee...