Simon Génier pushed to branch no-non-recusive-decl at Stefan / Typer

Commits: 38b35061 by Simon Génier at 2021-03-13T16:25:43-05:00 Avoid putting a non-recursive decl in the lctx.

- - - - -

6 changed files:

- src/debruijn.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/debruijn.ml ===================================== @@ -201,39 +201,43 @@ let senv_lookup (name: string) (ctx: elab_context): int =

senv_lookup_fail (get_related_names n name map)

-let lexp_ctx_cons (ctx : lexp_context) d v t = - assert (let offset = match v with | LetDef (o, _) -> o | _ -> 0 in +let lctx_extend + (ctx : lexp_context) + (name : vname) + (binding : varbind) + (ty : lexp) + : lexp_context = + + assert (let offset = match binding with | LetDef (o, _) -> o | _ -> 0 in offset >= 0 && (ctx = M.nil - || match M.car ctx with - | (_, LetDef (previous_offset, _), _) - -> previous_offset >= 0 (* General constraint. *) - (* Either `ctx` is self-standing (doesn't depend on us), - * or it depends on us (and maybe other bindings to come), in - * which case we have to depend on the exact same bindings. *) - && (previous_offset <= 1 - || previous_offset = 1 + offset) - | _ -> true)); - M.cons (d, v, t) ctx - -let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) = - lexp_ctx_cons ctx def v t + || match M.car ctx with + | (_, LetDef (previous_offset, _), _) + -> previous_offset >= 0 (* General constraint. *) + (* Either `ctx` is self-standing (doesn't depend on us), + * or it depends on us (and maybe other bindings to come), in + * which case we have to depend on the exact same bindings. *) + && (previous_offset <= 1 + || previous_offset = 1 + offset) + | _ -> true)); + M.cons (name, binding, ty) ctx

let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = let (_loc, oname) = def in let (grm, (n, map), env, sl) = ctx in let nmap = match oname with None -> map | Some name -> SMap.add name n map in (grm, (n + 1, nmap), - lexp_ctx_cons env def v t, + lctx_extend env def v t, sl)

-let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t +let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = + env_extend_rec ctx def v t

let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) = let (ctx, _) = List.fold_left (fun (ctx, recursion_offset) (def, e, t) -> - lexp_ctx_cons ctx def (LetDef (recursion_offset, e)) t, + lctx_extend ctx def (LetDef (recursion_offset, e)) t, recursion_offset - 1) (ctx, List.length defs) defs in ctx @@ -400,24 +404,24 @@ let env_lookup_expr ctx (v : vref): lexp option =

type lct_view = | CVempty - | CVlet of vname * varbind * ltype * lexp_context - | CVfix of (vname * lexp * ltype) list * lexp_context + | CVvar of vname * ltype * lexp_context + | CVdefs of (vname * lexp * ltype) list * lexp_context

-let lctx_view lctx = +let lctx_view (lctx : lexp_context) : lct_view = match lctx with | Myers.Mnil -> CVempty | Myers.Mcons ((loname, LetDef (1, def), t), lctx, _, _) -> let rec loop i lctx defs = - match lctx with - | Myers.Mcons ((loname, LetDef (o, def), t), lctx, _, _) - when o = i - -> loop (i + 1) lctx ((loname, def, t) :: defs) - | _ -> CVfix (defs, lctx) in - loop 2 lctx [(loname, def, t)] - | Myers.Mcons ((_, LetDef (o, _def), _), _, _, _) when o > 1 + match lctx with + | Myers.Mcons ((loname, LetDef (o, def), t), lctx, _, _) + when o = i + -> loop (i + 1) lctx ((loname, def, t) :: defs) + | _ -> CVdefs (defs, lctx) in + loop 2 lctx [(loname, def, t)] + | Myers.Mcons ((_, LetDef (o, _), _), _, _, _) when o > 1 -> fatal "Unexpected lexp_context shape!" - | Myers.Mcons ((loname, odef, t), lctx, _, _) - -> CVlet (loname, odef, t, lctx) + | Myers.Mcons ((loname, _, t), lctx, _, _) + -> CVvar (loname, t, lctx)

(** Sets of DeBruijn indices **)

