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

Commits: 967baf86 by “falismai@iro.umontreal.ca” at 2022-04-03T06:11:39+00:00 location -> 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 dummy_sinfo)) lexprs; + List.iter (fun lexpr -> ignore (OL.check (ectx_to_lctx ectx') lexpr)) 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) dummy_sinfo + mkSusp p (S.shift r) 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) dummy_sinfo) dummy_sinfo + mkArrow (Anormal, (dloc, None), t, dloc, t) )

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 dummy_sinfo in + let t = OL.check Myers.nil e in lmap := SMap.add name (e, t) map

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

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

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

let dloc = dummy_location -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_level_sort = mkSort (dloc, StypeLevel) +let sort_omega = mkSort (dloc, StypeOmega) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort) +let level0 = mkSortLevel SLz +let level1 = mkSortLevel (mkSLsucc level0) +let level2 = mkSortLevel (mkSLsucc level1) +let type0 = mkSort (dloc, Stype level0) +let type1 = mkSort (dloc, Stype level1) +let type2 = mkSort (dloc, Stype level2) +let type_int = mkBuiltin ((dloc, "Int"), type0) +let type_integer = mkBuiltin ((dloc, "Integer"), type0) +let type_float = mkBuiltin ((dloc, "Float"), type0) +let type_string = mkBuiltin ((dloc, "String"), type0) +let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0) let type_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) dummy_sinfo)) dummy_sinfo , dloc, + mkSort (dloc, Stype (mkVar (lv, 0))) , dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 0) dummy_sinfo, dloc, + mkVar (tv, 0), dloc, mkArrow (Anormal, (dloc, None), - mkVar (tv, 1) dummy_sinfo, dloc, - mkSort (dloc, Stype (mkVar (lv, 3) dummy_sinfo)) dummy_sinfo) dummy_sinfo) dummy_sinfo) dummy_sinfo) + mkVar (tv, 1) , dloc, + mkSort (dloc, Stype (mkVar (lv, 3)))))))

-let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type dummy_sinfo) dummy_sinfo +let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type)

let eq_refl = let lv = (dloc, Some "l") in @@ -121,14 +121,14 @@ let eq_refl = mkArrow (Aerasable, lv, type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (mkVar (lv, 0) dummy_sinfo)) dummy_sinfo, dloc, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, mkArrow (Aerasable, xv, - mkVar (tv, 0) dummy_sinfo, dloc, + mkVar (tv, 0), dloc, mkCall (type_eq, - [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 + [Aerasable, mkVar (lv, 2); + Aerasable, mkVar (tv, 1); + Anormal, mkVar (xv, 0); + Anormal, mkVar (xv, 0)])))))

(* easier to debug with type annotations *) @@ -296,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 dummy_sinfo in + -> (let str = lexp_str (!debug_ppctx) lexp in let strs = match String.split_on_char '\n' str with | hd :: tl -> print_string hd; tl @@ -383,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)) dummy_sinfo + mkSusp t (S.shift (i + 1))

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)) dummy_sinfo) + | (_, LetDef (o, v), _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> 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) dummy_sinfo); + BI.add_builtin_cst name (mkBuiltin ((dloc, name) , type_special_form)); 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 dummy_sinfo) var ltp + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) 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 dummy_sinfo + let ltype' = try OL.check lctx lxp 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) dummy_sinfo) var; + nctx (push_susp ltp (S.shift n)) 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) dummy_sinfo); + (push_susp ltp (S.shift n)); 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) dummy_sinfo + mkMetavar (meta, S.identity, name)

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)) dummy_sinfo) + (mkSort (loc, Stype (newMetalevel ctx sl loc)))

(* 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) dummy_sinfo in + let lxp = mkVar (id, idx) 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) sinfo = +let meta_to_var ids (e : lexp) =

let count = IMap.cardinal ids in

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

let sort_generalized_metavars sl cl ctx mfvs = @@ -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)) dummy_sinfo + Inverse_subst.apply_inv_subst mt (S.shift (cl' - cl)) 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 dummy_sinfo + meta_to_var ids e | ((id, vname, mt) :: mfvs) - -> let mt' = meta_to_var ids mt dummy_sinfo in + -> let mt' = meta_to_var ids mt 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) dummy_sinfo) ((ak, arg)::args) - | _ -> (mkCall (e, List.rev args) dummy_sinfo, t) + instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) + | _ -> (mkCall (e, List.rev args), t) in instantiate t []

-and infer_type pexp ectx var sinfo = +and infer_type pexp ectx var = (* We could also use lexp_check with an argument of the form * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) @@ -643,7 +643,7 @@ and infer_type pexp ectx var sinfo = Unif.unify (mkSort (l, Stype (newMetalevel (ectx_to_lctx ectx) (ectx_to_scope_level ectx) - l)) sinfo) + l))) s (ectx_to_lctx ectx) with | (_::_) @@ -658,7 +658,7 @@ and infer_type pexp ectx var sinfo = t

and lexp_let_decls declss (body: lexp) _ctx = - List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp) dummy_sinfo) + List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) 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) dummy_sinfo in + let arrow = mkArrow (kind, var, arg, l, body) 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 dummy_sinfo) in + name (mkSusp t s) 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) dummy_sinfo); + ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); 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))) dummy_sinfo in + - M.length (ectx_to_lctx ctx))) 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')]) dummy_sinfo (* Target lexp *) + (Anormal, tlxp')]) (* 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) dummy_sinfo in + let head_lexp = mkVar (v, 0) 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) dummy_sinfo + mkSusp body (S.substitute arg) | _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 dummy_sinfo) in - make_nctx nctx (ssink dummy_sinfo var s) pargs cargs + let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink 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 dummy_sinfo) in - make_nctx nctx (ssink dummy_sinfo var s) pargs cargs pe + -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + make_nctx nctx (ssink 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 dummy_sinfo) in + let nctx = ctx_extend ctx var Variable (mkSusp fty s) 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 dummy_sinfo var s) pargs cargs pe + make_nctx nctx (ssink 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) dummy_sinfo) in + (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in let head_lexp_args = List.mapi (fun i (ak, vname) -> - (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 + (ak, mkVar (vname, List.length fargs - i - 1))) fargs in + let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) 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 dummy_sinfo then + -> if Eval.constructor_p name ctx 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) dummy_sinfo + mkCase (loc, tlxp, rtype, lpattern, dflt)

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) dummy_sinfo with + func args ctx (Some t) 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) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg))

