Stefan pushed to branch master at Stefan / Typer

Commits: 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function

* src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it.

- - - - -

4 changed files:

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

Changes:

===================================== src/elab.ml ===================================== @@ -1520,8 +1520,7 @@ let rec sform_lambda kind ctx loc sargs ot = * in order to account for the fact that `arg` and `v` * might not be the same name! *) | Some lt2 - -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in - Some (mkSusp lt2 s) in + -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with

===================================== src/lexp.ml ===================================== @@ -295,6 +295,15 @@ and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) s l v 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. + * This should probably be made into a no-op, but only after we get rid + * of the check in DB.lookup that a `Var` has the same name as the + * one stored in the lctx! + * Using DeBruijn *should* make α-renaming unnecessary + * so this is a real PITA! :-( *) +let srename name le = mkSusp le (S.cons (mkVar (name, 0)) (S.shift 1)) + (* Shift by a negative amount! *) let rec sunshift n = if n = 0 then S.identity

===================================== src/opslexp.ml ===================================== @@ -277,7 +277,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') - t12 t22 + 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)

===================================== src/unification.ml ===================================== @@ -232,7 +232,7 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) - @(unify' lexp1 lexp2 + @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, arrow, lxp)]

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