[Typer] [Git][monnier/typer][track-sexp-lexp] first

Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer

Commits: c4bb0b85 by Fallismaila at 2022-03-04T00:25:36+00:00 first

- - - - -

18 changed files:

- + .idea/.gitignore - + .idea/modules.xml - + .idea/typer.iml - + .idea/vcs.xml - + .vscode/settings.json - doc/primer.md - + log.txt - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/heap.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/sexp.ml - src/subst.ml - src/unification.ml

Changes:

===================================== .idea/.gitignore ===================================== @@ -0,0 +1,8 @@ +# Default ignored files +/shelf/ +/workspace.xml +# Editor-based HTTP Client requests +/httpRequests/ +# Datasource local storage ignored files +/dataSources/ +/dataSources.local.xml

===================================== .idea/modules.xml ===================================== @@ -0,0 +1,8 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="ProjectModuleManager"> + <modules> + <module fileurl="file://$PROJECT_DIR$/.idea/typer.iml" filepath="$PROJECT_DIR$/.idea/typer.iml" /> + </modules> + </component> +</project> \ No newline at end of file

===================================== .idea/typer.iml ===================================== @@ -0,0 +1,9 @@ +<?xml version="1.0" encoding="UTF-8"?> +<module type="JAVA_MODULE" version="4"> + <component name="NewModuleRootManager" inherit-compiler-output="true"> + <exclude-output /> + <content url="file://$MODULE_DIR$" /> + <orderEntry type="inheritedJdk" /> + <orderEntry type="sourceFolder" forTests="false" /> + </component> +</module> \ No newline at end of file

===================================== .idea/vcs.xml ===================================== @@ -0,0 +1,6 @@ +<?xml version="1.0" encoding="UTF-8"?> +<project version="4"> + <component name="VcsDirectoryMappings"> + <mapping directory="" vcs="Git" /> + </component> +</project> \ No newline at end of file

===================================== .vscode/settings.json ===================================== @@ -0,0 +1,6 @@ +{ + "ocaml.sandbox": { + "kind": "opam", + "switch": "default" + } +} \ No newline at end of file

===================================== doc/primer.md ===================================== @@ -1,4 +1,4 @@ -# Typer Primer +c# Typer Primer

## Basic functional programming

===================================== log.txt ===================================== @@ -0,0 +1,2 @@ +gcc: fatal error: no input files +compilation terminated.

===================================== src/builtin.ml ===================================== @@ -90,7 +90,7 @@ let predef_map : lexp SMap.t ref let get_predef (name: string) (ctx: DB.elab_context) : lexp = try let r = (DB.get_size ctx) - !builtin_size - 0 in let p = SMap.find name (!predef_map) in - mkSusp p (S.shift r) + mkSusp p (S.shift r) sinfo with Not_found -> log_raise_error {|"%s" was not predefined|} name

let set_predef name lexp @@ -100,7 +100,7 @@ let set_predef name lexp let dloc = DB.dloc

let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc, - mkArrow (Anormal, (dloc, None), t, dloc, t)) + mkArrow (Anormal, (dloc, None), t, dloc, t) sinfo) sinfo

let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx

@@ -140,7 +140,7 @@ let add_builtin_cst (name : string) (e : lexp) lmap := SMap.add name (e, t) map

let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) in + let t = mkBuiltin ((dloc, name), kind) sinfo in add_builtin_cst name t; t

@@ -159,7 +159,7 @@ let register_builtin_csts () = add_builtin_cst "Eq.refl" DB.eq_refl

let type_arrow_0 = - mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) sinfo

let register_builtin_types () = let _ = new_builtin_type "Sexp" DB.type0 in

===================================== src/debruijn.ml ===================================== @@ -83,33 +83,33 @@ let fatal ?print_action ?loc fmt = * ---------------------------------- *)

let dloc = dummy_location -let type_level_sort = mkSort (dloc, StypeLevel) -let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) -let level0 = mkSortLevel SLz -let level1 = mkSortLevel (mkSLsucc level0) -let level2 = mkSortLevel (mkSLsucc level1) -let type0 = mkSort (dloc, Stype level0) -let type1 = mkSort (dloc, Stype level1) -let type2 = mkSort (dloc, Stype level2) -let type_int = mkBuiltin ((dloc, "Int"), type0) -let type_integer = mkBuiltin ((dloc, "Integer"), type0) -let type_float = mkBuiltin ((dloc, "Float"), type0) -let type_string = mkBuiltin ((dloc, "String"), type0) -let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) +let type_level_sort = mkSort (dloc, StypeLevel) sinfo +let sort_omega = mkSort (dloc, StypeOmega) sinfo +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) sinfo +let level0 = mkSortLevel SLz sinfo +let level1 = mkSortLevel (mkSLsucc level0) sinfo +let level2 = mkSortLevel (mkSLsucc level1) sinfo +let type0 = mkSort (dloc, Stype level0) sinfo +let type1 = mkSort (dloc, Stype level1) sinfo +let type2 = mkSort (dloc, Stype level2) sinfo +let type_int = mkBuiltin ((dloc, "Int"), type0) sinfo +let type_integer = mkBuiltin ((dloc, "Integer"), type0) sinfo +let type_float = mkBuiltin ((dloc, "Float"), type0) sinfo +let type_string = mkBuiltin ((dloc, "String"), type0) sinfo +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) sinfo let type_eq_type = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkSort (dloc, Stype (mkVar (lv, 0) sinfo)) sinfo, dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 0), dloc, + mkVar (tv, 0) sinfo, dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 1), dloc, - mkSort (dloc, Stype (mkVar (lv, 3))))))) -let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) + mkVar (tv, 1) sinfo, dloc, + mkSort (dloc, Stype (mkVar (lv, 3) sinfo)) sinfo) sinfo) sinfo) sinfo) sinfo +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) sinfo let eq_refl = let lv = (dloc, Some "l") in let tv = (dloc, Some "t") in @@ -118,14 +118,14 @@ let eq_refl = mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0))), dloc, + mkSort (dloc, Stype (mkVar (lv, 0) sinfo)) sinfo, dloc, mkArrow (Aerasable, xv, - mkVar (tv, 0), dloc, + mkVar (tv, 0) sinfo, dloc, mkCall (type_eq, - [Aerasable, mkVar (lv, 2); - Aerasable, mkVar (tv, 1); - Anormal, mkVar (xv, 0); - Anormal, mkVar (xv, 0)]))))) + [Aerasable, mkVar (lv, 2) sinfo; + Aerasable, mkVar (tv, 1) sinfo; + Anormal, mkVar (xv, 0) sinfo; + Anormal, mkVar (xv, 0) sinfo]) sinfo) sinfo) sinfo) sinfo) sinfo

