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

Commits: c6bb08e5 by Fallismaila at 2022-03-17T17:48:53+00:00 Introduce sinfo

- - - - -

12 changed files:

- src/REPL.ml - 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/positivity.ml - src/sexp.ml - src/unification.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -136,7 +136,7 @@ let eval_interactive let ldecls, ectx' = Elab.lexp_p_decls decls [] ectx in

let lexprs = Elab.lexp_parse_all exprs ectx' in - List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) lexprs; + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr dummy_sinfo)) lexprs;

List.iter interactive#process_decls ldecls; Log.print_log ();

===================================== 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) sinfo + mkSusp p (S.shift r) dummy_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) sinfo) sinfo + mkArrow (Anormal, (dloc, None), t, dloc, t) dummy_sinfo) dummy_sinfo

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

@@ -136,11 +136,11 @@ let lmap = ref (SMap.empty : (lexp * ltype) SMap.t) let add_builtin_cst (name : string) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - let t = OL.check Myers.nil e in + let t = OL.check Myers.nil e dummy_sinfo in lmap := SMap.add name (e, t) map

let new_builtin_type name kind = - let t = mkBuiltin ((dloc, name), kind) sinfo in + let t = mkBuiltin ((dloc, name), kind) dummy_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) sinfo + mkArrow (Anormal, (dloc, None), DB.type0, dloc, DB.type0) dummy_sinfo

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

===================================== src/debruijn.ml ===================================== @@ -44,6 +44,7 @@ open Fmt

module S = Subst

+ let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"DEBRUIJN" ?print_action ?loc fmt

@@ -83,33 +84,35 @@ let fatal ?print_action ?loc fmt = * ---------------------------------- *)

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

(* easier to debug with type annotations *) @@ -293,7 +296,7 @@ let print_lexp_ctx_n (ctx : lexp_context) (ranges : (int * int) list) = (match lexp with | None -> print_string "<var>" | Some lexp - -> (let str = lexp_str (!debug_ppctx) lexp in + -> (let str = lexp_str (!debug_ppctx) lexp dummy_sinfo in let strs = match String.split_on_char '\n' str with | hd :: tl -> print_string hd; tl @@ -380,12 +383,12 @@ 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)) sinfo + mkSusp t (S.shift (i + 1)) dummy_sinfo

let lctx_lookup_value (ctx : lexp_context) (vref : vref) : lexp option = let (_, i) = vref in match lctx_lookup ctx vref with - | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o)) dummy_sinfo) | _ -> None

let env_lookup_type ctx (v : vref): lexp =

===================================== 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) sinfo); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form) dummy_sinfo); special_forms := SMap.add name func (!special_forms)

let get_special_form name = @@ -141,7 +141,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = -> lexp_error l ltp {|Type of "%s" is not a proper type: %s|} name tystr

let elab_check_proper_type (ctx : elab_context) ltp var = - try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp dummy_sinfo) var ltp with e -> match e with | Log.Stop_compilation _ -> raise e | _ @@ -161,7 +161,7 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in

- let ltype' = try OL.check lctx lxp + let ltype' = try OL.check lctx lxp dummy_sinfo with e -> match e with | Log.Stop_compilation _ -> raise e | _ -> @@ -210,13 +210,13 @@ let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, _lxp, ltp) -> elab_check_proper_type - nctx (push_susp ltp (S.shift n)) var; + nctx (push_susp ltp (S.shift n) dummy_sinfo) var; n - 1) (List.length decls) decls in let _ = List.fold_left (fun n (var, lxp, ltp) -> elab_check_def nctx var lxp - (push_susp ltp (S.shift n)); + (push_susp ltp (S.shift n) dummy_sinfo); n - 1) (List.length decls) decls in @@ -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) sinfo + mkMetavar (meta, S.identity, name) dummy_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)) sinfo) + (mkSort (loc, Stype (newMetalevel ctx sl loc)) dummy_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) sinfo in + let lxp = mkVar (id, idx) dummy_sinfo in let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp) with Senv_Lookup_Fail xs -> @@ -317,7 +317,7 @@ let elab_varref ctx (loc, name) (* Turn metavar into plain vars after generalization. * ids: an IMap that maps metavars to their position as argument * (first arg gets position 0). *) -let meta_to_var ids (e : lexp) = +let meta_to_var ids (e : lexp) sinfo =

let count = IMap.cardinal ids in

@@ -429,7 +429,7 @@ let meta_to_var ids (e : lexp) = | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (n,i) -> if i < o then e else mkVar (n, i + count) sinfo - | Susp (e, s) -> loop o (push_susp e s) + | Susp (e, s) -> loop o (push_susp e s dummy_sinfo) | Let (l, defs, e) -> let len = List.length defs in let (_, ndefs) @@ -481,7 +481,7 @@ let meta_to_var ids (e : lexp) = -> if IMap.mem id ids then mkVar (name, o + count - IMap.find id ids) sinfo else match metavar_lookup id with - | MVal e -> loop o (push_susp e s) + | MVal e -> loop o (push_susp e s dummy_sinfo) | _ -> mkMetavar (id, adjust_subst o s, name) sinfo in loop 0 e

@@ -503,7 +503,7 @@ let sort_generalized_metavars sl cl ctx mfvs = then acc else (assert (cl' >= cl); let mt = if cl' > cl then - Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) + Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) dummy_sinfo else mt in let mv = (id, vname, mt) in if (OL.conv_p ctx mt type_level) then @@ -536,9 +536,9 @@ let generalize (nctx : elab_context) e = assert (n = IMap.cardinal ids); match mfvs with | [] -> assert (n = len); - meta_to_var ids e + meta_to_var ids e dummy_sinfo | ((id, vname, mt) :: mfvs) - -> let mt' = meta_to_var ids mt in + -> let mt' = meta_to_var ids mt dummy_sinfo in let n = n + 1 in let e' = loop (IMap.add id n ids) n mfvs in wrap (IMap.mem id nes) vname mt' l e' in @@ -621,11 +621,11 @@ and instantiate_implicit e t ctx = 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) sinfo) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args) sinfo, t) + instantiate (mkSusp t2 (S.substitute arg) dummy_sinfo) ((ak, arg)::args) + | _ -> (mkCall (e, List.rev args) dummy_sinfo, t) in instantiate t []

-and infer_type pexp ectx var = +and infer_type pexp ectx var sinfo = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -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) sinfo) + List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) dummy_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) sinfo in + let arrow = mkArrow (kind, var, arg, l, body) dummy_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 sinfo) in + name (mkSusp t s dummy_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) sinfo); + ltarget := check_inferred ctx tlxp tltp (mkCall (it', args) dummy_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))) sinfo in + - M.length (ectx_to_lctx ctx))) dummy_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')]) sinfo (* Target lexp *) + (Anormal, tlxp')]) dummy_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) sinfo in + let head_lexp = mkVar (v, 0) dummy_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) sinfo + mkSusp body (S.substitute arg) dummy_sinfo | _e -> lxp in match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) @@ -861,16 +861,16 @@ 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 sinfo) in - make_nctx nctx (ssink var s) pargs cargs + let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in + make_nctx nctx (ssink dummy_sinfo var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) | ((ef, var)::pargs, (ak, _, fty)::cargs) when (match (ef, ak) with | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) - -> let nctx = ctx_extend ctx var Variable (mkSusp fty s sinfo) in - make_nctx nctx (ssink var s) pargs cargs pe + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in + make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe ((ak, var)::acc) | ((Some (l, fname), var)::pargs, cargs) -> if SMap.mem fname pe then @@ -878,23 +878,23 @@ 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 sinfo) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s dummy_sinfo) in if ak = Anormal then sexp_error loc {|Missing pattern for normal field%s|} (match fname with | (_, Some n) -> sprintf {| "%s"|} n | _ -> ""); - make_nctx nctx (ssink var s) pargs cargs pe + make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe ((ak, var)::acc) in 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) sinfo) in + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs) dummy_sinfo) in let head_lexp_args = List.mapi (fun i (ak, vname) -> - (ak, mkVar (vname, List.length fargs - i - 1) sinfo)) fargs in - let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) sinfo in + (ak, mkVar (vname, List.length fargs - i - 1) dummy_sinfo)) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) dummy_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 @@ -908,7 +908,7 @@ and check_case rtype (loc, target, ppatterns) ctx = match pat with | Ppatsym ((_, None) as var) -> add_default var | Ppatsym ((l, Some name) as var) - -> if Eval.constructor_p name ctx then + -> if Eval.constructor_p name ctx dummy_sinfo then add_branch (Symbol (l, name)) [] else add_default var (* A named default branch. *)

@@ -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) sinfo + mkCase (loc, tlxp, rtype, lpattern, dflt) dummy_sinfo