| (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) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg))

| (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) dummy_sinfo) + (L.mkSusp ret_type (S.substitute larg)) | [], _ -> (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) dummy_sinfo) in + (L.mkSusp ret_type (S.substitute larg)) in

let (largs, ret_type) = handle_fun_args [] sargs SMap.empty ltp in - (mkCall (func, List.rev largs) dummy_sinfo, Inferred ret_type) + (mkCall (func, List.rev largs), 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) dummy_sinfo) + -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> mkArrow (Aerasable, vname, t, l, e) dummy_sinfo) + -> mkArrow (Aerasable, vname, t, l, e)) 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 dummy_sinfo in + -> let lxp = infer_type exp ctx var 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) sinfo +and lexp_expand_macro loc macro_funct sargs ctx (_ot : ltype option) : 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 sinfo in + let macro_expand = lexp_eval ctx macro_expand in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let macro = lexp_eval ctx macro_funct sinfo in + let macro = lexp_eval ctx macro_funct in let args = [macro; BI.o2v_list sargs] in

(* FIXME: Make a proper `Var`. *) @@ -1116,7 +1116,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = 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 dummy_sinfo in + let ret = lexp_expand_macro loc lxp sargs ctx None in match ret with | Vcommand cmd -> (match cmd () with @@ -1149,7 +1149,7 @@ 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)) dummy_sinfo in + -> let adjusted_t = push_susp t (S.shift (i + 1)) 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 @@ -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 sinfo = +and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in - let t = infer_type se nctx name sinfo in + let t = infer_type se nctx name 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 @@ -1193,12 +1193,12 @@ and infer_and_generalize_type (ctx : elab_context) se name sinfo = let rec strip_rettype t = match lexp_lexp' t with | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, t1, l, strip_rettype t2) sinfo + -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e) sinfo) + -> mkArrow (Aerasable, name, t, l, e)) t

and infer_and_generalize_def (ctx : elab_context) se = @@ -1207,11 +1207,11 @@ and infer_and_generalize_def (ctx : elab_context) se = let g = generalize nctx e in let e' = g (fun ne vname t _l e -> mkLambda ((if ne then Aimplicit else Aerasable), - vname, t, e) dummy_sinfo) + vname, t, e)) e in let t' = g (fun ne name t _l e -> mkArrow ((if ne then Aimplicit else Aerasable), - name, t, sexp_location se, e) dummy_sinfo) + name, t, sexp_location se, e)) 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) dummy_sinfo in + -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) 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)) dummy_sinfo + | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) | _ -> 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) dummy_sinfo, ltp)], sdecls, toks, + [(var, mkSusp lexp (S.shift 1), 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) dummy_sinfo in - let bi = mkBuiltin ((loc, name), ltp') dummy_sinfo in + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in + let bi = mkBuiltin ((loc, name), ltp') 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) dummy_sinfo, Lazy) + (mkCons (idt, sym), Lazy)

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

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

let sform_hastype ctx loc sargs _ot = match sargs with - | [se; st] -> let lt = infer_type st ctx (loc, None) dummy_sinfo in + | [se; st] -> let lt = infer_type st ctx (loc, None) in let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; @@ -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 dummy_sinfo in + let lt1 = infer_type st1 ctx v in let nctx = ectx_extend ctx v Variable lt1 in - let lt2 = infer_type st2 nctx (sexp_location st2, None) dummy_sinfo in - (mkArrow (kind, v, lt1, loc, lt2) dummy_sinfo, Lazy) + let lt2 = infer_type st2 nctx (sexp_location st2, None) in + (mkArrow (kind, v, lt1, loc, lt2), 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) 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 + | [(String _) as se] -> mkImm (se), Inferred DB.type_string + | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int + | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [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)) dummy_sinfo, Lazy) + (mkMetavar (idx, subst, (loc, Some name)), 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 dummy_sinfo in + -> Inverse_subst.apply_inv_subst t subst 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 dummy_sinfo, + (mkSusp mv subst, 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 dummy_sinfo) + | Some st -> Some (infer_type st ctx arg) | _ -> 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) dummy_sinfo, + (mkLambda (kind, arg, lt1, lbody), match alt with - | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2) dummy_sinfo) + | Inferred lt2 -> Inferred (mkArrow (kind, arg, lt1, loc, lt2)) | _ -> 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) dummy_sinfo, + (mkLambda (ak2, v, lt1, lam), match alt with - | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2') dummy_sinfo) + | Inferred lt2' -> Inferred (mkArrow (ak2, v, lt1, loc, lt2')) | _ -> 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) dummy_sinfo) ot in + let ot = Option.map (fun t -> mkSusp t (S.shift off)) ot in let bdy, ot = elaborate nctx sbody ot in let ot = match ot with - | Inferred t -> Inferred (mkSusp t s dummy_sinfo) + | Inferred t -> Inferred (mkSusp t s) | _ -> 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 dummy_sinfo + | Symbol (_, "z") -> mkSortLevel SLz | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) - -> mkSortLevel (SLsucc (infer_level ctx se)) dummy_sinfo + -> mkSortLevel (SLsucc (infer_level ctx se)) | Node (Symbol (_, "_∪_"), [se1; se2]) -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in @@ -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) dummy_sinfo, - Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l) dummy_sinfo)) dummy_sinfo)) + (mkSort (loc, Stype l), + Inferred (mkSort (loc, Stype (mkSortLevel (mkSLsucc l))))) | _ -> (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) dummy_sinfo in (lxp, Lazy) + let lxp = mkVar ((loc, None), i) 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)) dummy_sinfo) in + (Lexp.mkSusp tuple (S.shift (usr_len - dflt_len))) 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) dummy_sinfo in + let v = mkVar ((dloc, Some name), idx) 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 dummy_sinfo)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) 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) sinfo : (value_type) = +let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info) : (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) sinfo : (valu (* ---------------- *) | Let(_, decls, inst) -> let nctx = eval_decls decls ctx trace in - eval' inst nctx sinfo + eval' inst nctx

(* Function call *) | Call (f, args) -> eval_call (elexp_location f) f trace - (eval f ctx trace sinfo) - (List.map (fun e -> eval e ctx trace sinfo) args) + (eval f ctx trace ) + (List.map (fun e -> eval e ctx trace ) 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 dummy_sinfo - | _ -> eval_call loc unef i (eval e ctx i dummy_sinfo) vs in + eval e ctx trace + | _ -> eval_call loc unef i (eval e ctx i ) 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) dummy_sinfo)]) dummy_sinfo) + -> Vtype (L.mkCall (e, [(Anormal, mkVar (vdummy, -1) )]) ) | _ -> 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 dummy_sinfo in + let v = eval target ctx i 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 dummy_sinfo + eval exp nctx i