(* easier to debug with type annotations *) @@ -380,7 +380,7 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in let (_, _, t) = lctx_lookup ctx vref in - mkSusp t (S.shift (i + 1)) + mkSusp t (S.shift (i + 1)) sinfo

let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in

===================================== src/elab.ml ===================================== @@ -111,7 +111,7 @@ let special_forms : special_forms_map ref = ref SMap.empty let type_special_form = BI.new_builtin_type "Special-Form" type0

let add_special_form (name, func) = - BI.add_builtin_cst name (mkBuiltin ((dloc, name), type_special_form)); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form) sinfo); special_forms := SMap.add name func (!special_forms)

let get_special_form name = @@ -261,14 +261,14 @@ let ctx_define_rec (ctx: elab_context) decls =

let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in - mkMetavar (meta, S.identity, name) + mkMetavar (meta, S.identity, name) sinfo

let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

let newMetatype (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "τ") - (mkSort (loc, Stype (newMetalevel ctx sl loc))) + (mkSort (loc, Stype (newMetalevel ctx sl loc)) sinfo)

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -303,7 +303,7 @@ let elab_varref ctx (loc, name) = try let idx = senv_lookup name ctx in let id = (loc, Some name) in - let lxp = mkVar (id, idx) in + let lxp = mkVar (id, idx) sinfo in let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp) with Senv_Lookup_Fail xs -> @@ -311,7 +311,7 @@ let elab_varref ctx (loc, name) if ((List.length xs) > 0) then ". Did you mean: " ^ (String.concat " or " xs) ^" ?" else "" in - sexp_error loc {|The variable "%s" was not declared%s|} name relateds; + sexp_error loc {|The variable "%s" was not declared%s|} name relateds; sform_dummy_ret ctx loc)

(* Turn metavar into plain vars after generalization. @@ -423,12 +423,12 @@ let meta_to_var ids (e : lexp) = match lexp_lexp' e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) sinfo + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) sinfo | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) sinfo | Susp (e, s) -> loop o (push_susp e s) | Let (l, defs, e) -> let len = List.length defs in @@ -438,13 +438,13 @@ let meta_to_var ids (e : lexp) = (o', (l, loop (len + o) e, loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, loop (len + o) e) + mkLet (l, ndefs, loop (len + o) e) sinfo | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) sinfo | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop o t, loop (1 + o) e) + -> mkLambda (ak, v, loop o t, loop (1 + o) e) sinfo | Call (f, args) - -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args) sinfo | Inductive (l, label, args, cases) -> let alen = List.length args in let (_, nargs) @@ -466,8 +466,8 @@ let meta_to_var ids (e : lexp) = fields (flen + alen, []) in nfields) cases in - mkInductive (l, label, nargs, ncases) - | Cons (t, l) -> mkCons (loop o t, l) + mkInductive (l, label, nargs, ncases) sinfo + | Cons (t, l) -> mkCons (loop o t, l) sinfo | Case (l, e, t, cases, default) -> let ncases = SMap.map @@ -476,13 +476,13 @@ let meta_to_var ids (e : lexp) = cases in mkCase (l, loop o e, loop o t, ncases, match default with None -> None - | Some (v, e) -> Some (v, loop (2 + o) e)) + | Some (v, e) -> Some (v, loop (2 + o) e)) sinfo | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + count - IMap.find id ids) + mkVar (name, o + count - IMap.find id ids) sinfo else match metavar_lookup id with | MVal e -> loop o (push_susp e s) - | _ -> mkMetavar (id, adjust_subst o s, name) + | _ -> mkMetavar (id, adjust_subst o s, name) sinfo in loop 0 e

let sort_generalized_metavars sl cl ctx mfvs = @@ -617,12 +617,12 @@ and get_implicit_arg ctx loc oname t =

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = - let rec instantiate t args = + let rec instantiate t args = match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in - instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args), t) + instantiate (mkSusp t2 (S.substitute arg) sinfo) ((ak, arg)::args) + | _ -> (mkCall (e, List.rev args) sinfo, t) in instantiate t []

and infer_type pexp ectx var = @@ -643,7 +643,7 @@ and infer_type pexp ectx var = Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) (ectx_to_scope_level ectx) - l))) + l)) sinfo) s (ectx_to_lctx ectx) with | (_::_) @@ -658,7 +658,7 @@ and infer_type pexp ectx var = t

and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) + List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) sinfo) declss body

and unify_with_arrow ctx tloc lxp kind var aty @@ -668,7 +668,7 @@ and unify_with_arrow ctx tloc lxp kind var aty let nctx = ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in - let arrow = mkArrow (kind, var, arg, l, body) in + let arrow = mkArrow (kind, var, arg, l, body) sinfo in match Unif.unify arrow lxp (ectx_to_lctx ctx) with | ((_ck, _ctx, t1, t2)::_) -> lexp_error @@ -756,12 +756,12 @@ and check_case rtype (loc, target, ppatterns) ctx = -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) - name (mkSusp t s) in + name (mkSusp t s sinfo) in (S.cons arg s, (ak, arg) :: targs)) (S.identity, []) fargs in let (cs, args) = (constructors, List.rev targs) in - ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + ltarget := check_inferred ctx tlxp tltp (mkCall (it', args) sinfo); it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = @@ -788,7 +788,7 @@ and check_case rtype (loc, target, ppatterns) ctx =

let shift_to_extended_ctx nctx lexp = mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx) - - M.length (ectx_to_lctx ctx))) in + - M.length (ectx_to_lctx ctx))) sinfo in