and elab_macro_call ctx func args ot = let t @@ -926,7 +926,7 @@ and elab_macro_call ctx func args ot = (lexp_location func) | Some t -> t in let sxp = match lexp_expand_macro (lexp_location func) - func args ctx (Some t) with + func args ctx (Some t) dummy_sinfo with | Vcommand cmd -> (match cmd () with | Vsexp (sxp) -> sxp @@ -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) sinfo) + (L.mkSusp ret_type (S.substitute larg) dummy_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) sinfo) + (L.mkSusp ret_type (S.substitute larg) dummy_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) sinfo) + (L.mkSusp ret_type (S.substitute larg) dummy_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) sinfo) in + (L.mkSusp ret_type (S.substitute larg) dummy_sinfo) in

let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs) sinfo, Inferred ret_type) + (mkCall (func, List.rev largs) dummy_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) sinfo) + -> mkArrow (ak, n, t, dummy_location, aa) dummy_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) sinfo) + -> mkArrow (Aerasable, vname, t, l, e) dummy_sinfo) altacc in if altacc' == altacc then acc (* No generalization! *) @@ -1038,7 +1038,7 @@ and lexp_parse_inductive ctors ctx = | _ -> assert (e = impossible); [] in loop altacc' | (kind, var, exp)::tl - -> let lxp = infer_type exp ctx var in + -> let lxp = infer_type exp ctx var dummy_sinfo in let nctx = ectx_extend ctx var Variable lxp in loop tl ((kind, var, lxp)::acc) nctx in loop args [] nctx in @@ -1089,16 +1089,16 @@ and lexp_eval ectx e = "Exception happened during evaluation:"; raise exc

-and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) +and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) sinfo : value_type =

(* Build the function to be called *) let macro_expand = BI.get_predef "Macro_expand" ctx in (* FIXME: Rather than remember the lexp of "expand_macro" in predef, * we should remember its value so we don't have to re-eval it everytime. *) - let macro_expand = lexp_eval ctx macro_expand in + let macro_expand = lexp_eval ctx macro_expand sinfo in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let macro = lexp_eval ctx macro_funct in + let macro = lexp_eval ctx macro_funct sinfo in let args = [macro; BI.o2v_list sargs] in

(* FIXME: Make a proper `Var`. *) @@ -1113,10 +1113,10 @@ and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) * | e -> sexp_print e; print_string "\n" *)

and lexp_decls_macro (loc, mname) sargs ctx: sexp = - try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in + try let lxp, _ltp = infer (Symbol (loc, mname)) ctx in

(* FIXME: Check that (conv_p ltp Macro)! *) - let ret = lexp_expand_macro loc lxp sargs ctx None in + let ret = lexp_expand_macro loc lxp sargs ctx None dummy_sinfo in match ret with | Vcommand cmd -> (match cmd () with @@ -1149,14 +1149,14 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) assert (i < List.length defs); match Myers.nth i (ectx_to_lctx nctx) with | (_v', ForwardRef, t) - -> let adjusted_t = push_susp t (S.shift (i + 1)) in + -> let adjusted_t = push_susp t (S.shift (i + 1)) dummy_sinfo in (* We elab `sexp` within the original `nctx`, i.e. * the context where the other vars don't have * a definition yet. This is because we can't yet * build the proper `nctx`: a partially filled * mutually-recursive block would not have the * proper format, e.g. for `lctx_view`! *) - let e = check sexp adjusted_t nctx in + let e = check sexp adjusted_t nctx in (* let d = (v', LetDef (i + 1, e), t) in *) (IMap.add i ((l, Some vname), e, t) map) | _ -> Log.internal_error "Defining same slot!") @@ -1164,9 +1164,9 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls

-and infer_and_generalize_type (ctx : elab_context) se name = +and infer_and_generalize_type (ctx : elab_context) se name sinfo = let nctx = ectx_new_scope ctx in - let t = infer_type se nctx name in + let t = infer_type se nctx name sinfo in (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those @@ -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) sinfo) + vname, t, e) dummy_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) sinfo) + name, t, sexp_location se, e) dummy_sinfo) t in (e', t')

@@ -1255,13 +1255,13 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) dummy_sinfo in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in (* Take the previous type annotation. *) let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) dummy_sinfo | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with @@ -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) sinfo, ltp)], sdecls, toks, + [(var, mkSusp lexp (S.shift 1) dummy_sinfo, ltp)], sdecls, toks, ctx_define nctx var lexp ltp

| [Symbol (loc, vname); sexp] @@ -1408,8 +1408,8 @@ let sform_built_in ctx loc sargs ot = * 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' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in - let bi = mkBuiltin ((loc, name), ltp') sinfo in + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) dummy_sinfo in + let bi = mkBuiltin ((loc, name), ltp') dummy_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) sinfo, Lazy) + (mkCons (idt, sym) dummy_sinfo, Lazy)

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

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

let sform_hastype ctx loc sargs _ot = match sargs with - | [se; st] -> let lt = infer_type st ctx (loc, None) in - let le = check se lt ctx in + | [se; st] -> let lt = infer_type st ctx (loc, None) dummy_sinfo in + let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; sform_dummy_ret ctx loc @@ -1515,18 +1515,18 @@ let sform_arrow kind ctx loc sargs _ot = -> let (v, st1) = match st1 with | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) | _ -> ((sexp_location st1, None), st1) in - let lt1 = infer_type st1 ctx v in + let lt1 = infer_type st1 ctx v dummy_sinfo 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) sinfo, Lazy) + let lt2 = infer_type st2 nctx (sexp_location st2, None) dummy_sinfo in + (mkArrow (kind, v, lt1, loc, lt2) dummy_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) 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 + | [(String _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se) dummy_sinfo, Inferred DB.type_int + | [(Float _) as se] -> mkImm (se) dummy_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)) sinfo, Lazy) + (mkMetavar (idx, subst, (loc, Some name)) dummy_sinfo, Lazy) else (* FIXME: The variable is from another scope_level! It means that `subst` is not the right substitution for @@ -1592,7 +1592,7 @@ let sform_identifier ctx loc sargs ot = | None -> newMetatype octx sl loc | Some t (* `t` is defined in ctx instead of octx. *) - -> Inverse_subst.apply_inv_subst t subst in + -> Inverse_subst.apply_inv_subst t subst dummy_sinfo in let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then let idx = @@ -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 sinfo, + (mkSusp mv subst dummy_sinfo, match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *) @@ -1625,7 +1625,7 @@ let rec sform_lambda kind ctx loc sargs ot = ((dummy_location, None), None) in

let olt1 = match ost1 with - | Some st -> Some (infer_type st ctx arg) + | Some st -> Some (infer_type st ctx arg dummy_sinfo) | _ -> None in

let mklam lt1 olt2 = @@ -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) sinfo, + (mkLambda (kind, arg, lt1, lbody) dummy_sinfo, match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) sinfo) + | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) dummy_sinfo) | _ -> alt) in

(match ot with @@ -1672,9 +1672,9 @@ 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) sinfo, + (mkLambda (ak2, v, lt1, lam) dummy_sinfo, match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') sinfo) + | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') dummy_sinfo) | _ -> alt)

| _lt @@ -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) sinfo) ot in + let ot = Option.map (fun t -> mkSusp t (S.shift off) dummy_sinfo) ot in let bdy, ot = elaborate nctx sbody ot in let ot = match ot with - | Inferred t -> Inferred (mkSusp t s sinfo) + | Inferred t -> Inferred (mkSusp t s dummy_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 sinfo + | Symbol (_, "z") -> mkSortLevel SLz dummy_sinfo | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) - -> mkSortLevel (SLsucc (infer_level ctx se)) sinfo + -> mkSortLevel (SLsucc (infer_level ctx se)) dummy_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) sinfo, - Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) sinfo)) sinfo)) + (mkSort (loc, Stype l) dummy_sinfo, + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) dummy_sinfo)) dummy_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) sinfo in (lxp, Lazy) + let lxp = mkVar ((loc, None), i) dummy_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)) sinfo) in + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len)) dummy_sinfo) in