(* Run default *) with Not_found -> (match dflt with | Some (var, lxp) - -> eval lxp (add_rte_variable var v ctx) i dummy_sinfo + -> eval lxp (add_rte_variable var v ctx) i | _ -> 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 dummy_sinfo) args in + let arg_val = List.map (fun (_k, e) -> eval e ctx i ) 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 dummy_sinfo in + let v = eval lxp nctx i in let offset = n - idx in ignore (set_rte_variable offset name v nctx)) decls;

@@ -798,12 +798,12 @@ 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 sinfo = +let constructor_p name ectx = try let idx = senv_lookup name ectx in (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) ) (ectx_to_lctx ectx) with | Cons _ -> true (* It's indeed a constructor! *) | _ -> false with Senv_Lookup_Fail _ -> false @@ -817,7 +817,7 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) ) (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) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx) ) (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) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) ) (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) dummy_sinfo) (ectx_to_lctx ectx) with + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx) ) (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 dummy_sinfo) + | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx ) | _ -> 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 dummy_sinfo + eval (OL.erase_type lctx e) rctx 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 dummy_sinfo) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx ) 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 dummy_sinfo + debug_eval elexp rctx

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

let next_free_address : addr ref = ref 1

===================================== src/inverse_subst.ml ===================================== @@ -65,7 +65,7 @@ let transfo (s: subst) : substIR option = | _ -> assert false in let shiftVar (var: lexp) (offset: int): int = - indexOf (mkSusp var (S.shift offset) dummy_sinfo) (* Helper : shift the index of a var *) + indexOf (mkSusp var (S.shift offset) ) (* 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) dummy_sinfo + mkVar ((U.dummy_location, None), idx)

(** 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 dummy_sinfo) (compose_inv_subst s' s) + S.cons (apply_inv_subst e s ) (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) sinfo : lexp = +and apply_inv_subst (e : lexp) (s : subst) : lexp = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s dummy_sinfo)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s )) | SortLevel (SLlub (e1, e2)) (* FIXME: use mkSLlub? *) - -> 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 + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s , apply_inv_subst e2 s )) + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s )) | Sort (_l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) sinfo - | Susp (e, s') -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo + | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Susp (e, s') -> apply_inv_subst (push_susp e s' ) s | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink dummy_sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink dummy_sinfo v s, - (v, apply_inv_subst def s' dummy_sinfo, apply_inv_subst ty s dummy_sinfo) + -> (ssink v s, + (v, apply_inv_subst def s' , apply_inv_subst ty s ) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, apply_inv_subst e s' dummy_sinfo) sinfo + mkLet (l, ndefs, apply_inv_subst e s' ) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, apply_inv_subst t1 s dummy_sinfo, l, - apply_inv_subst t2 (ssink dummy_sinfo v s) dummy_sinfo) sinfo + -> mkArrow (ak, v, apply_inv_subst t1 s , l, + apply_inv_subst t2 (ssink v s) ) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, apply_inv_subst t s dummy_sinfo, apply_inv_subst e (ssink dummy_sinfo v s) dummy_sinfo) sinfo + -> mkLambda (ak, v, apply_inv_subst t s , apply_inv_subst e (ssink v s) ) | Call (f, args) - -> mkCall (apply_inv_subst f s dummy_sinfo, - L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s dummy_sinfo)) args) sinfo + -> mkCall (apply_inv_subst f s , + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink dummy_sinfo v s, (ak, v, apply_inv_subst t s dummy_sinfo) :: nargs)) + -> (ssink v s, (ak, v, apply_inv_subst t s ) :: 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 dummy_sinfo v s, - (ak, v, apply_inv_subst t s dummy_sinfo) + -> (ssink v s, + (ak, v, apply_inv_subst t s ) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (apply_inv_subst it s dummy_sinfo, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (apply_inv_subst it s , name) | Case (l, e, ret, cases, default) - -> mkCase (l, apply_inv_subst e s dummy_sinfo, apply_inv_subst ret s dummy_sinfo, + -> mkCase (l, apply_inv_subst e s , apply_inv_subst ret s , SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink dummy_sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - let s'' = ssink dummy_sinfo (l, None) s' in - (l, cargs, apply_inv_subst e s'' dummy_sinfo )) + let s'' = ssink (l, None) s' in + (l, cargs, apply_inv_subst e s'' )) cases, match default with | None -> default - | Some (v,e) -> Some (v, apply_inv_subst e (ssink dummy_sinfo (l, None) (ssink dummy_sinfo v s)) dummy_sinfo)) sinfo + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s)) )) | Metavar (id, s', name) -> match metavar_lookup id with - | MVal e -> apply_inv_subst (push_susp e s' dummy_sinfo) s sinfo - | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) sinfo + | MVal e -> apply_inv_subst (push_susp e s' ) s + | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name)

===================================== src/lexp.ml ===================================== @@ -36,14 +36,13 @@ 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 sinfo = sexp

type label = symbol

include Pexp.ArgKind

-let dummy_sinfo : sexp list = []

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

@@ -63,32 +62,32 @@ let dummy_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 * sinfo + and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level - | Sort of U.location * sort + | Sort of sinfo * sort | Builtin of symbol * ltype | Var of vref | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype + | Let of sinfo * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname * ltype * sinfo * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label + | Inductive of sinfo * label * ((arg_kind * vname * ltype) list) (* formal Args *) * ((arg_kind * vname * ltype) list) SMap.t | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp + | Case of sinfo * lexp * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (sinfo * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) (* The `subst` will be applied to the the metavar's value when it * gets instantiated. *) | Metavar of meta_id * subst * vname (* (* For logical metavars, there's no substitution. *) - * | Metavar of (U.location * string) * metakind * metavar ref + * | Metavar of (sinfo * string) * metakind * metavar ref * and metavar = * (* An uninstantiated var, along with a venv (stipulating over which vars * * it should be closed), and its type. @@ -181,8 +180,8 @@ let metavar_lookup (id : meta_id) : metavar_info * biggest bucket length: 205 / 36 * found/new lexp entries: - / 2 *)

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

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

let hc_table : WHC.t = WHC.create 1000

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

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

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

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

(* Apply a "dummy" substitution which replace #0 with #0 * in order to account for changes to a variable's name. @@ -475,7 +474,7 @@ let ssink sinfo = 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) dummy_sinfo) (S.shift 1)) dummy_sinfo +let srename name le = mkSusp le (S.cons (mkVar (name, 0) ) (S.shift 1))

(* Shift by a negative amount! *) let rec sunshift n = @@ -515,20 +514,20 @@ let rec lexp_location e = | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e - | SortLevel SLz -> U.dummy_location - | Imm s -> sexp_location s - | Var ((l,_),_) -> l - | Builtin ((l, _), _) -> l + | SortLevel SLz -> dummy_sinfo + | Imm s -> s + | Var ((l,_),_) -> dummy_sinfo + | Builtin ((l, _), _) -> dummy_sinfo | Let (l,_,_) -> l | Arrow (_,_,_,l,_) -> l - | Lambda (_,(l,_),_,_) -> l + | Lambda (_,(l,_),_,_) -> dummy_sinfo | Call (f,_) -> lexp_location f | Inductive (l,_,_,_) -> l - | Cons (_,(l,_)) -> l + | Cons (_,(l,_)) -> dummy_sinfo | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_)) -> l + | Metavar (_,_,(l,_)) -> dummy_sinfo