let ctx_extend_with_eq nctx head_lexp = (* Add a proof of equality between the target and the branch @@ -800,14 +800,14 @@ and check_case rtype (loc, target, ppatterns) ctx = [(Aerasable, tlvl'); (* Typelevel *) (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) - (Anormal, tlxp')]) (* Target lexp *) + (Anormal, tlxp')]) sinfo (* Target lexp *) in ctx_extend nctx (loc, None) Variable eqty in

let add_default v = (if dflt != None then uniqueness_warn pat); let nctx = ctx_extend ctx v Variable tltp in - let head_lexp = mkVar (v, 0) in + let head_lexp = mkVar (v, 0) sinfo in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in @@ -824,7 +824,7 @@ and check_case rtype (loc, target, ppatterns) ctx = v t in let nctx = ctx_extend ctx v Variable t in let body = inst_args nctx body in - mkSusp body (S.substitute arg) + mkSusp body (S.substitute arg) sinfo | _e -> lxp in match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) @@ -833,7 +833,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let cargs = try SMap.find cons_name constructors with | Not_found - -> lexp_error + -> lexp_error loc lctor {|"%s" does not a have a "%s" constructor|} (lexp_string it') cons_name; [] in @@ -861,7 +861,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | (_, (ak, (_, Some fname), fty)::cargs) when SMap.mem fname pe -> let var = SMap.find fname pe in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in make_nctx nctx (ssink var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) @@ -869,7 +869,7 @@ and check_case rtype (loc, target, ppatterns) ctx = when (match (ef, ak) with | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) - -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in make_nctx nctx (ssink var s) pargs cargs pe ((ak, var)::acc) | ((Some (l, fname), var)::pargs, cargs) @@ -878,7 +878,7 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in if ak = Anormal then sexp_error loc {|Missing pattern for normal field%s|} @@ -890,11 +890,11 @@ and check_case rtype (loc, target, ppatterns) ctx = let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in let head_lexp_ctor = shift_to_extended_ctx nctx - (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs) sinfo) in let head_lexp_args = List.mapi (fun i (ak, vname) -> - (ak, mkVar (vname, List.length fargs - i - 1))) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in + (ak, mkVar (vname, List.length fargs - i - 1) sinfo)) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) sinfo in let nctx = ctx_extend_with_eq nctx head_lexp in let rtype' = shift_to_extended_ctx nctx rtype in let lexp = check pexp rtype' nctx in @@ -917,7 +917,7 @@ and check_case rtype (loc, target, ppatterns) ctx = let (lpattern, dflt) = List.fold_left fold_fun (SMap.empty, None) ppatterns in

- mkCase (loc, tlxp, rtype, lpattern, dflt) + mkCase (loc, tlxp, rtype, lpattern, dflt) sinfo

and elab_macro_call ctx func args ot = let t @@ -949,7 +949,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs (SMap.remove aname pending) - (L.mkSusp ret_type (S.substitute larg)) + (L.mkSusp ret_type (S.substitute larg) sinfo)

| (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs, Arrow (ak, _, arg_type, _, ret_type) @@ -957,7 +957,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Explicit-implicit argument. *) -> let larg = check sarg arg_type ctx in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) + (L.mkSusp ret_type (S.substitute larg) sinfo)

| (Node (Symbol (_, "_:=_"), [Symbol (l, aname); sarg])) :: sargs, Arrow _ @@ -982,7 +982,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | sarg::_ -> sexp_location sarg) v arg_type in handle_fun_args ((ak, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) + (L.mkSusp ret_type (S.substitute larg) sinfo) | [], _ -> (if not (SMap.is_empty pending) then let pending = SMap.bindings pending in @@ -1002,10 +1002,10 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = ltp' Anormal (dloc, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending - (L.mkSusp ret_type (S.substitute larg)) in + (L.mkSusp ret_type (S.substitute larg) sinfo) in

let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs), Inferred ret_type) + (mkCall (func, List.rev largs) sinfo, Inferred ret_type)

(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = @@ -1022,11 +1022,11 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> mkArrow (ak, n, t, dummy_location, aa)) + -> mkArrow (ak, n, t, dummy_location, aa) sinfo) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e)) + -> mkArrow (Aerasable, vname, t, l, e) sinfo) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1193,12 +1193,12 @@ and infer_and_generalize_type (ctx : elab_context) se name = let rec strip_rettype t = match lexp_lexp' t with | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) + -> mkArrow (ak, v, t1, l, strip_rettype t2) sinfo | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) + -> mkArrow (Aerasable, name, t, l, e) sinfo) t

and infer_and_generalize_def (ctx : elab_context) se = @@ -1207,11 +1207,11 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = generalize nctx e in let e' = g (fun ne vname t _l e -> mkLambda ((if ne then Aimplicit else Aerasable), - vname, t, e)) + vname, t, e) sinfo) e in let t' = g (fun ne name t _l e -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e)) + name, t, sexp_location se, e) sinfo) t in (e', t')

@@ -1297,7 +1297,7 @@ and lexp_decls_1 let var = (l, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, + [(var, mkSusp lexp (S.shift 1) sinfo, ltp)], sdecls, toks, ctx_define nctx var lexp ltp

| [Symbol (loc, vname); sexp] @@ -1409,7 +1409,7 @@ let sform_built_in ctx loc sargs ot = * performance of type-inference (at least until we have proper * memoization of push_susp and/or whnf). *) -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') in + let bi = mkBuiltin ((loc, name), ltp') sinfo in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc {|Unknown built-in "%s"|} name; BI.add_builtin_cst name bi; @@ -1427,7 +1427,7 @@ let sform_datacons ctx loc sargs _ot = match sargs with | [t; Symbol ((_sloc, _cname) as sym)] -> let idt, _ = infer t ctx in - (mkCons (idt, sym), Lazy) + (mkCons (idt, sym) sinfo, Lazy)