(tuple',Lazy)

@@ -1890,7 +1890,7 @@ let default_ectx let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in - let v = mkVar ((dloc, Some name), idx) sinfo in + let v = mkVar ((dloc, Some name), idx) dummy_sinfo in BI.set_predef name v) BI.predef_names; with Senv_Lookup_Fail _ -> warning "Predef not found"; in @@ -1939,7 +1939,7 @@ let lexp_expr_str str ctx = let source = new Source.source_string str in let pxps = sexp_parse_source source tenv grm limit in let lexps = lexp_parse_all pxps ctx in - List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp dummy_sinfo)) lexps; lexps

===================================== src/eval.ml ===================================== @@ -421,7 +421,7 @@ let file_write loc _depth args_val = match args_val with ) "File.write expects an out_channel and a string. Actual arguments:"

-let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = +let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) sinfo : (value_type) =

let trace = append_eval_trace trace lxp in let eval' lxp ctx = eval lxp ctx trace in @@ -455,13 +455,13 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) (* ---------------- *) | Let(_, decls, inst) -> let nctx = eval_decls decls ctx trace in - eval' inst nctx + eval' inst nctx sinfo

(* Function call *) | Call (f, args) -> eval_call (elexp_location f) f trace - (eval f ctx trace) - (List.map (fun e -> eval e ctx trace) args) + (eval f ctx trace sinfo) + (List.map (fun e -> eval e ctx trace sinfo) args)

(* Case *) | Case (loc, target, pat, dflt) @@ -510,8 +510,8 @@ and eval_call loc unef i f args = -> bindargs e vs (add_rte_variable x v ctx) | ([], _) -> let trace = append_typer_trace i unef in - eval e ctx trace - | _ -> eval_call loc unef i (eval e ctx i) vs in + eval e ctx trace dummy_sinfo + | _ -> eval_call loc unef i (eval e ctx i dummy_sinfo) vs in bindargs e vs (add_rte_variable x v ctx)

| Vbuiltin (name), args @@ -553,12 +553,12 @@ 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) sinfo)]) sinfo) + -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) dummy_sinfo)]) dummy_sinfo) | _ -> fatal loc "Trying to call a non-function!\n%s" (trace_value f)

and eval_case ctx i loc target pat dflt = (* Eval target *) - let v = eval target ctx i in + let v = eval target ctx i dummy_sinfo in

(* extract constructor name and arguments *) let ctor_name, args = match v with @@ -586,17 +586,17 @@ and eval_case ctx i loc target pat dflt = | [], [] -> nctx in

let nctx = fold2 ctx pat_args args in - eval exp nctx i + eval exp nctx i dummy_sinfo

(* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> eval lxp (add_rte_variable var v ctx) i + -> eval lxp (add_rte_variable var v ctx) i dummy_sinfo | _ -> error loc "Match Failure")

and build_arg_list args ctx i = (* eval every args *) - let arg_val = List.map (fun (_k, e) -> eval e ctx i) args in + let arg_val = List.map (fun (_k, e) -> eval e ctx i dummy_sinfo) args in

(* Add args inside context *) List.fold_left (fun c v -> add_rte_variable vdummy v c) ctx arg_val @@ -611,7 +611,7 @@ and eval_decls (decls: (vname * elexp) list) add_rte_variable name Vundefined ctx) ctx decls in

List.iteri (fun idx (name, lxp) -> - let v = eval lxp nctx i in + let v = eval lxp nctx i dummy_sinfo in let offset = n - idx in ignore (set_rte_variable offset name v nctx)) decls;

@@ -798,7 +798,7 @@ let is_bound loc _depth args_val = match args_val with with Senv_Lookup_Fail _ -> false) | _ -> error loc "Elab.isbound takes an Elab_Context and a String as arguments"

-let constructor_p name ectx = +let constructor_p name ectx sinfo = try let idx = senv_lookup name ectx in (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor @@ -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) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_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) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx) dummy_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) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_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) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_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 @@ -887,7 +887,7 @@ let ctor_arg_pos name arg ectx = with Senv_Lookup_Fail _ -> (-1)

let is_constructor loc _depth args_val = match args_val with - | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) + | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx dummy_sinfo) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"

let is_nth_erasable loc _depth args_val = match args_val with @@ -1151,7 +1151,7 @@ let from_lctx (lctx: lexp_context): runtime_env = ref (match def with | LetDef (_, e) -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx + eval (OL.erase_type lctx e) rctx dummy_sinfo else Vundefined | _ -> Vundefined)) rctx @@ -1173,7 +1173,7 @@ let from_lctx (lctx: lexp_context): runtime_env = * are present! *) let lctx' = DB.lctx_extend_rec lctx defs in if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx dummy_sinfo) evs else () in nrctx and from_lctx lctx = @@ -1201,7 +1201,7 @@ class ast_interpreter lctx = object

method eval_expr lexp = let elexp = Opslexp.erase_type lctx lexp in - debug_eval elexp rctx + debug_eval elexp rctx dummy_sinfo

method print_rte_ctx = Env.print_rte_ctx rctx

===================================== 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) sinfo -let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) sinfo +let type_datacons_label = mkBuiltin ((dloc, "DataconsLabel"), type0) dummy_sinfo +let type_heap = mkBuiltin ((dloc, "Heap"), type_arrow_0) dummy_sinfo

let next_free_address : addr ref = ref 1

===================================== src/inverse_subst.ml ===================================== @@ -56,7 +56,7 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: subst) : substIR option = +let transfo (s: subst) : substIR option = let rec transfo (s: subst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) @@ -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) sinfo) (* Helper : shift the index of a var *) + indexOf (mkSusp var (S.shift offset) dummy_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) sinfo + mkVar ((U.dummy_location, None), idx) dummy_sinfo

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -242,7 +242,7 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with | S.Cons (e, s', o) -> let s = shift_inv_subst o s in (* FIXME: Why don't we ever return a Shift? *) - S.cons (apply_inv_subst e s) (compose_inv_subst s' s) + S.cons (apply_inv_subst e s dummy_sinfo) (compose_inv_subst s' s) | S.Identity o -> (match inverse (shift_inv_subst o s) with | Some s -> s (* FIXME: could also be Ambiguous, depending on `s`. *) @@ -252,66 +252,66 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * The function presumes that `invertible s` was true. * This can be used like mkSusp/push_susp, but it's not lazy. * This is because it can signal errors Not_invertible or Ambiguous. *) -and apply_inv_subst (e : lexp) (s : subst) : lexp = +and apply_inv_subst (e : lexp) (s : subst) sinfo : lexp = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s dummy_sinfo)) sinfo | SortLevel (SLlub (e1, e2)) (* FIXME: use mkSLlub? *) - -> 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 + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s dummy_sinfo, apply_inv_subst e2 s dummy_sinfo)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s dummy_sinfo)) sinfo | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) sinfo - | Susp (e, s') -> apply_inv_subst (push_susp e s') s + | Susp (e, s') -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink dummy_sinfo v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink v s, - (v, apply_inv_subst def s', apply_inv_subst ty s) + -> (ssink dummy_sinfo v s, + (v, apply_inv_subst def s' dummy_sinfo, apply_inv_subst ty s dummy_sinfo) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, apply_inv_subst e s') sinfo + mkLet (l, ndefs, apply_inv_subst e s' dummy_sinfo) sinfo | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s, l, - apply_inv_subst t2 (ssink v s)) sinfo + -> mkArrow (ak, v, apply_inv_subst t1 s dummy_sinfo, l, + apply_inv_subst t2 (ssink dummy_sinfo v s) dummy_sinfo) sinfo | Lambda (ak, v, t, e) - -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) sinfo + -> mkLambda (ak, v, apply_inv_subst t s dummy_sinfo, apply_inv_subst e (ssink dummy_sinfo v s) dummy_sinfo) sinfo | Call (f, args) - -> mkCall (apply_inv_subst f s, - L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) sinfo + -> mkCall (apply_inv_subst f s dummy_sinfo, + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s dummy_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, apply_inv_subst t s) :: nargs)) + -> (ssink dummy_sinfo v s, (ak, v, apply_inv_subst t s dummy_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, apply_inv_subst t s) + -> (ssink dummy_sinfo v s, + (ak, v, apply_inv_subst t s dummy_sinfo) :: nargs)) (s, []) args in L.rev ncase) cases in mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (apply_inv_subst it s, name) sinfo + | Cons (it, name) -> mkCons (apply_inv_subst it s dummy_sinfo, name) sinfo | Case (l, e, ret, cases, default) - -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, + -> mkCase (l, apply_inv_subst e s dummy_sinfo, apply_inv_subst ret s dummy_sinfo, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink ov s) + (fun s (_,ov) -> ssink dummy_sinfo ov s) s cargs in - let s'' = ssink (l, None) s' in - (l, cargs, apply_inv_subst e s'')) + let s'' = ssink dummy_sinfo (l, None) s' in + (l, cargs, apply_inv_subst e s'' dummy_sinfo )) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)))) sinfo + | Some (v,e) -> Some (v, apply_inv_subst e (ssink dummy_sinfo (l, None) (ssink dummy_sinfo v s)) dummy_sinfo)) sinfo | Metavar (id, s', name) -> match metavar_lookup id with - | MVal e -> apply_inv_subst (push_susp e s') s + | MVal e -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) sinfo