(********* Normalizing a term *********) @@ -537,132 +536,132 @@ 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 sinfo = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s sinfo)) sinfo + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s )) | 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 + -> mkSortLevel (mkSLlub' (mkSusp e1 s , mkSusp e2 s )) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s )) | Sort (_, _) -> e | Builtin _ -> e

| Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink 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 sinfo v s) defs in - mkLet (l, loop s defs, mkSusp e s' sinfo) sinfo + -> (v, mkSusp def s' , mkSusp ty s ) :: loop (ssink v s) defs in + mkLet (l, loop s defs, mkSusp e s' ) | Arrow (ak, v, t1, l, t2) - -> 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 + -> mkArrow (ak, v, mkSusp t1 s , l, mkSusp t2 (ssink v s) ) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s , mkSusp e (ssink v s) ) + | Call (f, args) -> mkCall (mkSusp f s , + L.map (fun (ak, arg) -> (ak, mkSusp arg s )) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, (ak, v, mkSusp t s sinfo) :: nargs)) + -> (ssink v s, (ak, v, mkSusp t s ) :: 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 sinfo v s, - (ak, v, mkSusp t s sinfo) + -> (ssink v s, + (ak, v, mkSusp t s ) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (mkSusp it s sinfo, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (mkSusp it s , name) | Case (l, e, ret, cases, default) - -> mkCase (l, mkSusp e s sinfo, mkSusp ret s sinfo, - SMap.map (fun (l, cargs, e) + -> mkCase (l, mkSusp e s , mkSusp ret s , + SMap.map (fun ((l: sinfo), cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - (l, cargs, mkSusp e (ssink sinfo (l, None) s') sinfo)) + (l, cargs, mkSusp e (ssink (l, None) s') )) cases, match default with | None -> default - | Some (v,e) -> Some (v, mkSusp e (ssink sinfo (l, None) (ssink sinfo v s)) sinfo)) sinfo + | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s)) )) (* 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) sinfo - | (Var _ | Metavar _) -> nosusp (mkSusp e s sinfo) + | Susp (e,s') -> push_susp e (scompose s' s) + | (Var _ | Metavar _) -> nosusp (mkSusp e s )

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

(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) -let clean e sinfo = +let clean e = let rec clean s e = match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) sinfo + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) | SortLevel (SLlub (e1, e2)) (* FIXME: The new SLlub could have `succ` on both sides! *) - -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) sinfo - | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) sinfo + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (_, _) -> e | Builtin _ -> e | Let (l, defs, e) - -> let s' = L.fold_left (fun s (v, _, _) -> ssink sinfo v s) s defs in + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) - -> (ssink sinfo v s, + -> (ssink v s, (v, clean s' def, clean s ty) :: ndefs)) (s, []) defs in - mkLet (l, ndefs, clean s' e) sinfo + mkLet (l, ndefs, clean s' e) | Arrow (ak, v, t1, l, t2) - -> 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 + -> mkArrow (ak, v, clean s t1, l, clean (ssink v s) t2) + | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e) | Call (f, args) -> mkCall (clean s f, - L.map (fun (ak, arg) -> (ak, clean s arg)) args) sinfo + L.map (fun (ak, arg) -> (ak, clean s arg)) args) | Inductive (l, label, args, cases) -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t) - -> (ssink sinfo v s, (ak, v, clean s t) :: nargs)) + -> (ssink 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 sinfo v s, + -> (ssink v s, (ak, v, clean s t) :: nargs)) (s, []) args in L.rev ncase) cases in - mkInductive (l, label, nargs, ncases) sinfo - | Cons (it, name) -> mkCons (clean s it, name) sinfo + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) -> let s' = L.fold_left - (fun s (_,ov) -> ssink sinfo ov s) + (fun s (_,ov) -> ssink ov s) s cargs in - let s'' = ssink sinfo (l, None) s' in + let s'' = ssink (l, None) s' in (l, cargs, clean s'' e)) cases, match default with | None -> default - | Some (v,e) -> Some (v, clean (ssink sinfo (l, None) (ssink sinfo v s)) e)) sinfo + | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e)) | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e - else clean S.identity (mkSusp e s sinfo) + else clean S.identity (mkSusp e s ) | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with | MVal e -> clean s e - | _ -> mkMetavar (idx, s, name) sinfo + | _ -> mkMetavar (idx, s, name) in clean S.identity e