===================================== src/elab.ml ===================================== @@ -191,16 +191,22 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ~loc "Type check error: ¡¡ctx_define error!!"

-let ctx_extend (ctx: elab_context) (var : vname) def ltype = +let ectx_extend + (ctx : elab_context) + (var : vname) + (def : varbind) + (ltype : lexp) + : elab_context = + elab_check_proper_type ctx ltype var; - ectx_extend ctx var def ltype + DB.ectx_extend ctx var def ltype

-let ctx_define (ctx: elab_context) var lxp ltype = - elab_check_def ctx var lxp ltype; - ectx_extend ctx var (LetDef (0, lxp)) ltype +let ectx_extend_rec + (ectx : elab_context) + (decls : ldecls) + : elab_context =

-let ctx_define_rec (ctx: elab_context) decls = - let nctx = ectx_extend_rec ctx decls in + let nctx = DB.ectx_extend_rec ectx decls in let _ = List.fold_left (fun n (var, _lxp, ltp) -> elab_check_proper_type nctx (push_susp ltp (S.shift n)) var; @@ -649,7 +655,7 @@ and unify_with_arrow ctx tloc lxp kind var aty = let arg = match aty with | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) tloc | Some laty -> laty in - let nctx = ectx_extend ctx var Variable arg in + let nctx = DB.ectx_extend ctx var Variable arg in let body = newMetatype (ectx_to_lctx nctx) (ectx_to_scope_level ctx) tloc in let (l, _) = var in let arrow = mkArrow (kind, var, arg, l, body) in @@ -785,12 +791,12 @@ and check_case rtype (loc, target, ppatterns) ctx = (Aerasable, tltp'); (* Inductive type *) (Anormal, head_lexp); (* Lexp of the branch head *) (Anormal, tlxp')]) (* Target lexp *) - in ctx_extend nctx (loc, None) Variable eqty + in ectx_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 nctx = ectx_extend ctx v Variable tltp 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 @@ -806,7 +812,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | Lambda (Aerasable, v, t, body) -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) v t in - let nctx = ctx_extend ctx v Variable t in + let nctx = ectx_extend ctx v Variable t in let body = inst_args nctx body in mkSusp body (S.substitute arg) | _e -> lxp in @@ -848,7 +854,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | (_, (ak, (_, Some fname), fty)::cargs) when SMap.mem fname pe -> let var = SMap.find fname pe in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + let nctx = ectx_extend ctx var Variable (mkSusp fty s) in make_nctx nctx (ssink var s) pargs cargs (SMap.remove fname pe) ((ak, var)::acc) @@ -856,7 +862,7 @@ and check_case rtype (loc, target, ppatterns) ctx = when (match (ef, ak) with | (Some (_, "_"), _) | (None, Anormal) -> true | _ -> false) - -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + -> let nctx = ectx_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) @@ -865,7 +871,7 @@ and check_case rtype (loc, target, ppatterns) ctx = make_nctx ctx s pargs cargs (SMap.add fname var pe) acc | pargs, (ak, fname, fty)::cargs -> let var = (loc, None) in - let nctx = ctx_extend ctx var Variable (mkSusp fty s) in + let nctx = ectx_extend ctx var Variable (mkSusp fty s) in if ak = Anormal then sexp_error loc ("Missing pattern for normal field" @@ -1027,7 +1033,7 @@ and lexp_parse_inductive ctors ctx = loop altacc' | (kind, var, exp)::tl -> let lxp = infer_type exp ctx var in - let nctx = ectx_extend ctx var Variable lxp in + let nctx = DB.ectx_extend ctx var Variable lxp in loop tl ((kind, var, lxp)::acc) nctx in loop args [] nctx in

@@ -1150,7 +1156,7 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) | _ -> Log.internal_error "Defining same slot!") defs (IMap.empty) in let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in - decls, ctx_define_rec ectx decls + decls, ectx_extend_rec ectx decls