| [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; sform_dummy_ret ctx loc @@ -1499,7 +1499,7 @@ let sform_typecons ctx loc sargs _ot = constrs [] in

let map_ctor = lexp_parse_inductive ctors nctx in - (mkInductive (loc, label, formals, map_ctor), Lazy) + (mkInductive (loc, label, formals, map_ctor) sinfo, Lazy)

let sform_hastype ctx loc sargs _ot = match sargs with @@ -1518,15 +1518,15 @@ let sform_arrow kind ctx loc sargs _ot = let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (sexp_location st2, None) in - (mkArrow (kind, v, lt1, loc, lt2), Lazy) + (mkArrow (kind, v, lt1, loc, lt2) sinfo, Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; sform_dummy_ret ctx loc

let sform_immediate ctx loc sargs ot = match sargs with - | [(String _) as se] -> mkImm (se), Inferred DB.type_string - | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int - | [(Float _) as se] -> mkImm (se), Inferred DB.type_float + | [(String _) as se] -> mkImm (se) sinfo, Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se) sinfo, Inferred DB.type_int + | [(Float _) as se] -> mkImm (se) sinfo, Inferred DB.type_float | [Block (_location, pts)] -> let grm = ectx_get_grammar ctx in let tokens = lex default_stt pts in @@ -1575,7 +1575,7 @@ let sform_identifier ctx loc sargs ot = match (metavar_lookup idx) with | MVar (sl',_,_) -> if sl = sl' then - (mkMetavar (idx, subst, (loc, Some name)), Lazy) + (mkMetavar (idx, subst, (loc, Some name)) sinfo, Lazy) else (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for @@ -1600,7 +1600,7 @@ let sform_identifier ctx loc sargs ot = | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); - (mkSusp mv subst, + (mkSusp mv subst sinfo, match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *) @@ -1638,9 +1638,9 @@ let rec sform_lambda kind ctx loc sargs ot = | Some lt2 -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in - (mkLambda (kind, arg, lt1, lbody), + (mkLambda (kind, arg, lt1, lbody) sinfo, match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) + | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) sinfo) | _ -> alt) in

(match ot with @@ -1672,14 +1672,14 @@ let rec sform_lambda kind ctx loc sargs ot = (* FIXME: Don't go back to sform_lambda, but use an internal * loop to avoid re-computing olt1 each time. *) let (lam, alt) = sform_lambda kind nctx loc sargs (Some lt2) in - (mkLambda (ak2, v, lt1, lam), + (mkLambda (ak2, v, lt1, lam) sinfo, match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) + | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') sinfo) | _ -> alt)

| _lt -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 - in mklam lt1 (Some lt2)) + in mklam lt1 (Some lt2) )

| _ -> sexp_error @@ -1717,10 +1717,10 @@ let sform_letin ctx loc sargs ot = match sargs with List.fold_left (fun (s, off) decls -> (OL.lexp_defs_subst loc s decls, off + List.length decls)) (S.identity, 0) declss in - let ot = Option.map (fun t -> mkSusp t (S.shift off)) ot in + let ot = Option.map (fun t -> mkSusp t (S.shift off) sinfo) ot in let bdy, ot = elaborate nctx sbody ot in let ot = match ot with - | Inferred t -> Inferred (mkSusp t s) + | Inferred t -> Inferred (mkSusp t s sinfo) | _ -> ot in (lexp_let_decls declss bdy nctx, ot) | _ -> sexp_error loc "Unrecognized let_in_ expression"; @@ -1728,10 +1728,10 @@ let sform_letin ctx loc sargs ot = match sargs with

let rec infer_level ctx se : lexp = match se with - | Symbol (_, "z") -> mkSortLevel SLz + | Symbol (_, "z") -> mkSortLevel SLz sinfo | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) - -> mkSortLevel (SLsucc (infer_level ctx se)) + -> mkSortLevel (SLsucc (infer_level ctx se)) sinfo | Node (Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in @@ -1747,8 +1747,8 @@ let rec infer_level ctx se : lexp = let sform_type ctx loc sargs _ot = match sargs with | [se] -> let l = infer_level ctx se in - (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) + (mkSort (loc, Stype l) sinfo, + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) sinfo)) sinfo)) | _ -> (sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc)

@@ -1759,7 +1759,7 @@ let sform_debruijn ctx loc sargs _ot = (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else - let lxp = mkVar ((loc, None), i) in (lxp, Lazy) + let lxp = mkVar ((loc, None), i) sinfo in (lxp, Lazy) | _ -> (sexp_error loc "##DeBruijn expects one integer argument"; sform_dummy_ret ctx loc)

@@ -1831,7 +1831,7 @@ let sform_load usr_elctx loc sargs _ot = let tuple' = if !in_pervasive then tuple else - (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) in + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) sinfo) in

(tuple',Lazy)

@@ -1885,11 +1885,12 @@ let default_ectx let _, lctx = lexp_p_decls [] sxps elctx in lctx in

+ (* Register predef *) let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) in + let v = mkVar ((dloc, Some name), idx) sinfo in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -1978,6 +1979,7 @@ let process_file let ldecls, ectx' = lexp_p_decls [] tokens ectx in List.iter backend#process_decls ldecls; ectx' + with | Sys_error _ -> (error {|file %s does not exist.|} file_name;

===================================== src/eval.ml ===================================== @@ -553,7 +553,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1))])) + -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) sinfo)]) sinfo) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f)

and eval_case ctx i loc target pat dflt = @@ -803,7 +803,7 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -817,7 +817,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -838,7 +838,7 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx) sinfo) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -856,7 +856,7 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i @@ -877,7 +877,7 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with | Cons (e, _) when is_var e -> (match (env_lookup_expr ectx (get_var e)) with | Some i when is_inductive i

===================================== src/heap.ml ===================================== @@ -39,8 +39,8 @@ let error ~(loc : location) ?print_action fmt =

let dloc = Util.dummy_location let type0 = Debruijn.type0 -let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) -let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) sinfo +let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) sinfo

let next_free_address : addr ref = ref 1