let sdatacons = Symbol (U.dummy_location, "##datacons") @@ -913,14 +912,14 @@ 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 dummy_sinfo +and lexp_cstring ctx e = lexp_str ctx e

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

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 lexp_str' = lexp_str ctx in + let lexp_stri idt e = lexp_str (add_indent ctx idt) e in

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

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

| 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 sinfo) sinfo + | MVal e -> lexp_str ctx (push_susp e subst ) | _ -> "?" ^ maybename name ^ (subst_string subst ) ^ (index idx))

| Let (_, decls, body) -> @@ -1001,35 +1000,35 @@ and lexp_str ctx (exp : lexp) sinfo : string = else decls in

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

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

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

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

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

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

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

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

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

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

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

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

| Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str' target sinfo) in + let str = (keyword "case ") ^ (lexp_str' target ) in let arg_str arg = List.fold_left (fun str v -> match v with @@ -1065,7 +1064,7 @@ and lexp_str ctx (exp : lexp) sinfo : 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 sinfo)) + "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp )) map str in

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

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

@@ -1103,7 +1102,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 dummy_sinfo)) + -> str ^ " " ^ (lexp_str ctx arg )) str value in str ^ ")") ctors "" @@ -1114,13 +1113,13 @@ 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 dummy_sinfo) ^ ";") else "") in + name ^ " : " ^ (lexp_str' lxp ) ^ ";") 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 dummy_sinfo) ^ ";" ^ sepdecl)::str) + (name ^ " = " ^ (lexp_str' lxp ) ^ ";" ^ sepdecl)::str) [] decls in List.rev ret

@@ -1139,8 +1138,8 @@ let rec eq e1 e2 = | (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 dummy_sinfo) e2 - | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 dummy_sinfo) + | (Susp (e1, s1), _) -> eq (push_susp e1 s1 ) e2 + | (_, Susp (e2, s2)) -> eq e1 (push_susp e2 s2 ) | (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 @@ -1167,16 +1166,16 @@ let rec eq e1 e2 = | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> if i1 == i2 then subst_eq s1 s2 else (match (metavar_lookup i1, metavar_lookup i2) with - | (MVal l, _) -> eq (push_susp l s1 dummy_sinfo) e2 - | (_, MVal l) -> eq e1 (push_susp l s2 dummy_sinfo) + | (MVal l, _) -> eq (push_susp l s1 ) e2 + | (_, MVal l) -> eq e1 (push_susp l s2 ) | _ -> false) | (Metavar (i1, s1, _), _) -> (match metavar_lookup i1 with - | MVal l -> eq (push_susp l s1 dummy_sinfo) e2 + | MVal l -> eq (push_susp l s1 ) e2 | _ -> false) | (_, Metavar (i2, s2, _)) -> (match metavar_lookup i2 with - | MVal l -> eq e1 (push_susp l s2 dummy_sinfo) + | MVal l -> eq e1 (push_susp l s2 ) | _ -> false) | _ -> false with @@ -1191,10 +1190,10 @@ and subst_eq s1 s2 = eq e1 e2 && subst_eq s1 s2 else if o1 > o2 then let o = o1 - o2 in - eq (mkSusp e1 (S.shift o) dummy_sinfo) e2 + eq (mkSusp e1 (S.shift o) ) e2 && subst_eq (S.mkShift s1 o) s2 else let o = o2 - o1 in - eq e1 (mkSusp e2 (S.shift o) dummy_sinfo) + eq e1 (mkSusp e2 (S.shift o) ) && 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) dummy_sinfo) s) defs' + -> lexp_defs_subst l (S.cons (mkLet (l, defs, lexp) ) 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 dummy_sinfo v s + L.ssink 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) dummy_sinfo + mkSusp e (lctx_to_subst lctx)