===================================== src/lexp.ml ===================================== @@ -36,12 +36,14 @@ module S = Subst type vname = U.vname type vref = U.vref type meta_id = int (* Identifier of a meta variable. *) +type sinfo = sexp list

type label = symbol

include Pexp.ArgKind

-let sinfo: (sexp list) = [] + +let dummy_sinfo : sexp list = []

(*************** Elaboration to Lexp *********************)

@@ -61,7 +63,7 @@ let sinfo: (sexp list) = [] 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 * sexp list + and lexp = lexp' * int * sinfo and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level @@ -324,7 +326,7 @@ let mkCall (f, es) sinfo = | _, [] -> f | _ -> hc (Call (f, es)) sinfo

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

let lexp_head e = match lexp_lexp' e with @@ -449,21 +451,22 @@ let rec mkSusp e s sinfo = match lexp_lexp' e with | 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) sinfo + | Susp (e, s') -> mkSusp_memo e (scompose s' s ) + | Var (l, v) -> slookup s l v sinfo + | 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 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) sinfo) - (fun e o -> mkSusp e (S.shift o) sinfo) + else let res = mkSusp e s [] in + Hashtbl.add hcs_table (e, s) res; + res + +and scompose s1 s2 = S.compose mkSusp_memo s1 s2 +and slookup s l v sinfo = 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) sinfo) +let ssink sinfo = 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. @@ -472,7 +475,7 @@ let ssink = S.sink (fun l i -> mkVar (l, i) sinfo) * 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) sinfo) (S.shift 1)) sinfo +let srename name le = mkSusp le (S.cons (mkVar (name, 0) dummy_sinfo) (S.shift 1)) dummy_sinfo

(* Shift by a negative amount! *) let rec sunshift n = @@ -534,11 +537,11 @@ let vdummy = (U.dummy_location, None) let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l,n) = (l, maybename n)

-let rec push_susp e s = (* Push a suspension one level down. *) +let rec push_susp e s sinfo = (* Push a suspension one level down. *) match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (mkSusp e1 s sinfo, mkSusp e2 s sinfo)) sinfo | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s sinfo)) sinfo @@ -546,26 +549,26 @@ let rec push_susp e s = (* Push a suspension one level down. *) | Builtin _ -> e

| Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in let rec loop s defs = match defs with | [] -> [] | (v, def, ty) :: defs - -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink v s) defs in + -> (v, mkSusp def s' sinfo, mkSusp ty s sinfo) :: loop (ssink sinfo 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 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 + -> mkArrow (ak, v, mkSusp t1 s sinfo, l, mkSusp t2 (ssink sinfo v s) sinfo) sinfo + | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s sinfo, mkSusp e (ssink sinfo 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 sinfo) :: nargs)) + -> (ssink sinfo 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, + -> (ssink sinfo v s, (ak, v, mkSusp t s sinfo) :: nargs)) (s, []) args in @@ -577,30 +580,30 @@ let rec push_susp e s = (* Push a suspension one level down. *) -> 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) + (fun s (_,ov) -> ssink sinfo ov s) s cargs in - (l, cargs, mkSusp e (ssink (l, None) s') sinfo)) + (l, cargs, mkSusp e (ssink sinfo (l, None) s') sinfo)) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)) sinfo)) sinfo + | Some (v,e) -> Some (v, mkSusp e (ssink sinfo (l, None) (ssink sinfo 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 * rather than Susp. * 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) + | Susp (e,s') -> push_susp e (scompose s' s) sinfo | (Var _ | Metavar _) -> nosusp (mkSusp e s sinfo)

-and nosusp e = (* Return `e` with no outermost `Susp`. *) +and nosusp (e: lexp ) = (* Return `e` with no outermost `Susp`. *) match lexp_lexp' e with - | Susp(e, s) -> push_susp e s + | Susp(e, s) -> push_susp e s dummy_sinfo | _ -> e

(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) -let clean e = +let clean e sinfo = let rec clean s e = match lexp_lexp' e with | Imm _ -> e @@ -613,26 +616,26 @@ let clean e = | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink v s, + -> (ssink sinfo v s, (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in 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) sinfo - | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) sinfo + -> mkArrow (ak, v, clean s t1, l, clean (ssink sinfo v s) t2) sinfo + | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink sinfo v s) e) sinfo | Call (f, args) -> mkCall (clean s f, 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)) + -> (ssink sinfo v s, (ak, v, clean s t) :: 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, + -> (ssink sinfo v s, (ak, v, clean s t) :: nargs)) (s, []) args in @@ -644,14 +647,14 @@ let clean e = -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink ov s) + (fun s (_,ov) -> ssink sinfo ov s) s cargs in - let s'' = ssink (l, None) s' in + let s'' = ssink sinfo (l, None) s' in (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) sinfo + | Some (v,e) -> Some (v, clean (ssink sinfo (l, None) (ssink sinfo 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 sinfo) @@ -666,9 +669,9 @@ let sdatacons = Symbol (U.dummy_location, "##datacons") let stypecons = Symbol (U.dummy_location, "##typecons")

(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) -let rec lexp_unparse lxp = +let rec lexp_unparse lxp = match lexp_lexp' lxp with - | Susp _ -> lexp_unparse (nosusp lxp) + | Susp _ -> lexp_unparse (nosusp lxp ) | Imm (sexp) -> sexp | Builtin ((l,name), _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) @@ -684,33 +687,33 @@ let rec lexp_unparse lxp = | Aimplicit -> "lambda_=>_" | Aerasable -> "lambda_≡>_"), [Node (Symbol (l, "_:_"), [Symbol (sname vdef); st]); - lexp_unparse body]) + lexp_unparse body ]) | Arrow (arg_kind, (l,oname), ltp1, loc, ltp2) - -> let ut1 = lexp_unparse ltp1 in + -> let ut1 = lexp_unparse ltp1 in Node (Symbol (loc, match arg_kind with Anormal -> "_->_" | Aimplicit -> "_=>_" | Aerasable -> "_≡>_"), [(match oname with None -> ut1 | Some v -> Node (Symbol (l, "_:_"), [Symbol (l,v); ut1])); - lexp_unparse ltp2]) + lexp_unparse ltp2 ])

| Let (loc, ldecls, body) -> (* (vdef * lexp * ltype) list *) let sdecls = List.fold_left (fun acc (vdef, lxp, ltp) -> Node (Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse ltp]) + [Symbol (sname vdef); lexp_unparse ltp ]) :: Node (Symbol (U.dummy_location, "_=_"), - [Symbol (sname vdef); lexp_unparse lxp]) + [Symbol (sname vdef); lexp_unparse lxp ]) :: acc) [] ldecls in Node (Symbol (loc, "let_in_"), [Node (Symbol (U.dummy_location, "_;_"), sdecls); - lexp_unparse body]) + lexp_unparse body ])