===================================== src/inverse_subst.ml ===================================== @@ -65,7 +65,7 @@ let transfo (s: subst) : substIR option = | _ -> assert false in let shiftVar (var: lexp) (offset: int): int = - indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) + indexOf (mkSusp var (S.shift offset) sinfo) (* Helper : shift the index of a var *) in match s with | S.Cons (e, s, o) when is_var e @@ -94,7 +94,7 @@ let sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - mkVar ((U.dummy_location, None), idx) + mkVar ((U.dummy_location, None), idx) sinfo

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -256,14 +256,14 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) sinfo | SortLevel (SLlub (e1, e2)) (* FIXME: use mkSLlub? *) - -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) - | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) sinfo | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) sinfo | Susp (e, s') -> apply_inv_subst (push_susp e s') s | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in @@ -273,15 +273,15 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = (v, apply_inv_subst def s', apply_inv_subst ty s) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, apply_inv_subst e s') + mkLet (l, ndefs, apply_inv_subst e s') sinfo | Arrow (ak, v, t1, l, t2) -> mkArrow (ak, v, apply_inv_subst t1 s, l, - apply_inv_subst t2 (ssink v s)) + apply_inv_subst t2 (ssink v s)) sinfo | Lambda (ak, v, t, e) - -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) + -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) sinfo | Call (f, args) -> mkCall (apply_inv_subst f s, - L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) sinfo | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) @@ -297,8 +297,8 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> mkCons (apply_inv_subst it s, name) + mkInductive (l, label, nargs, ncases) sinfo + | Cons (it, name) -> mkCons (apply_inv_subst it s, name) sinfo | Case (l, e, ret, cases, default) -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, SMap.map (fun (l, cargs, e) @@ -310,8 +310,8 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) sinfo | Metavar (id, s', name) -> match metavar_lookup id with | MVal e -> apply_inv_subst (push_susp e s') s - | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) + | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) sinfo

===================================== src/lexp.ml ===================================== @@ -41,6 +41,8 @@ type label = symbol

include Pexp.ArgKind

+let sinfo: (sexp list) = [] + (*************** Elaboration to Lexp *********************)

(* The scoping of `Let` is tricky: @@ -59,7 +61,7 @@ include Pexp.ArgKind type ltype = lexp and subst = lexp S.subst (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) - and lexp = lexp' * int + and lexp = lexp' * int * sexp list and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level @@ -177,8 +179,8 @@ let metavar_lookup (id : meta_id) : metavar_info * biggest bucket length: 205 / 36 * found/new lexp entries: - / 2 *)

-let lexp_lexp' (e, _h) = e -let lexp_hash (_e, h) = h +let lexp_lexp' (e, _h, _) = e +let lexp_hash (_e, h, _) = h

(* Hash `Lexp` using combine_hash (lxor) with hash of "sub-lexp". *) let lexp'_hash (lp : lexp') = @@ -301,28 +303,28 @@ module WHC = Weak.Make (struct type t = lexp

let hc_table : WHC.t = WHC.create 1000

-let hc (l : lexp') : lexp = - WHC.merge hc_table (l, lexp'_hash l) - -let mkImm s = hc (Imm s) -let mkSortLevel l = hc (SortLevel l) -let mkSort (l, s) = hc (Sort (l, s)) -let mkBuiltin (v, t) = hc (Builtin (v, t)) -let mkVar v = hc (Var v) -let mkLet (l, ds, e) = hc (Let (l, ds, e)) -let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2)) -let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) -let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) -let mkCons (t, n) = hc (Cons (t, n)) -let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) = +let hc (l : lexp') (sinfo: sexp list) : lexp = + WHC.merge hc_table (l, lexp'_hash l, sinfo) + +let mkImm s sinfo = hc (Imm s) sinfo +let mkSortLevel l sinfo = hc (SortLevel l) sinfo +let mkSort (l, s) sinfo = hc (Sort (l, s)) sinfo +let mkBuiltin (v, t) sinfo = hc (Builtin (v, t)) sinfo +let mkVar v sinfo = hc (Var v) sinfo +let mkLet (l, ds, e) sinfo = hc (Let (l, ds, e)) sinfo +let mkArrow (k, v, t1, l, t2) sinfo = hc (Arrow (k, v, t1, l, t2)) sinfo +let mkLambda (k, v, t, e) sinfo = hc (Lambda (k, v, t, e)) sinfo +let mkInductive (l, n, a, cs) sinfo = hc (Inductive (l, n, a, cs)) sinfo +let mkCons (t, n) sinfo = hc (Cons (t, n)) sinfo +let mkCase (l, e, rt, bs, d) sinfo = hc (Case (l, e, rt, bs, d)) sinfo +let mkMetavar (n, s, v) sinfo = hc (Metavar (n, s, v)) sinfo +let mkCall (f, es) sinfo = match lexp_lexp' f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | Call (f', es'), _ -> hc (Call (f', es' @ es)) sinfo | _, [] -> f - | _ -> hc (Call (f, es)) + | _ -> hc (Call (f, es)) sinfo

-let impossible = mkImm Sexp.dummy_epsilon +let impossible = mkImm Sexp.dummy_epsilon Sexp.dummy_sinfo

let lexp_head e = match lexp_lexp' e with @@ -439,7 +441,7 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * ... *)