(** Reduce to weak head normal form. @@ -167,34 +167,34 @@ 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) sinfo : lexp = - let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo: lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + let rec lexp_whnf_aux e (ctx : DB.lexp_context) : 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 sinfo) - | Susp (e, s) -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo - | Call (e, []) -> lexp_whnf_aux e ctx sinfo + | 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 | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with + (match lexp_lexp' (lexp_whnf_aux f ctx ) 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 dummy_sinfo)) dummy_sinfo, - args) dummy_sinfo) - ctx sinfo - | Call (f', xs1) -> mkCall (f', List.append xs1 xs) sinfo + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx )) , + args) ) + ctx + | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | Builtin ((_, name), _) -> (match SMap.find_opt name (!reducible_builtins) with | Some f -> Option.value ~default:e (f ctx args) | None -> e) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf_aux e ctx sinfo in + let e' = lexp_whnf_aux e ctx 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) sinfo : lexp = mkCall (DB.eq_refl, [L.Aerasable, elevel; L.Aerasable, etype; - L.Aerasable, e]) dummy_sinfo in + L.Aerasable, e]) in let reduce it name aargs = - let targs = match lexp_lexp' (lexp_whnf_aux it ctx dummy_sinfo) with + let targs = match lexp_lexp' (lexp_whnf_aux it ctx ) 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) sinfo : lexp = = List.fold_left (fun (s, targs) (_, arg) -> match targs with - | [] -> (S.cons (lexp_whnf_aux arg ctx dummy_sinfo) s, []) + | [] -> (S.cons (lexp_whnf_aux arg ctx ) s, []) | _targ::targs -> (* Ignore the type arguments *) (s, targs)) @@ -222,43 +222,43 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) sinfo : 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 dummy_sinfo) ctx sinfo + lexp_whnf_aux (push_susp branch subst ) ctx 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 dummy_sinfo) ctx sinfo + lexp_whnf_aux (push_susp default subst ) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l {|Unhandled constructor "%s" in case expression|} name; - mkCase (l, e, rt, branches, default) dummy_sinfo in + mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with | Cons (it, (_, name)) -> reduce it name [] | Call (f, aargs) -> - (match lexp_lexp' (lexp_whnf_aux f ctx sinfo) with + (match lexp_lexp' (lexp_whnf_aux f ctx ) with | Cons (it, (_, name)) -> reduce it name aargs - | _ -> mkCase (l, e, rt, branches, default) dummy_sinfo) - | _ -> mkCase (l, e, rt, branches, default) sinfo) + | _ -> mkCase (l, e, rt, branches, default) ) + | _ -> mkCase (l, e, rt, branches, default) ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> lexp_whnf_aux (push_susp e s dummy_sinfo) ctx sinfo + | MVal e -> lexp_whnf_aux (push_susp e s ) ctx | _ -> 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) dummy_sinfo) ctx sinfo + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs) ) ctx

| _elem -> e