and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in @@ -1263,7 +1269,7 @@ and lexp_decls_1 pending_defs then (error ~loc ("Variable `" ^ vname ^ "` already defined!"); recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) + else recur [] (DB.ectx_extend nctx (loc, Some vname) ForwardRef ltp) (SMap.add vname loc pending_decls) pending_defs | _ -> error ~loc ("Invalid type declaration syntax : `" ^ @@ -1282,8 +1288,9 @@ and lexp_decls_1 let var = (l, Some vname) in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, - ctx_define nctx var lexp ltp + let lexp' = mkSusp lexp (S.shift 1) in + let ectx' = ectx_extend_rec nctx [(var, lexp', ltp)] in + ([(var, lexp', ltp)], sdecls, toks, ectx')

| [Symbol (l, vname); sexp] -> if SMap.mem vname pending_decls then @@ -1464,7 +1471,7 @@ let sform_typecons ctx loc sargs _ot = (ectx_to_scope_level ctx) l in

parse_formals sformals ((kind, var, ltp) :: rformals) - (ectx_extend ctx var Variable ltp) in + (DB.ectx_extend ctx var Variable ltp) in

let (formals, nctx) = parse_formals formals [] ctx in

@@ -1501,7 +1508,7 @@ let sform_arrow kind ctx loc sargs _ot = | Node (Symbol (_, "_:_"), [Symbol v; st1]) -> (elab_p_id v, st1) | _ -> ((sexp_location st1, None), st1) in let lt1 = infer_type st1 ctx v in - let nctx = ectx_extend ctx v Variable lt1 in + let nctx = DB.ectx_extend ctx v Variable lt1 in let lt2 = infer_type st2 nctx (sexp_location st2, None) in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; @@ -1612,7 +1619,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> None in

let mklam lt1 olt2 = - let nctx = ectx_extend ctx arg Variable lt1 in + let nctx = DB.ectx_extend ctx arg Variable lt1 in let olt2 = match olt2 with | None -> None (* Apply a "dummy" substitution which replace #0 with #0 @@ -1651,7 +1658,7 @@ let rec sform_lambda kind ctx loc sargs ot = -> (* FIXME: Here we end up adding a local variable `v` whose * name is not lexically present, so there's a risk of * name capture. We should make those vars anonymous? *) - let nctx = ectx_extend ctx v Variable lt1 in + let nctx = DB.ectx_extend ctx v Variable lt1 in (* 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 @@ -1875,8 +1882,9 @@ let default_ectx (* Empty context *) let lctx = empty_elab_context in let lctx = SMap.fold (fun key (e, t) ctx - -> if String.get key 0 = '-' then ctx - else ctx_define ctx (dloc, Some key) e t) + -> if String.get key 0 = '-' + then ctx + else ectx_extend_rec ctx [(dloc, Some key), e, t]) (!BI.lmap) lctx in

Heap.register_builtins ();

===================================== src/eval.ml ===================================== @@ -1143,17 +1143,10 @@ let from_lctx (lctx: lexp_context): runtime_env = let rec from_lctx' (lctx: lexp_context): runtime_env = match lctx_view lctx with | CVempty -> Myers.nil - | CVlet (loname, def, _, lctx) + | CVvar (loname, _, lctx) -> let rctx = from_lctx lctx in - Myers.cons (loname, - ref (match def with - | LetDef (_, e) - -> if closed_p rctx (OL.fv e) then - eval (OL.erase_type lctx e) rctx - else Vundefined - | _ -> Vundefined)) - rctx - | CVfix (defs, lctx) + Myers.cons (loname, ref Vundefined) rctx + | CVdefs (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) -> OL.fv_union fvs (OL.fv e)) @@ -1166,11 +1159,12 @@ let from_lctx (lctx: lexp_context): runtime_env = let nrctx = Myers.cons (loname, rc) rctx in (nrctx, (e, rc)::evs, alldefs)) (rctx, [], true) defs in + let lctx' = lctx_extend_rec lctx defs in let _ = (* FIXME: Evaluate those defs that we can, even if not all defs * are present! *) if alldefs && closed_p rctx (OL.fv_hoist (List.length defs) fvs) then - List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx e) nrctx) evs + List.iter (fun (e, rc) -> rc := eval (OL.erase_type lctx' e) nrctx) evs else () in nrctx and from_lctx lctx =

===================================== src/lexp.ml ===================================== @@ -118,6 +118,7 @@ type ltype = lexp | SLlub of lexp * lexp

type ldecl = vname * lexp * ltype +type ldecls = ldecl list

type varbind = | Variable

===================================== src/opslexp.ml ===================================== @@ -112,17 +112,14 @@ let rec lexp_defs_subst l s defs = match defs with let rec lctx_to_subst lctx = match DB.lctx_view lctx with | DB.CVempty -> Subst.identity - | DB.CVlet (_, LetDef (_, e), _, lctx) - -> let s = lctx_to_subst lctx in - L.scompose (S.substitute e) s - | DB.CVlet (v, _, _, lctx) + | DB.CVvar (v, _, lctx) -> let s = lctx_to_subst lctx in (* Here we decide to keep those vars in the target domain. * Another option would be to map them to `L.impossible`, * hence making the target domain be empty (i.e. making the substitution * generate closed results). *) L.ssink v s - | DB.CVfix (defs, lctx) + | DB.CVdefs (defs, lctx) -> let s1 = lctx_to_subst lctx in let s2 = lexp_defs_subst DB.dloc S.identity (List.rev defs) in @@ -352,14 +349,14 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Var (_, v1), Var (_, v2)) -> v1 = v2 | (Arrow (ak1, vd1, t11, _, t12), Arrow (ak2, _vd2, t21, _, t22)) -> ak1 == ak2 - && conv_p t11 t21 - && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') - t12 (srename vd1 t22) + && conv_p t11 t21 + && conv_p' (DB.lctx_extend ctx vd1 Variable t11) (set_shift vs') + t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, _l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) - && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs') - e1 e2 + && conv_p' (DB.lctx_extend ctx l1 Variable t1) + (set_shift vs') + e1 e2 | (Call (f1, args1), Call (f2, args2)) -> let conv_arglist_p args1 args2 : bool = List.fold_left2 @@ -374,9 +371,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | ([], []) -> true | ((ak1,vd1,t1)::fields1, (ak2,_vd2,t2)::fields2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1) - (set_shift vs) - fields1 fields2 + && conv_fields (DB.lctx_extend ctx vd1 Variable t1) + (set_shift vs) + fields1 fields2 | _,_ -> false in let rec conv_args ctx vs args1 args2 = match args1, args2 with @@ -386,9 +383,9 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = SMap.equal (conv_fields ctx vs) cases1 cases2 | ((ak1,l1,t1)::args1, (ak2,_l2,t2)::args2) -> ak1 == ak2 && conv_p' ctx vs t1 t2 - && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1) - (set_shift vs) - args1 args2 + && conv_args (DB.lctx_extend ctx l1 Variable t1) + (set_shift vs) + args1 args2 | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 @@ -433,7 +430,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = (L.Aerasable, tltp); (* Inductive type *) (L.Anormal, hlxp); (* Lexp of the branch head *) (L.Anormal, tlxp)]) in (* Target lexp *) - DB.lexp_ctx_cons ctx (DB.dloc, None) Variable eqty in + DB.lctx_extend 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 from the inductive. Instead, we work with the lists of @@ -449,7 +446,7 @@ 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)) + (DB.lctx_extend ctx vdef1 Variable (mkSusp ftype s)) ((ak1, (mkVar (vdef1, i)))::args) (ssink vdef1 s) (i - 1) @@ -658,23 +655,25 @@ and check'' erased ctx e = (List.length defs) defs in mkSusp (check nerased nctx e) (lexp_defs_subst l S.identity defs) + | Arrow (ak, v, t1, l, t2) -> (let k1 = check_type erased ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in - let k2 = check_type (DB.set_sink 1 erased) nctx t2 in - match sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> k - | SortInvalid - -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; - mkSort (l, StypeOmega) - | SortK1NotType - -> (error_tc ~loc:(lexp_location t1) - "Not a proper type"; - mkSort (l, StypeOmega)) - | SortK2NotType - -> (error_tc ~loc:(lexp_location t2) - "Not a proper type"; - mkSort (l, StypeOmega))) + let nctx = DB.lctx_extend ctx v Variable t1 in + let k2 = check_type (DB.set_sink 1 erased) nctx t2 in + match sort_compose ctx nctx l ak k1 k2 with + | SortResult k -> k + | SortInvalid + -> error_tc ~loc:l "Invalid arrow: inner TypelLevel argument"; + mkSort (l, StypeOmega) + | SortK1NotType + -> (error_tc ~loc:(lexp_location t1) + "Not a proper type"; + mkSort (l, StypeOmega)) + | SortK2NotType + -> (error_tc ~loc:(lexp_location t2) + "Not a proper type"; + mkSort (l, StypeOmega))) + | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in mkArrow (ak, v, t, l, @@ -785,7 +784,7 @@ and check'' erased ctx e = (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 + let nctx = DB.lctx_extend ctx (l, None) Variable eqty in (nerased, nctx) in SMap.iter (fun name (l, vdefs, branch) @@ -797,10 +796,10 @@ and check'' erased ctx e = * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) - (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (ssink vdef s) - (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) - vdefs fieldtypes + (DB.lctx_extend ctx vdef Variable (mkSusp ftype s)) + (ssink vdef s) + (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))])) + vdefs fieldtypes | _,_ -> (error_tc ~loc:l "Wrong number of args to constructor!"; (erased, ctx, hlxp)) in @@ -1016,14 +1015,16 @@ and get_type ctx e = | 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) + | Arrow (ak, v, t1, l, t2) (* FIXME: Use `check` here but silencing errors? *) -> (let k1 = get_type ctx t1 in - let nctx = DB.lexp_ctx_cons ctx v Variable t1 in - let k2 = get_type nctx t2 in - match sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> k - | _ -> mkSort (l, StypeOmega)) + let nctx = DB.lctx_extend ctx v Variable t1 in + let k2 = get_type nctx t2 in + match sort_compose ctx nctx l ak k1 k2 with + | SortResult k -> k + | _ -> mkSort (l, StypeOmega)) + | Lambda (ak, ((l,_) as v), t, e) -> (mkArrow (ak, v, t, l, get_type (DB.lctx_extend ctx v Variable t) @@ -1252,8 +1253,8 @@ let ctx2tup ctx nctx = let rec get_blocs nctx blocs = if nctx == ctx then blocs else match DB.lctx_view nctx with - | DB.CVlet (_, _, _, nctx) as bloc -> get_blocs nctx (bloc :: blocs) - | DB.CVfix (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) + | DB.CVvar (_, _, nctx) as bloc -> get_blocs nctx (bloc :: blocs) + | DB.CVdefs (_, nctx) as bloc -> get_blocs nctx (bloc :: blocs) | _ -> assert false in let rec mk_lets_and_tup blocs types = let loc = U.dummy_location in @@ -1285,17 +1286,14 @@ let ctx2tup ctx nctx = List.mapi (fun i (oname, _t) -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) - | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> mkLet (loc, [(name, mkSusp e (S.shift 1), t)], - mk_lets_and_tup blocs ((name, t) :: types)) - | (DB.CVfix (defs, _) :: blocs) + | (DB.CVdefs (defs, _) :: blocs) -> mkLet (loc, defs, - mk_lets_and_tup blocs (List.append - (List.rev - (List.map (fun (oname, _, t) - -> (oname, t)) - defs)) - types)) + mk_lets_and_tup blocs (List.append + (List.rev + (List.map (fun (oname, _, t) + -> (oname, t)) + defs)) + types)) | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []

===================================== src/unification.ml ===================================== @@ -267,7 +267,7 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) @(unify' lexp1 (srename v1 lexp2) - (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (DB.lctx_extend ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)] @@ -282,10 +282,11 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then (unify' ltype1 ltype2 ctx vs) - @(unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) + then + (unify' ltype1 ltype2 ctx vs) + @ (unify' lexp1 lexp2 + (DB.lctx_extend ctx v1 Variable ltype1) + (OL.set_shift vs)) else [(CKimpossible, ctx, lambda, lxp)] | (_, _) -> [(CKimpossible, ctx, lambda, lxp)]

@@ -576,10 +577,10 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 = (ctx, vs, [(CKimpossible, ctx, e1, e2)]) else List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, _v2, t2)) - -> (DB.lexp_ctx_cons ctx v1 Variable t1, - OL.set_shift vs, - if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] - else (unify' t1 t2 ctx vs) @ residue)) + -> (DB.lctx_extend ctx v1 Variable t1, + OL.set_shift vs, + if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] + else (unify' t1 t2 ctx vs) @ residue)) (ctx, vs, []) (List.combine args1 args2) in let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in

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