-let rec mkSusp e s = +let rec mkSusp e s sinfo = if S.identity_p s then e else (* We apply the substitution eagerly to some terms. * There's no deep technical reason for that: @@ -448,29 +450,29 @@ let rec mkSusp e s = | Imm _ -> e | Builtin _ -> e | 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) - | _ -> hc (Susp (e, s)) + | Var (l, v) -> slookup s l v + | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) sinfo + | _ -> hc (Susp (e, s)) sinfo and mkSusp_memo e s = if Hashtbl.mem hcs_table (e, s) then Hashtbl.find hcs_table (e, s) - else let res = mkSusp e s in + else let res = mkSusp e s sinfo in Hashtbl.add hcs_table (e, s) res; res and scompose s1 s2 = S.compose mkSusp_memo s1 s2 -and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) - (fun e o -> mkSusp e (S.shift o)) +and slookup s l v = S.lookup (fun l i -> mkVar (l, i) sinfo) + (fun e o -> mkSusp e (S.shift o) sinfo) s l v -let ssink = S.sink (fun l i -> mkVar (l, i)) +let ssink = S.sink (fun l i -> mkVar (l, i) sinfo)

(* Apply a "dummy" substitution which replace #0 with #0 * in order to account for changes to a variable's name. - * This should probably be made into a no-op, but only after we get rid + * This should probably `````be made into a no-op, but only after we get rid * of the check in DB.lookup that a `Var` has the same name as the * one stored in the lctx! * Using DeBruijn *should* make α-renaming unnecessary * so this is a real PITA! :-( *) -let srename name le = mkSusp le (S.cons (mkVar (name, 0)) (S.shift 1)) +let srename name le = mkSusp le (S.cons (mkVar (name, 0) sinfo) (S.shift 1)) sinfo

(* Shift by a negative amount! *) let rec sunshift n = @@ -536,10 +538,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) - | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) + -> mkSortLevel (mkSLlub' (mkSusp e1 s sinfo, mkSusp e2 s sinfo)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s sinfo)) sinfo | Sort (_, _) -> e | Builtin _ -> e

@@ -548,40 +550,40 @@ let rec push_susp e s = (* Push a suspension one level down. *) let rec loop s defs = match defs with | [] -> [] | (v, def, ty) :: defs - -> (v, mkSusp def s', mkSusp ty s) :: loop (ssink v s) defs in - mkLet (l, loop s defs, mkSusp e s') + -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink v s) defs in + mkLet (l, loop s defs, mkSusp e s' sinfo) sinfo | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, mkSusp t1 s, l, mkSusp t2 (ssink v s)) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s)) - | Call (f, args) -> mkCall (mkSusp f s, - L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args) + -> mkArrow (ak, v, mkSusp t1 s sinfo, l, mkSusp t2 (ssink v s) sinfo) sinfo + | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s sinfo, mkSusp e (ssink v s) sinfo) sinfo + | Call (f, args) -> mkCall (mkSusp f s sinfo, + L.map (fun (ak, arg) -> (ak, mkSusp arg s sinfo)) args) sinfo | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink v s, (ak, v, mkSusp t s) :: nargs)) + -> (ssink v s, (ak, v, mkSusp t s sinfo) :: nargs)) (s, []) args in let nargs = List.rev nargs in let ncases = SMap.map (fun args -> let (_, ncase) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, - (ak, v, mkSusp t s) + (ak, v, mkSusp t s sinfo) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> mkCons (mkSusp it s, name) + mkInductive (l, label, nargs, ncases) sinfo + | Cons (it, name) -> mkCons (mkSusp it s sinfo, name) sinfo | Case (l, e, ret, cases, default) - -> mkCase (l, mkSusp e s, mkSusp ret s, + -> mkCase (l, mkSusp e s sinfo, mkSusp ret s sinfo, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e (ssink (l, None) s'))) + (l, cargs, mkSusp e (ssink (l, None) s') sinfo)) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)))) + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)) sinfo)) sinfo (* Susp should never appear around Var/Susp/Metavar because mkSusp * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp @@ -589,7 +591,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) * But we still have to handle them here, since push_susp is called * in many other cases than just when we bump into a Susp. *) | Susp (e,s') -> push_susp e (scompose s' s) - | (Var _ | Metavar _) -> nosusp (mkSusp e s) + | (Var _ | Metavar _) -> nosusp (mkSusp e s sinfo)

and nosusp e = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with @@ -603,11 +605,11 @@ let clean e = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) sinfo | SortLevel (SLlub (e1, e2)) (* FIXME: The new SLlub could have `succ` on both sides! *) - -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) sinfo | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) @@ -616,12 +618,12 @@ let clean e = -> (ssink v s, (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, clean s' e) + mkLet (l, ndefs, clean s' e) sinfo | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) - | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) + -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) sinfo + | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) sinfo | Call (f, args) -> mkCall (clean s f, - L.map (fun (ak, arg) -> (ak, clean s arg)) args) + L.map (fun (ak, arg) -> (ak, clean s arg)) args) sinfo | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) -> (ssink v s, (ak, v, clean s t) :: nargs)) @@ -636,8 +638,8 @@ let clean e = (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> mkCons (clean s it, name) + mkInductive (l, label, nargs, ncases) sinfo + | Cons (it, name) -> mkCons (clean s it, name) sinfo | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) @@ -649,15 +651,15 @@ let clean e = cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) sinfo | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e - else clean S.identity (mkSusp e s) + else clean S.identity (mkSusp e s sinfo) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with | MVal e -> clean s e - | _ -> mkMetavar (idx, s, name) + | _ -> mkMetavar (idx, s, name) sinfo in clean S.identity e

let sdatacons = Symbol (U.dummy_location, "##datacons") @@ -1186,10 +1188,10 @@ and subst_eq s1 s2 = eq e1 e2 && subst_eq s1 s2 else if o1 > o2 then let o = o1 - o2 in - eq (mkSusp e1 (S.shift o)) e2 + eq (mkSusp e1 (S.shift o) sinfo) e2 && subst_eq (S.mkShift s1 o) s2 else let o = o2 - o1 in - eq e1 (mkSusp e2 (S.shift o)) + eq e1 (mkSusp e2 (S.shift o) sinfo) && subst_eq s1 (S.mkShift s2 o) | _ -> false

===================================== src/opslexp.ml ===================================== @@ -108,7 +108,7 @@ let lookup_value = DB.lctx_lookup_value let rec lexp_defs_subst l s defs = match defs with | [] -> s | (_, lexp, _) :: defs' - -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp)) s) defs' + -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) sinfo) s) defs'

(** Convert a lexp_context into a substitution. *)

@@ -142,7 +142,7 @@ let lexp_close lctx e = * - 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) + mkSusp e (lctx_to_subst lctx) sinfo