- in lexp_whnf_aux e ctx sinfo + in lexp_whnf_aux e ctx

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

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

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 dummy_sinfo, Lexp.push_susp e2 s dummy_sinfo)) + fun (e1, e2) -> (Lexp.push_susp e1 s , Lexp.push_susp e2 s )) 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 dummy_sinfo) d acc + | MVal e -> canon (push_susp e s ) d acc | _ -> add_var_depth (- i) d acc) - | Susp (e, s) -> canon (push_susp e s dummy_sinfo) d acc + | Susp (e, s) -> canon (push_susp e s ) 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 dummy_sinfo in - let tltp = mkSusp etype subst dummy_sinfo in - let tlvl = mkSusp elvl subst dummy_sinfo in + let tlxp = mkSusp target subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst 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)]) dummy_sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) 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 dummy_sinfo)) - ((ak1, (mkVar (vdef1, i) dummy_sinfo))::args) - (ssink dummy_sinfo vdef1 s) + (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s )) + ((ak1, (mkVar (vdef1, i) ))::args) + (ssink 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)) dummy_sinfo, - eaargs) dummy_sinfo) subst dummy_sinfo in - let hlxp = mkCall (ctor, args) dummy_sinfo in + let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) , + eaargs) ) subst in + let hlxp = mkCall (ctor, args) 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) dummy_sinfo in + let hlxp = mkVar ((DB.dloc, None), 0) 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)) dummy_sinfo + -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (_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)) dummy_sinfo (* FIXME: Could be more canonical *) + else mkSortLevel (mkSLlub' (e1, e2)) (* 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) dummy_sinfo) - else let l2' = (mkSusp l2 (S.substitute impossible) dummy_sinfo) in + then SortResult (mkSusp k2 (S.substitute impossible) ) + else let l2' = (mkSusp l2 (S.substitute impossible) ) 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')) dummy_sinfo) + SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2')) ) | (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) dummy_sinfo) + SortResult (mkSusp k2 (S.substitute DB.level0) ) | (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) dummy_sinfo) + -> SortResult (mkSort (l, StypeOmega) ) | _ -> 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 sinfo = +and check'' erased ctx e = 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 sinfo = (lexp_string e) (lexp_string t) (lexp_string t') in let check_type erased ctx t = - let s = check erased ctx t sinfo in + let s = check erased ctx t in (match lexp'_whnf s ctx with | Sort _ -> () | _ @@ -610,21 +610,21 @@ and check'' erased ctx e sinfo = DB.type_int ) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) - -> let t = check erased ctx e sinfo in + -> let t = check erased ctx e 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 sinfo in + -> let t1 = check erased ctx e1 in assert_type ctx e1 t1 DB.type_level; - let t2 = check erased ctx e2 sinfo in + let t2 = check erased ctx e2 in assert_type ctx e2 t2 DB.type_level; DB.type_level | Sort (l, Stype e) - -> let t = check erased ctx e sinfo in + -> let t = check erased ctx e in assert_type ctx e t DB.type_level; - mkSort (l, Stype (mkSortLevel (SLsucc e) dummy_sinfo)) dummy_sinfo + mkSort (l, Stype (mkSortLevel (SLsucc e) )) | 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 sinfo = {|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 dummy_sinfo) sinfo + | Susp (e, s) -> check erased ctx (push_susp e s ) | Let (l, defs, e) -> let _ = List.fold_left (fun ctx (v, _e, t) @@ -657,12 +657,12 @@ and check'' erased ctx e sinfo = (check (if DB.set_mem (n - 1) nerased then DB.set_empty else nerased) - nctx e sinfo) - (push_susp t (S.shift n) dummy_sinfo); + nctx e ) + (push_susp t (S.shift n) ); n - 1) (List.length defs) defs in - mkSusp (check nerased nctx e sinfo) - (lexp_defs_subst l S.identity defs) dummy_sinfo + mkSusp (check nerased nctx e ) + (lexp_defs_subst l S.identity defs) | Arrow (ak, v, t1, loc, t2) -> (let k1 = check_type erased ctx t1 in let nctx = DB.lexp_ctx_cons ctx v Variable t1 in @@ -671,31 +671,31 @@ and check'' erased ctx e sinfo = | SortResult k -> k | SortInvalid -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; - mkSort (loc, StypeOmega) sinfo + mkSort (loc, StypeOmega) | SortK1NotType -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; - mkSort (loc, StypeOmega) sinfo + mkSort (loc, StypeOmega) | SortK2NotType -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; - mkSort (loc, StypeOmega) sinfo) + mkSort (loc, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, l, check (dbset_push ak erased) (DB.lctx_extend ctx v Variable t) - e sinfo) dummy_sinfo) + e ) ) | Call (f, args) - -> let ft = check erased ctx f sinfo in + -> let ft = check erased ctx f in List.fold_left (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) - ctx arg sinfo in + ctx arg 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) dummy_sinfo + mkSusp t2 (S.substitute arg) | _ -> log_tc_error ~loc:(lexp_location arg) "Calling a non functin (type = %s)!" (lexp_string ft); @@ -722,7 +722,7 @@ and check'' erased ctx e sinfo = * cannot refer to the fields! *) (* FIXME: If it does refer, * we get an ugly error! *) - (mkSusp level' (L.sunshift n) sinfo) + (mkSusp level' (L.sunshift n) ) | _tt -> log_tc_error ~loc:(lexp_location t) @@ -737,14 +737,14 @@ and check'' erased ctx e sinfo = (level, ctx, erased, 0) case in level) - cases (mkSortLevel SLz sinfo) in - mkSort (l, Stype level) sinfo + cases (mkSortLevel SLz ) in + mkSort (l, Stype level) | (ak, v, t)::args -> let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, lexp_location t, arg_loop (DB.lctx_extend ctx v Variable t) (dbset_push ak erased) - args) dummy_sinfo in + args) 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 sinfo = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in - let etype = lexp_whnf (check erased ctx e sinfo) ctx in + let etype = lexp_whnf (check erased ctx e ) 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 sinfo = s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased = - 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 tlxp = mkSusp e subst in + let tltp = mkSusp etype subst in + let tlvl = mkSusp elvl subst 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)]) dummy_sinfo in (* Target lexp *) + (L.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) let nerased = dbset_push L.Aerasable nerased in let nctx = DB.lexp_ctx_cons ctx (l, None) Variable eqty in @@ -798,23 +798,23 @@ and check'' erased ctx e sinfo = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s sinfo)) - (ssink dummy_sinfo vdef s) - (mkCall (mkSusp hlxp (S.shift 1) sinfo, [(ak, mkVar (vdef, 0) sinfo)]) sinfo) + (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s )) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1) , [(ak, mkVar (vdef, 0) )]) ) vdefs fieldtypes | _ -> log_tc_error ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp) in let hctor = - mkCall (mkCons (it, (l, name)) sinfo, - List.map (fun (_, a) -> (P.Aerasable, a)) aargs) dummy_sinfo in + mkCall (mkCons (it, (l, name)) , + List.map (fun (_, a) -> (P.Aerasable, a)) aargs) 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 sinfo) - (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) sinfo)) + (check nerased nctx branch ) + (mkSusp ret (S.shift ((List.length fieldtypes) + 1)) )) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -824,11 +824,11 @@ and check'' erased ctx e sinfo = 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) dummy_sinfo in + let hlxp = mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in - assert_type nctx d (check nerased nctx d sinfo) - (mkSusp ret (S.shift 2) dummy_sinfo) + assert_type nctx d (check nerased nctx d ) + (mkSusp ret (S.shift 2) ) | None -> if diff > 0 then @@ -844,22 +844,22 @@ and check'' erased ctx e sinfo = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) dummy_sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) ) :: 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) dummy_sinfo, - indtype fargs (nargs - 1)) dummy_sinfo + mkCall (mkSusp t (S.shift nargs) , + indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) dummy_sinfo in + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) dummy_sinfo in + buildtype fargs) in buildtype fargs with | Not_found @@ -871,9 +871,9 @@ and check'' erased ctx e sinfo = DB.type_int ) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> let e = push_susp e s dummy_sinfo in - check erased ctx e sinfo - | MVar (_, t, _) -> push_susp t s dummy_sinfo) + | MVal e -> let e = push_susp e s in + check erased ctx e + | MVar (_, t, _) -> push_susp t s )

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 dummy_sinfo) + | Susp (e, s) -> fv (push_susp e s ) | 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 dummy_sinfo) + | MVal e -> fv (push_susp e s ) | MVar (sl, t, cl) - -> let (fvs, mvs) = fv_erase (fv (push_susp t s dummy_sinfo)) in + -> let (fvs, mvs) = fv_erase (fv (push_susp t s )) in (fvs, mv_set_add mvs id (sl, t, cl, name))) in let ofvs = LMap.find_opt fv_memo e in @@ -1010,14 +1010,14 @@ and get_type ctx e = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) dummy_sinfo)) dummy_sinfo + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e) )) | 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 dummy_sinfo) + | Susp (e, s) -> get_type ctx (push_susp e s ) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in - mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs) dummy_sinfo + mkSusp (get_type nctx e) (lexp_defs_subst l S.identity defs)

| Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) @@ -1026,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) dummy_sinfo) + | _ -> mkSort (l, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, v, t, l, get_type (DB.lctx_extend ctx v Variable t) - e) dummy_sinfo) + e) ) | 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) dummy_sinfo + -> mkSusp t2 (S.substitute arg) | _ -> ft) ft args | Inductive (l, _label, args, cases) @@ -1059,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) dummy_sinfo) + (mkSusp level' (L.sunshift n) ) | _tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) (level, ctx, 0) case in level) - cases (mkSortLevel SLz dummy_sinfo) in - mkSort (l, Stype level) dummy_sinfo + cases (mkSortLevel SLz ) in + mkSort (l, Stype level) | (ak, v, t)::args -> mkArrow (ak, v, t, lexp_location t, - arg_loop args (DB.lctx_extend ctx v Variable t)) dummy_sinfo in + arg_loop args (DB.lctx_extend ctx v Variable t)) in let tct = arg_loop args ctx in tct | Case (_l, _e, ret, _branches, _default) -> ret @@ -1082,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) dummy_sinfo) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index) ) :: 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) dummy_sinfo, - indtype fargs (nargs - 1)) dummy_sinfo + mkCall (mkSusp t (S.shift nargs) , + indtype fargs (nargs - 1)) | (ak, vd, ftype) :: ftypes -> mkArrow (ak, vd, ftype, lexp_location ftype, - fieldargs ftypes) dummy_sinfo in + fieldargs ftypes) in let rec buildtype fargs = match fargs with | [] -> fieldargs fieldtypes | (_ak, ((l,_) as vd), atype) :: fargs -> mkArrow (P.Aerasable, vd, atype, l, - buildtype fargs) dummy_sinfo in + buildtype fargs) in buildtype fargs 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 dummy_sinfo) - | MVar (_, t, _) -> push_susp t s dummy_sinfo) + | MVal e -> get_type ctx (push_susp e s ) + | MVar (_, t, _) -> push_susp t s )

(* FIXME: Remove the mutual recursion between `lexp_whnf` and `get_type`, and move this closer to the `lexp_whnf`. *) @@ -1149,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) dummy_sinfo) + -> erase_type lctx (L.push_susp body (S.substitute erasure_dummy) )

| L.Lambda (_, vdef, ty, body) -> let lctx' = DB.lctx_extend lctx vdef Variable ty in @@ -1167,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 dummy_sinfo) + | L.Susp (l, s) -> erase_type lctx (L.push_susp l s )

(* To be thrown out *) | L.Arrow _ -> E.Type lxp @@ -1178,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 dummy_sinfo) + | MVal e -> erase_type lctx (push_susp e s ) | MVar _ -> Log.internal_error "Metavar in erase_type")

and clean_arg lctx = function @@ -1195,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) dummy_sinfo in + -> let lxp' = L.push_susp lxp (S.substitute erasure_dummy) in Some (v, erase_type lctx lxp') | None -> None

@@ -1209,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 dummy_sinfo var subst) lctx' + clean_arg_list tl (var :: acc) (ssink 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 dummy_sinfo)) + (l, eargs, erase_type lctx' (L.push_susp expr subst )) in SMap.map clean_branch cases

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

| Lexp.Var _ (*

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

let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location +let dummy_sinfo = epsilon dummy_location + (********************** 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) dummy_sinfo) (mkSusp le2 (S.shift o2) dummy_sinfo) + && OL.conv_p ctx (mkSusp le1 (S.shift o1) ) (mkSusp le2 (S.shift o2) ) 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) dummy_sinfo, + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0) , 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) dummy_sinfo, + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0) , S.Identity 1, o2')) o1 o2 o | (S.Identity o1', S.Cons _) - -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) dummy_sinfo, + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0) , 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' dummy_sinfo - | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' dummy_sinfo + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2'

(* 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) sinfo +and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : 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 sinfo in - match Inverse_subst.apply_inv_subst lxp s sinfo with + | MVar (_, t, _) -> push_susp t s in + match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible -> log_info "Unification of metavar failed:\n ?[%s]\nAgainst:\n %s\n" @@ -363,12 +363,12 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) sinfo "`lexp_whnf` returned an instantiated metavar!!" | (Some s_inv, MVar (sl, t, clen)) -> let clen' = clen - s_offset s in - let t' = mkSusp t s_inv sinfo in + let t' = mkSusp t s_inv in let newmv = create_metavar_1 sl t' clen' in - let lexp = mkMetavar (newmv, s, name) sinfo in + let lexp = mkMetavar (newmv, s, name) in assert (sl <= clen); assert (sl <= clen'); - assert (OL.conv_p ctx (mkSusp t' s sinfo) t); + assert (OL.conv_p ctx (mkSusp t' s ) t); (* if (OL.conv_p ctx (mkSusp lexp s1) (mkSusp lexp s2)) then * print_string ("common_subset successful:\n " * ^ subst_string s

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