| Call(lxp, largs) -> (* (arg_kind * lexp) list *) - let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem) largs in + let sargs = List.map (fun (_kind, elem) -> lexp_unparse elem ) largs in Node (lexp_unparse lxp, sargs)

| Inductive(loc, label, lfargs, ctors) -> @@ -734,12 +737,12 @@ let rec lexp_unparse lxp = | Anormal -> "_:_" | Aimplicit -> "_::_" | Aerasable -> "_:::_"), - [Symbol id; lexp_unparse t])) + [Symbol id; lexp_unparse t ])) types)) (SMap.bindings ctors))

| Case (loc, target, bltp, branches, default) -> - let bt = lexp_unparse bltp in + let bt = lexp_unparse bltp in let pbranch = List.map (fun (str, (loc, args, bch)) -> match args with | [] -> Ppatsym (loc, Some str), lexp_unparse bch @@ -755,14 +758,14 @@ let rec lexp_unparse lxp = in (Ppatcons (Node (sdatacons, [bt; Symbol (loc, str)]), pat_args), - lexp_unparse bch) + lexp_unparse bch ) ) (SMap.bindings branches) in

let pbranch = match default with | Some (v,dft) -> (Ppatsym v, - lexp_unparse dft)::pbranch + lexp_unparse dft )::pbranch | None -> pbranch - in let e = lexp_unparse target in + in let e = lexp_unparse target in Node (Symbol (loc, "case_"), e :: List.map (fun (pat, branch) -> @@ -781,15 +784,15 @@ let rec lexp_unparse lxp = [lexp_unparse l]) | SortLevel (SLlub (l1, l2)) -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), - [lexp_unparse l1; lexp_unparse l2]) + [lexp_unparse l1 ; lexp_unparse l2 ]) | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") | Sort (_l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), - [lexp_unparse sl]) + [lexp_unparse sl ])

(* FIXME: ¡Unify lexp_print and lexp_string! *) -and lexp_string lxp = sexp_string (lexp_unparse lxp) +and lexp_string lxp = sexp_string (lexp_unparse lxp )

and subst_string s = match s with | S.Identity o -> "↑" ^ string_of_int o @@ -797,7 +800,7 @@ and subst_string s = match s with | S.Cons (l, s, o) -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"

-and lexp_name e = +and lexp_name e = match lexp_lexp' e with | Imm _ -> lexp_string e | Var _ -> lexp_string e @@ -905,19 +908,19 @@ let rec get_precedence expr ctx = (* Printing Functions * ========================================== *)

-let rec lexp_print e = print_string (lexp_string e) -and lexp_string e = lexp_cstring (!debug_ppctx) e +let rec lexp_print e = print_string (lexp_string e ) +and lexp_string e = lexp_cstring (!debug_ppctx) e

(* Context Print *) -and lexp_cprint ctx e = print_string (lexp_cstring ctx e) -and lexp_cstring ctx e = lexp_str ctx e +and lexp_cprint ctx e = print_string (lexp_cstring ctx e ) +and lexp_cstring ctx e = lexp_str ctx e dummy_sinfo

(* Implementation *) -and lexp_str ctx (exp : lexp) : string = +and lexp_str ctx (exp : lexp) sinfo : string =

- let inter_ctx = add_indent ctx 1 in - let lexp_str' = lexp_str ctx in - let lexp_stri idt e = lexp_str (add_indent ctx idt) e in + let inter_ctx = add_indent ctx 1 in + let lexp_str' sinfo = lexp_str ctx sinfo in + let lexp_stri idt e sinfo = lexp_str (add_indent ctx idt) e sinfo in

let pretty = pp_pretty ctx in let color = pp_color ctx in @@ -971,15 +974,15 @@ and lexp_str ctx (exp : lexp) : string = | Float (_, s) -> tval (string_of_float s) | e -> sexp_string e)

- | Susp (e, s) -> lexp_str ctx (push_susp e s) + | Susp (e, s) -> lexp_str ctx (push_susp e s sinfo) sinfo

| Var ((_loc, name), idx) -> maybename name ^ (index idx) ;

| Metavar (idx, subst, (_loc, name)) (* print metavar result if any *) -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx (push_susp e subst) - | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + | MVal e -> lexp_str ctx (push_susp e subst sinfo) sinfo + | _ -> "?" ^ maybename name ^ (subst_string subst ) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *) @@ -998,35 +1001,35 @@ and lexp_str ctx (exp : lexp) : string = else decls in

(keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ - (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) + (make_indent idt_lvl) ^ (lexp_stri idt_lvl body sinfo)

| Arrow(k, (_, Some name), tp, _loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str' expr) + "(" ^ name ^ " : " ^ (lexp_str' tp sinfo) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str' expr sinfo)

| Arrow(k, (_, None), tp, _loc, expr) -> - "(" ^ (lexp_str' tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" + "(" ^ (lexp_str' tp sinfo) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str' expr sinfo) ^ ")"

| Lambda(k, (_loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype sinfo) ^ ")" in

(keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ - (make_indent 1) ^ (lexp_stri 1 lbody) + (make_indent 1) ^ (lexp_stri 1 lbody sinfo)

| Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name + (keyword "datacons ") ^ (lexp_str' t sinfo) ^ " " ^ ctor_name

| Call(fname, args) -> let name, idx = get_name fname in let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in + "(" ^ (lexp_str' lhs sinfo) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs sinfo) ^ ")" in

let print_arg str (arg_type, lxp) = match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) - | Anormal -> str ^ " " ^ (lexp_str' lxp) + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp sinfo) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp sinfo) + | Anormal -> str ^ " " ^ (lexp_str' lxp sinfo) | _ -> str in (

match args with @@ -1034,7 +1037,7 @@ and lexp_str ctx (exp : lexp) : string = binop_str (" " ^ (get_binary_op_name name)) lhs rhs

| _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str' fname) ^ args ^ ")") + "(" ^ (lexp_str' fname sinfo) ^ args ^ ")")

| Inductive (_, (_, name), [], ctors) -> (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ @@ -1045,14 +1048,14 @@ and lexp_str ctx (exp : lexp) : string = = List.fold_left (fun str (arg_kind, (_, name), ltype) -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") + ^ (lexp_str' ltype sinfo) ^ ")") "" args in

(keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ - (lexp_str_ctor ctx ctors) + (lexp_str_ctor ctx ctors )

| Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str' target) in + let str = (keyword "case ") ^ (lexp_str' target sinfo) in let arg_str arg = List.fold_left (fun str v -> match v with @@ -1062,7 +1065,7 @@ and lexp_str ctx (exp : lexp) : string =

let str = SMap.fold (fun k (_, arg, exp) str -> str ^ nl ^ (make_indent 1) ^ - "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp)) + "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp sinfo)) map str in

match dflt with @@ -1071,7 +1074,7 @@ and lexp_str ctx (exp : lexp) : string = str ^ nl ^ (make_indent 1) ^ "| " ^ (match v with (_, None) -> "_" | (_, Some name) -> name) - ^ " => " ^ (lexp_stri 1 df)) + ^ " => " ^ (lexp_stri 1 df sinfo))

| Builtin ((_, name), _) -> "##" ^ name

@@ -1079,9 +1082,9 @@ and lexp_str ctx (exp : lexp) : string = | Sort (_, StypeOmega) -> "##Type_ω"

| SortLevel (SLz) -> "##TypeLevel.z" - | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" + | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" | SortLevel (SLlub (e1, e2)) - -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")" + -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"

| Sort (_, Stype l) -> match lexp_lexp' l with @@ -1100,7 +1103,7 @@ and lexp_str_ctor ctx ctors = SMap.fold (fun key value str -> let str = str ^ newline ^ (make_indent 1) ^ "(" ^ key in let str = List.fold_left (fun str (_k, _, arg) - -> str ^ " " ^ (lexp_str ctx arg)) + -> str ^ " " ^ (lexp_str ctx arg dummy_sinfo)) str value in str ^ ")") ctors "" @@ -1111,87 +1114,87 @@ and lexp_str_decls ctx decls = let sepdecl = (if pp_decl ctx then "\n" else "") in

let type_str name lxp = (if pp_type ctx then ( - name ^ " : " ^ (lexp_str' lxp) ^ ";") else "") in + name ^ " : " ^ (lexp_str' lxp dummy_sinfo) ^ ";") else "") in

let ret = List.fold_left (fun str ((_, name), lxp, ltp) -> let name = maybename name in let str = if pp_type ctx then (type_str name ltp)::str else str in - (name ^ " = " ^ (lexp_str' lxp) ^ ";" ^ sepdecl)::str) + (name ^ " = " ^ (lexp_str' lxp dummy_sinfo) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret

(** Syntactic equality (i.e. without β). *******)

-let rec eq e1 e2 = +let rec eq e1 e2 = try e1 == e2 || match (lexp_lexp' e1, lexp_lexp' e2) with | (Imm s1, Imm s2) -> sexp_equal s1 s2 | (SortLevel SLz, SortLevel SLz) -> true | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) - -> eq e11 e12 && eq e21 e22 + -> eq e11 e12 && eq e21 e22 | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 | (Builtin ((_, name1), _), Builtin ((_, name2), _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 - | (Susp (e1, s1), _) -> eq (push_susp e1 s1) e2 - | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) + | (Susp (e1, s1), _) -> eq (push_susp e1 s1 dummy_sinfo) e2 + | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 dummy_sinfo) | (Let (_, defs1, e1), Let (_, defs2, e2)) - -> eq e1 e2 && List.for_all2 - (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2) defs1 defs2 + -> eq e1 e2 && List.for_all2 + (fun (_, e1, t1) (_, e2, t2) -> eq t1 t2 && eq e1 e2 ) defs1 defs2 | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) - -> ak1 = ak2 && eq t11 t12 && eq t21 t22 + -> ak1 = ak2 && eq t11 t12 && eq t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) - -> ak1 = ak2 && eq t1 t2 && eq e1 e2 + -> ak1 = ak2 && eq t1 t2 && eq e1 e2 | (Call (e1, as1), Call (e2, as2)) - -> eq e1 e2 && List.for_all2 - (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 + -> eq e1 e2 && List.for_all2 + (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2 ) as1 as2 | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) -> l1 = l2 && List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2 ) as1 as2 && SMap.equal (List.for_all2 - (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2 - | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2 )) ctor1 ctor2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) - -> eq e1 e2 && eq r1 r2 && SMap.equal - (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2 + -> eq e1 e2 && eq r1 r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2 && (match (def1, def2) with | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) - -> if i1 == i2 then subst_eq s1 s2 else + -> if i1 == i2 then subst_eq s1 s2 else (match (metavar_lookup i1, metavar_lookup i2) with - | (MVal l, _) -> eq (push_susp l s1) e2 - | (_, MVal l) -> eq e1 (push_susp l s2) + | (MVal l, _) -> eq (push_susp l s1 dummy_sinfo) e2 + | (_, MVal l) -> eq e1 (push_susp l s2 dummy_sinfo) | _ -> false) | (Metavar (i1, s1, _), _) -> (match metavar_lookup i1 with - | MVal l -> eq (push_susp l s1) e2 + | MVal l -> eq (push_susp l s1 dummy_sinfo) e2 | _ -> false) | (_, Metavar (i2, s2, _)) -> (match metavar_lookup i2 with - | MVal l -> eq e1 (push_susp l s2) + | MVal l -> eq e1 (push_susp l s2 dummy_sinfo) | _ -> false) | _ -> false with | Invalid_argument _ -> false (* Different lengths in List.for_all2. *)

-and subst_eq s1 s2 = +and subst_eq s1 s2 = s1 == s2 || match (s1, s2) with | (S.Identity o1, S.Identity o2) -> o1 = o2 | (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2)) -> if o1 = o2 then - eq e1 e2 && 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) sinfo) e2 + eq (mkSusp e1 (S.shift o) dummy_sinfo) e2 && subst_eq (S.mkShift s1 o) s2 else let o = o2 - o1 in - eq e1 (mkSusp e2 (S.shift o) sinfo) + eq e1 (mkSusp e2 (S.shift o) dummy_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) sinfo) s) defs' + -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) dummy_sinfo) s) defs'

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

@@ -124,7 +124,7 @@ let rec lctx_to_subst lctx = * Another option would be to map them to `L.impossible`, * hence making the target domain be empty (i.e. making the substitution * generate closed results). *) - L.ssink v s + L.ssink dummy_sinfo v s | DB.CVfix (defs, lctx) -> let s1 = lctx_to_subst lctx in let s2 = lexp_defs_subst DB.dloc S.identity @@ -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) sinfo + mkSusp e (lctx_to_subst lctx) dummy_sinfo

(** Reduce to weak head normal form. @@ -167,26 +167,26 @@ let lexp_close lctx e = the inductive type of the target (and it's typelevel). A better solution would be to add these values as annotations in the lexp datatype. *) -let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = - let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : lexp = + let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo: lexp = match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf_aux e' ctx) - | Susp (e, s) -> lexp_whnf_aux (push_susp e s) ctx - | Call (e, []) -> lexp_whnf_aux e ctx + | Some e' -> lexp_whnf_aux e' ctx sinfo) + | Susp (e, s) -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo + | Call (e, []) -> lexp_whnf_aux e ctx sinfo | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_lexp' (lexp_whnf_aux f ctx) with + (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * 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) sinfo) - ctx + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx dummy_sinfo)) dummy_sinfo, + args) dummy_sinfo) + ctx sinfo | Call (f', xs1) -> mkCall (f', List.append xs1 xs) sinfo | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with @@ -194,7 +194,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf_aux e ctx in + let e' = lexp_whnf_aux e ctx sinfo in let get_refl e = let etype = get_type ctx e in (* FIXME we should not need get_type here *) let elevel = match lexp'_whnf (get_type ctx etype) ctx with @@ -203,9 +203,9 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = mkCall (DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; - L.Aerasable, e]) sinfo in + L.Aerasable, e]) dummy_sinfo in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with + let targs = match lexp_lexp' (lexp_whnf_aux it ctx dummy_sinfo) with | Inductive (_,_,fargs,_) -> fargs | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in try @@ -214,7 +214,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = = List.fold_left (fun (s, targs) (_, arg) -> match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx) s, []) + | [] -> (S.cons (lexp_whnf_aux arg ctx dummy_sinfo) s, []) | _targ::targs -> (* Ignore the type arguments *) (s, targs)) @@ -222,43 +222,43 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = aargs in (* Substitute case Eq variable by the proof (Eq.refl l t e') *) let subst = S.cons (get_refl e') subst in - lexp_whnf_aux (push_susp branch subst) ctx + lexp_whnf_aux (push_susp branch subst dummy_sinfo) ctx sinfo with | Not_found -> match default with | Some (_v,default) -> let subst = S.cons (get_refl e') (S.substitute e') in - lexp_whnf_aux (push_susp default subst) ctx + lexp_whnf_aux (push_susp default subst dummy_sinfo) ctx sinfo | _ -> Log.log_error ~section:"WHNF" ~loc:l {|Unhandled constructor "%s" in case expression|} name; - mkCase (l, e, rt, branches, default) sinfo in + mkCase (l, e, rt, branches, default) dummy_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 + (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with | Cons (it, (_, name)) -> reduce it name aargs - | _ -> mkCase (l, e, rt, branches, default) sinfo) + | _ -> mkCase (l, e, rt, branches, default) dummy_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 + | MVal e -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo | _ -> e)

(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs) dummy_sinfo) ctx sinfo

| _elem -> e

- in lexp_whnf_aux e ctx + in lexp_whnf_aux e ctx sinfo

and lexp'_whnf e (ctx : DB.lexp_context) : lexp' = - lexp_lexp' (lexp_whnf_aux e ctx) + lexp_lexp' (lexp_whnf_aux e ctx dummy_sinfo)

and lexp_whnf e (ctx : DB.lexp_context) : lexp = - lexp_whnf_aux e ctx + lexp_whnf_aux e ctx dummy_sinfo

