Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Novembre 2024
- 2 participants
- 3 discussions
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
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
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