(** Reduce to weak head normal form. @@ -185,9 +185,9 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = * to the idea of call-by-value, although in this context * we can't really make sure we always reduce the arg to a value. *) lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx)), - args)) + args) sinfo) ctx - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) + | Call (f', xs1) -> mkCall (f', List.append xs1 xs) sinfo | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) @@ -203,7 +203,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = mkCall (DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; - L.Aerasable, e]) in + L.Aerasable, e]) sinfo in let reduce it name aargs = let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with | Inductive (_,_,fargs,_) -> fargs @@ -232,14 +232,14 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | _ -> Log.log_error ~section:"WHNF" ~loc:l {|Unhandled constructor "%s" in case expression|} name; - mkCase (l, e, rt, branches, default) in + mkCase (l, e, rt, branches, default) sinfo in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> (match lexp_lexp' (lexp_whnf_aux f ctx) with | Cons (it, (_, name)) -> reduce it name aargs - | _ -> mkCase (l, e, rt, branches, default)) - | _ -> mkCase (l, e, rt, branches, default)) + | _ -> mkCase (l, e, rt, branches, default) sinfo) + | _ -> mkCase (l, e, rt, branches, default) sinfo) | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> lexp_whnf_aux (push_susp e s) ctx @@ -429,14 +429,14 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = S.identity fargs aargs in (* 3. Compare the branches *) let ctx_extend_with_eq ctx subst hlxp = - let tlxp = mkSusp target subst in - let tltp = mkSusp etype subst in - let tlvl = mkSusp elvl subst in + let tlxp = mkSusp target subst sinfo in + let tltp = mkSusp etype subst sinfo in + let tlvl = mkSusp elvl subst sinfo in let eqty = mkCall (DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) in (* Target lexp *) + (L.Anormal, tlxp)]) sinfo in (* Target lexp *) DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in (* The map module doesn't have a function to compare two maps with the key (which is needed to get the field types @@ -453,8 +453,8 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (ak', _vdef', ftype)::fieldtypes -> if ak1 = ak2 && ak2 = ak' then mkctx - (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s)) - ((ak1, (mkVar (vdef1, i)))::args) + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s sinfo)) + ((ak1, (mkVar (vdef1, i) sinfo))::args) (ssink vdef1 s) (i - 1) vdefs1 vdefs2 fieldtypes @@ -468,9 +468,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), - eaargs)) subst in - let hlxp = mkCall (ctor, args) in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) sinfo, + eaargs) sinfo) subst sinfo in + let hlxp = mkCall (ctor, args) sinfo in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2 ) (SMap.bindings cases1) (SMap.bindings cases2) @@ -481,7 +481,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Some (v1, e1), Some (_v2, e2)) -> let nctx = DB.lctx_extend ctx v1 Variable etype in let subst = S.shift 1 in - let hlxp = mkVar ((DB.dloc, None), 0) in + let hlxp = mkVar ((DB.dloc, None), 0) sinfo in let nctx = ctx_extend_with_eq nctx subst hlxp in conv_p' nctx (set_shift_n vs' 2) e1 e2 | None, None -> true @@ -505,13 +505,13 @@ and mkSLlub ctx e1 e2 = | (SortLevel SLz, _) -> e2 | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) - -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) sinfo | (_e1', _e2') -> let ce1 = level_canon lwhnf1 in let ce2 = level_canon lwhnf2 in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 - else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) + else mkSortLevel (mkSLlub' (e1, e2)) sinfo (* FIXME: Could be more canonical *)

and sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen @@ -523,13 +523,13 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = -> (match s1, s2 with | (Stype l1, Stype l2) -> if ak == P.Aerasable && impredicative_erase - then SortResult (mkSusp k2 (S.substitute impossible)) - else let l2' = (mkSusp l2 (S.substitute impossible)) in + then SortResult (mkSusp k2 (S.substitute impossible) sinfo) + else let l2' = (mkSusp l2 (S.substitute impossible) sinfo) in (* print_string ("Normal: " ^ lexp_string l1 ^ " -> " * ^ lexp_string l2' ^ " ==> " * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) * ^ "\n"); *) - SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) sinfo) | (StypeLevel, Stype _l2) when ak == P.Aerasable && impredicative_universe_poly (* The safety/soundness of this rule is completely unknown. @@ -540,7 +540,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * ^ lexp_string k2 ^ " ==> " * ^ lexp_string (mkSusp k2 (S.substitute DB.level0)) * ^ "\n"); *) - SortResult (mkSusp k2 (S.substitute DB.level0)) + SortResult (mkSusp k2 (S.substitute DB.level0) sinfo) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -548,7 +548,7 @@ and sort_compose ctx1 ctx2 l ak k1 k2 = * arguments, but let's not bother for now: it's easier to add it * later than to remove it later. * | (Stype _, StypeOmega) *) - -> SortResult (mkSort (l, StypeOmega)) + -> SortResult (mkSort (l, StypeOmega) sinfo) | _ -> SortInvalid) | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType @@ -624,7 +624,7 @@ and check'' erased ctx e = | Sort (l, Stype e) -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - mkSort (l, Stype (mkSortLevel (SLsucc e))) + mkSort (l, Stype (mkSortLevel (SLsucc e) sinfo)) sinfo | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; @@ -662,7 +662,7 @@ and check'' erased ctx e = n - 1) (List.length defs) defs in mkSusp (check nerased nctx e) - (lexp_defs_subst l S.identity defs) + (lexp_defs_subst l S.identity defs) sinfo | Arrow (ak, v, t1, loc, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -671,19 +671,19 @@ and check'' erased ctx e = | SortResult k -> k | SortInvalid -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; - mkSort (loc, StypeOmega) + mkSort (loc, StypeOmega) sinfo | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; - mkSort (loc, StypeOmega) + mkSort (loc, StypeOmega) sinfo | SortK2NotType -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; - mkSort (loc, StypeOmega)) + mkSort (loc, StypeOmega) sinfo) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, l, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) - e)) + e) sinfo) | Call (f, args) -> let ft = check erased ctx f in List.fold_left @@ -695,7 +695,7 @@ and check'' erased ctx e = -> if ak != ak' then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; assert_type ctx arg at t1; - mkSusp t2 (S.substitute arg) + mkSusp t2 (S.substitute arg) sinfo | _ -> log_tc_error ~loc:(lexp_location arg) "Calling a non functin (type = %s)!" (lexp_string ft); @@ -722,7 +722,7 @@ and check'' erased ctx e = * cannot refer to the fields! *) (* FIXME: If it does refer, * we get an ugly error! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' (L.sunshift n) sinfo) | _tt -> log_tc_error ~loc:(lexp_location t) @@ -737,14 +737,14 @@ and check'' erased ctx e = (level, ctx, erased, 0) case in level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) + cases (mkSortLevel SLz sinfo) in + mkSort (l, Stype level) sinfo | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, lexp_location t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) - args) in + args) sinfo in let tct = arg_loop ctx erased args in tct | Case (l, e, ret, branches, default) @@ -776,14 +776,14 @@ and check'' erased ctx e = s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = - let tlxp = mkSusp e subst in - let tltp = mkSusp etype subst in - let tlvl = mkSusp elvl subst in + let tlxp = mkSusp e subst sinfo in + let tltp = mkSusp etype subst sinfo in + let tlvl = mkSusp elvl subst sinfo in let eqty = mkCall (DB.type_eq, [(L.Aerasable, tlvl); (* Typelevel *) (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) - (L.Anormal, tlxp)]) in (* Target lexp *) + (L.Anormal, tlxp)]) sinfo in (* Target lexp *) (* The eq proof is erasable. *) let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in @@ -798,23 +798,23 @@ and check'' erased ctx e = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) + (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s sinfo)) (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) + (mkCall (mkSusp hlxp (S.shift 1) sinfo, [(ak, mkVar (vdef, 0) sinfo)]) sinfo) vdefs fieldtypes | _ -> log_tc_error ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)), - List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in + mkCall (mkCons (it, (l, name)) sinfo, + List.map (fun (_, a) -> (P.Aerasable, a)) aargs) sinfo in let (nerased, nctx, hlxp) = mkctx erased ctx s hctor vdefs fieldtypes in let subst = S.shift (List.length vdefs) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx branch (check nerased nctx branch) - (mkSusp ret (S.shift ((List.length fieldtypes) + 1)))) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) sinfo)) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -824,11 +824,11 @@ and check'' erased ctx e = 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 - let hlxp = mkVar ((l, None), 0) in + let hlxp = mkVar ((l, None), 0) sinfo in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in assert_type nctx d (check nerased nctx d) - (mkSusp ret (S.shift 2)) + (mkSusp ret (S.shift 2) sinfo) | None -> if diff > 0 then @@ -844,22 +844,22 @@ and check'' erased ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + mkCall (mkSusp t (S.shift nargs) sinfo, + indtype fargs (nargs - 1)) sinfo | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in + fieldargs ftypes) sinfo in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in + buildtype fargs) sinfo in buildtype fargs with | Not_found @@ -1010,14 +1010,14 @@ and get_type ctx e = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) sinfo)) sinfo | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in - mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) + mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) sinfo | Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in @@ -1025,18 +1025,18 @@ and get_type ctx e = let k2 = get_type nctx t2 in match sort_compose ctx nctx l ak k1 k2 with | SortResult k -> k - | _ -> mkSort (l, StypeOmega)) + | _ -> mkSort (l, StypeOmega) sinfo) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, v, t, l, get_type (DB.lctx_extend ctx v Variable t) - e)) + e) sinfo) | Call (f, args) -> let ft = get_type ctx f in List.fold_left (fun ft (_ak,arg) -> match lexp'_whnf ft ctx with | Arrow (_ak', _v, _t1, _l, t2) - -> mkSusp t2 (S.substitute arg) + -> mkSusp t2 (S.substitute arg) sinfo | _ -> ft) ft args | Inductive (l, _label, args, cases) @@ -1058,18 +1058,18 @@ and get_type ctx e = -> mkSLlub ctx level (* We need to unshift because the final type * cannot refer to the fields! *) - (mkSusp level' (L.sunshift n)) + (mkSusp level' (L.sunshift n) sinfo) | _tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) case in level) - cases (mkSortLevel SLz) in - mkSort (l, Stype level) + cases (mkSortLevel SLz sinfo) in + mkSort (l, Stype level) sinfo | (ak, v, t)::args -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) in + arg_loop args (DB.lctx_extend ctx v Variable t)) sinfo in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1081,22 +1081,22 @@ and get_type ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with | [] -> let nargs = List.length fieldtypes + List.length fargs in - mkCall (mkSusp t (S.shift nargs), - indtype fargs (nargs - 1)) + mkCall (mkSusp t (S.shift nargs) sinfo, + indtype fargs (nargs - 1)) sinfo | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) in + fieldargs ftypes) sinfo in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) in + buildtype fargs) sinfo in buildtype fargs with Not_found -> DB.type_int) | _ -> DB.type_int) @@ -1278,16 +1278,16 @@ let ctx2tup ctx nctx = * let-binding i.s.o the tuple * field (which would be both * equivalent and preferable). *) - mkSusp t (S.shift offset))) + mkSusp t (S.shift offset) sinfo)) types) - SMap.empty), - cons_label), + SMap.empty) sinfo, + cons_label) sinfo, List.mapi (fun i (oname, _t) - -> (P.Aimplicit, mkVar (oname, offset - i - 1))) - types) + -> (P.Aimplicit, mkVar (oname, offset - i - 1) sinfo)) + types) sinfo | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> mkLet (loc, [(name, mkSusp e (S.shift 1), t)], - mk_lets_and_tup blocs ((name, t) :: types)) + -> mkLet (loc, [(name, mkSusp e (S.shift 1) sinfo, t)], + mk_lets_and_tup blocs ((name, t) :: types)) sinfo | (DB.CVfix (defs, _) :: blocs) -> mkLet (loc, defs, mk_lets_and_tup blocs (List.append @@ -1295,7 +1295,7 @@ let ctx2tup ctx nctx = (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) + types)) sinfo | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []

===================================== src/sexp.ml ===================================== @@ -41,7 +41,7 @@ type token = sexp

let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location - +let dummy_sinfo : sexp list = [] (********************** Sexp tests **********************)

let pred_symbol s pred =

===================================== src/subst.ml ===================================== @@ -167,12 +167,15 @@ let cons e s = Cons (e, s, 0) let identity = Identity 0

(* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match s with | Identity o -> o = 0 | _ -> false +let identity_p s = + match s with + | Identity o -> o = 0 + | _ -> false

(* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) let compose (mkSusp : 'a -> 'a subst -> 'a) - (s1: 'a subst) (s2: 'a subst) : 'a subst = + (s1: 'a subst) (s2: 'a subst) : 'a subst = (* There is a bit of flexibility in what we return, in the sense * that some shifts can be pushed more or less down. Here we * want the shifts to float as far outside as possible. *)

===================================== src/unification.ml ===================================== @@ -135,10 +135,10 @@ let common_subset ctx s1 s2 = let o2 = o2 + o2' in (* FIXME: We should check if le1 and le2 are *unifiable* instead! *) if not (le1 = impossible || le1 = impossible) - && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) + && OL.conv_p ctx (mkSusp le1 (S.shift o1) sinfo) (mkSusp le2 (S.shift o2) sinfo) then match loop s1' s2' o1 o2 1 with | S.Identity 1 -> S.Identity o (* Optimization! *) - | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) sinfo, s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that @@ -146,11 +146,11 @@ let common_subset ctx s1 s2 = * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) | (S.Cons _, S.Identity o2') - -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) sinfo, S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) sinfo, S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -363,12 +363,12 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) "`lexp_whnf` returned an instantiated metavar!!" | (Some s_inv, MVar (sl, t, clen)) -> let clen' = clen - s_offset s in - let t' = mkSusp t s_inv in + let t' = mkSusp t s_inv sinfo in let newmv = create_metavar_1 sl t' clen' in - let lexp = mkMetavar (newmv, s, name) in + let lexp = mkMetavar (newmv, s, name) sinfo in assert (sl <= clen); assert (sl <= clen'); - assert (OL.conv_p ctx (mkSusp t' s) t); + assert (OL.conv_p ctx (mkSusp t' s sinfo) t); (* if (OL.conv_p ctx (mkSusp lexp s1) (mkSusp lexp s2)) then * print_string ("common_subset successful:\n " * ^ subst_string s

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c4bb0b8512440021e477b4e95e29fafde4...