and eq_cast_whnf ctx args = match args with @@ -289,7 +289,7 @@ and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp ((e1, e2) :: s) and set_shift_n (s : set_plexp) (n : U.db_offset) = List.map (let s = S.shift n in - fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s)) + fun (e1, e2) -> (Lexp.push_susp e1 s dummy_sinfo, Lexp.push_susp e2 s dummy_sinfo)) s and set_shift s : set_plexp = set_shift_n s 1

@@ -315,9 +315,9 @@ and level_canon e = | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with - | MVal e -> canon (push_susp e s) d acc + | MVal e -> canon (push_susp e s dummy_sinfo) d acc | _ -> add_var_depth (- i) d acc) - | Susp (e, s) -> canon (push_susp e s) d acc + | Susp (e, s) -> canon (push_susp e s dummy_sinfo) d acc | _ -> (max_int, m) in canon e 0 (0,IMap.empty)

@@ -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 sinfo in - let tltp = mkSusp etype subst sinfo in - let tlvl = mkSusp elvl subst sinfo in + let tlxp = mkSusp target subst dummy_sinfo in + let tltp = mkSusp etype subst dummy_sinfo in + let tlvl = mkSusp elvl subst dummy_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)]) sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) dummy_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,9 +453,9 @@ 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 sinfo)) - ((ak1, (mkVar (vdef1, i) sinfo))::args) - (ssink vdef1 s) + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s dummy_sinfo)) + ((ak1, (mkVar (vdef1, i) dummy_sinfo))::args) + (ssink dummy_sinfo vdef1 s) (i - 1) vdefs1 vdefs2 fieldtypes else None @@ -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)) sinfo, - eaargs) sinfo) subst sinfo in - let hlxp = mkCall (ctor, args) sinfo in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) dummy_sinfo, + eaargs) dummy_sinfo) subst dummy_sinfo in + let hlxp = mkCall (ctor, args) dummy_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) sinfo in + let hlxp = mkVar ((DB.dloc, None), 0) dummy_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)) sinfo + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) dummy_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)) sinfo (* FIXME: Could be more canonical *) + else mkSortLevel (mkSLlub' (e1, e2)) dummy_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) sinfo) - else let l2' = (mkSusp l2 (S.substitute impossible) sinfo) in + then SortResult (mkSusp k2 (S.substitute impossible) dummy_sinfo) + else let l2' = (mkSusp l2 (S.substitute impossible) dummy_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')) sinfo) + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) dummy_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) sinfo) + SortResult (mkSusp k2 (S.substitute DB.level0) dummy_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) sinfo) + -> SortResult (mkSort (l, StypeOmega) dummy_sinfo) | _ -> SortInvalid) | (Sort (_, _), _) -> SortK2NotType | (_, _) -> SortK1NotType @@ -583,7 +583,7 @@ and nerased_let defs erased = erased es

(* "check ctx e" should return τ when "Δ ⊢ e : τ" *) -and check'' erased ctx e = +and check'' erased ctx e sinfo = let check = check'' in let assert_type ctx e t t' = if conv_p ctx t t' then () @@ -594,7 +594,7 @@ and check'' erased ctx e = (lexp_string e) (lexp_string t) (lexp_string t') in let check_type erased ctx t = - let s = check erased ctx t in + let s = check erased ctx t sinfo in (match lexp'_whnf s ctx with | Sort _ -> () | _ @@ -607,24 +607,24 @@ and check'' erased ctx e = | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; - DB.type_int) + DB.type_int ) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) - -> let t = check erased ctx e in + -> let t = check erased ctx e sinfo in (* FIXME: Actually, we should probably have a special function to check * that `e` is a level, so as to avoid `case` and other funny things. *) assert_type ctx e t DB.type_level; DB.type_level | SortLevel (SLlub (e1, e2)) - -> let t1 = check erased ctx e1 in + -> let t1 = check erased ctx e1 sinfo in assert_type ctx e1 t1 DB.type_level; - let t2 = check erased ctx e2 in + let t2 = check erased ctx e2 sinfo in assert_type ctx e2 t2 DB.type_level; DB.type_level | Sort (l, Stype e) - -> let t = check erased ctx e in + -> let t = check erased ctx e sinfo in assert_type ctx e t DB.type_level; - mkSort (l, Stype (mkSortLevel (SLsucc e) sinfo)) sinfo + mkSort (l, Stype (mkSortLevel (SLsucc e) dummy_sinfo)) dummy_sinfo | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> ((* error_tc ~loc:(lexp_location e) "Reached unreachable sort!"; @@ -641,7 +641,7 @@ and check'' erased ctx e = {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v - | Susp (e, s) -> check erased ctx (push_susp e s) + | Susp (e, s) -> check erased ctx (push_susp e s dummy_sinfo) sinfo | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) @@ -657,12 +657,12 @@ and check'' erased ctx e = (check (if DB.set_mem (n - 1) nerased then DB.set_empty else nerased) - nctx e) - (push_susp t (S.shift n)); + nctx e sinfo) + (push_susp t (S.shift n) dummy_sinfo); n - 1) (List.length defs) defs in - mkSusp (check nerased nctx e) - (lexp_defs_subst l S.identity defs) sinfo + mkSusp (check nerased nctx e sinfo) + (lexp_defs_subst l S.identity defs) dummy_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 @@ -683,19 +683,19 @@ and check'' erased ctx e = mkArrow (ak, v, t, l, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) - e) sinfo) + e sinfo) dummy_sinfo) | Call (f, args) - -> let ft = check erased ctx f in + -> let ft = check erased ctx f sinfo in List.fold_left (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) - ctx arg in + ctx arg sinfo in match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> 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) sinfo + mkSusp t2 (S.substitute arg) dummy_sinfo | _ -> log_tc_error ~loc:(lexp_location arg) "Calling a non functin (type = %s)!" (lexp_string ft); @@ -744,7 +744,7 @@ and check'' erased ctx e = mkArrow (ak, v, t, lexp_location t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) - args) sinfo in + args) dummy_sinfo in let tct = arg_loop ctx erased args in tct | Case (l, e, ret, branches, default) @@ -753,7 +753,7 @@ and check'' erased ctx e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e) ctx in + let etype = lexp_whnf (check erased ctx e sinfo) ctx in (* FIXME save the type in the case lexp instead of recomputing it over and over again *) let ekind = get_type ctx etype in @@ -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 sinfo in - let tltp = mkSusp etype subst sinfo in - let tlvl = mkSusp elvl subst sinfo in + let tlxp = mkSusp e subst dummy_sinfo in + let tltp = mkSusp etype subst dummy_sinfo in + let tlvl = mkSusp elvl subst dummy_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)]) sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) dummy_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 @@ -799,7 +799,7 @@ and check'' erased ctx e = | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s sinfo)) - (ssink vdef s) + (ssink dummy_sinfo vdef s) (mkCall (mkSusp hlxp (S.shift 1) sinfo, [(ak, mkVar (vdef, 0) sinfo)]) sinfo) vdefs fieldtypes | _ @@ -807,13 +807,13 @@ and check'' erased ctx e = (erased, ctx, hlxp) in let hctor = mkCall (mkCons (it, (l, name)) sinfo, - List.map (fun (_, a) -> (P.Aerasable, a)) aargs) sinfo in + List.map (fun (_, a) -> (P.Aerasable, a)) aargs) dummy_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) + (check nerased nctx branch sinfo) (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) sinfo)) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in @@ -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) sinfo in + let hlxp = mkVar ((l, None), 0) dummy_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) sinfo) + assert_type nctx d (check nerased nctx d sinfo) + (mkSusp ret (S.shift 2) dummy_sinfo) | None -> if diff > 0 then @@ -844,36 +844,36 @@ and check'' erased ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_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) sinfo, - indtype fargs (nargs - 1)) sinfo + mkCall (mkSusp t (S.shift nargs) dummy_sinfo, + indtype fargs (nargs - 1)) dummy_sinfo | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) sinfo in + fieldargs ftypes) dummy_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) sinfo in + buildtype fargs) dummy_sinfo in buildtype fargs with | Not_found -> log_tc_error ~loc:l {|Constructor "%s" does not exist|} name; - DB.type_int) + DB.type_int ) | _ -> log_tc_error ~loc:(lexp_location e) "Cons of a non-inductive type: %s" (lexp_string t); - DB.type_int) + DB.type_int ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> let e = push_susp e s in - check erased ctx e - | MVar (_, t, _) -> push_susp t s) + | MVal e -> let e = push_susp e s dummy_sinfo in + check erased ctx e sinfo + | MVar (_, t, _) -> push_susp t s dummy_sinfo)

and check' ctx e = let res = check'' DB.set_empty ctx e in @@ -926,7 +926,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) - | Susp (e, s) -> fv (push_susp e s) + | Susp (e, s) -> fv (push_susp e s dummy_sinfo) | Let (_, defs, e) -> let len = List.length defs in let (fvs, _) @@ -975,9 +975,9 @@ and fv (e : lexp) : (DB.set * mv_set) = cases s | Metavar (id, s, name) -> (match metavar_lookup id with - | MVal e -> fv (push_susp e s) + | MVal e -> fv (push_susp e s dummy_sinfo) | MVar (sl, t, cl) - -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in + -> let (fvs, mvs) = fv_erase (fv (push_susp t s dummy_sinfo)) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in let ofvs = LMap.find_opt fv_memo e in @@ -1010,14 +1010,15 @@ 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) sinfo)) sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) dummy_sinfo)) dummy_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) + | Susp (e, s) -> get_type ctx (push_susp e s dummy_sinfo) | 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) sinfo + mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) dummy_sinfo + | Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in @@ -1025,18 +1026,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) sinfo) + | _ -> mkSort (l, StypeOmega) dummy_sinfo) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, v, t, l, get_type (DB.lctx_extend ctx v Variable t) - e) sinfo) + e) dummy_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) sinfo + -> mkSusp t2 (S.substitute arg) dummy_sinfo | _ -> ft) ft args | Inductive (l, _label, args, cases) @@ -1058,18 +1059,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) sinfo) + (mkSusp level' (L.sunshift n) dummy_sinfo) | _tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) case in level) - cases (mkSortLevel SLz sinfo) in - mkSort (l, Stype level) sinfo + cases (mkSortLevel SLz dummy_sinfo) in + mkSort (l, Stype level) dummy_sinfo | (ak, v, t)::args -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) sinfo in + arg_loop args (DB.lctx_extend ctx v Variable t)) dummy_sinfo in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1081,29 +1082,29 @@ and get_type ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_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) sinfo, - indtype fargs (nargs - 1)) sinfo + mkCall (mkSusp t (S.shift nargs) dummy_sinfo, + indtype fargs (nargs - 1)) dummy_sinfo | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) sinfo in + fieldargs ftypes) dummy_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) sinfo in + buildtype fargs) dummy_sinfo in buildtype fargs - with Not_found -> DB.type_int) - | _ -> DB.type_int) + with Not_found -> DB.type_int ) + | _ -> DB.type_int ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> get_type ctx (push_susp e s) - | MVar (_, t, _) -> push_susp t s) + | MVal e -> get_type ctx (push_susp e s dummy_sinfo) + | MVar (_, t, _) -> push_susp t s dummy_sinfo)

(* FIXME: Remove the mutual recursion between `lexp_whnf` and `get_type`, and move this closer to the `lexp_whnf`. *) @@ -1148,7 +1149,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)

| L.Lambda (P.Aerasable, _, _, body) - -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy)) + -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) dummy_sinfo)

| L.Lambda (_, vdef, ty, body) -> let lctx' = DB.lctx_extend lctx vdef Variable ty in @@ -1166,7 +1167,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = let ebranches = clean_branch_map lctx branches in E.Case (location, etarget, ebranches, clean_default lctx default)

- | L.Susp (l, s) -> erase_type lctx (L.push_susp l s) + | L.Susp (l, s) -> erase_type lctx (L.push_susp l s dummy_sinfo)

(* To be thrown out *) | L.Arrow _ -> E.Type lxp @@ -1177,7 +1178,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Inductive (_, _, _, _) -> E.Type lxp | L.Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> erase_type lctx (push_susp e s) + | MVal e -> erase_type lctx (push_susp e s dummy_sinfo) | MVar _ -> Log.internal_error "Metavar in erase_type")

and clean_arg lctx = function @@ -1194,7 +1195,7 @@ and clean_decls and clean_default lctx lxp = match lxp with | Some (v, lxp) - -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) in + -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) dummy_sinfo in Some (v, erase_type lctx lxp') | None -> None

@@ -1208,12 +1209,12 @@ and clean_branch_map lctx cases = | (_, var) :: tl -> (* Keep the variable and sink the substitution. *) let lctx' = DB.lctx_extend lctx var Variable erasure_dummy in - clean_arg_list tl (var :: acc) (ssink var subst) lctx' + clean_arg_list tl (var :: acc) (ssink dummy_sinfo var subst) lctx' | [] -> (List.rev acc, subst, lctx) in let eargs, subst, lctx' = clean_arg_list args [] S.identity lctx in let subst = S.cons erasure_dummy subst in (* Substitute the equality. *) - (l, eargs, erase_type lctx' (L.push_susp expr subst)) + (l, eargs, erase_type lctx' (L.push_susp expr subst dummy_sinfo)) in SMap.map clean_branch cases

@@ -1278,16 +1279,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) sinfo)) + mkSusp t (S.shift offset) dummy_sinfo)) types) - SMap.empty) sinfo, - cons_label) sinfo, + SMap.empty) dummy_sinfo, + cons_label) dummy_sinfo, List.mapi (fun i (oname, _t) - -> (P.Aimplicit, mkVar (oname, offset - i - 1) sinfo)) - types) sinfo + -> (P.Aimplicit, mkVar (oname, offset - i - 1) dummy_sinfo)) + types) dummy_sinfo | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> mkLet (loc, [(name, mkSusp e (S.shift 1) sinfo, t)], - mk_lets_and_tup blocs ((name, t) :: types)) sinfo + -> mkLet (loc, [(name, mkSusp e (S.shift 1) dummy_sinfo, t)], + mk_lets_and_tup blocs ((name, t) :: types)) dummy_sinfo | (DB.CVfix (defs, _) :: blocs) -> mkLet (loc, defs, mk_lets_and_tup blocs (List.append @@ -1295,7 +1296,7 @@ let ctx2tup ctx nctx = (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) sinfo + types)) dummy_sinfo | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []

===================================== src/positivity.ml ===================================== @@ -108,7 +108,7 @@ and positive' index lexp =

| Lexp.Lambda (_, _, _, e) -> positive index e

- | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s) + | Lexp.Susp (e, s) -> positive index (Lexp.push_susp e s dummy_sinfo)

| Lexp.Var _ (*

===================================== src/sexp.ml ===================================== @@ -41,7 +41,6 @@ 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/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) sinfo) (mkSusp le2 (S.shift o2) sinfo) + && OL.conv_p ctx (mkSusp le1 (S.shift o1) dummy_sinfo) (mkSusp le2 (S.shift o2) dummy_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) sinfo, + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) dummy_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) sinfo, + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo, S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) sinfo, + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo, S.Identity 1, o1')) s2 o1 o2 o | (S.Identity o1', S.Identity o2') @@ -215,8 +215,8 @@ and unify' (e1: lexp) (e2: lexp) (* Then, we handle metavariables (aka. flexible-flexible and Flexible-Rigid Equations). Reminder: WHNF implies that the metavariables are not already instanciated. *) - | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' - | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' dummy_sinfo + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' dummy_sinfo

(* Otherwise, the equation is rigid-rigid. Let's start with the cases that can leave residuals: 1. Variables, since they could @@ -292,14 +292,14 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> inverse subst (try both sides) - metavar , lexp -> inverse subst *) -and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) +and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) sinfo : return_type = let unif idx s lxp = let t = match metavar_lookup idx with | MVal _ -> Log.internal_error "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in - match Inverse_subst.apply_inv_subst lxp s with + | MVar (_, t, _) -> push_susp t s sinfo in + match Inverse_subst.apply_inv_subst lxp s sinfo with | exception Inverse_subst.Not_invertible -> log_info "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n"

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