Stefan pushed to branch master at Stefan / Typer

Commits: 71ec8850 by Stefan Monnier at 2019-10-22T20:41:34Z * src/elab.ml (sform_lambda): Rename the type's var

This should fix some deBruijn errors for cases like:

x : (y : T1) -> T2 y; x z = e;

since the (dependent) type of `e` will use the name `z` rather than `y`. Apparently it doesn't fix all our deBruijn name check errors, tho :-(

* sample/hurkens.typer: Unrelated cosmetic changes.

- - - - - c3706c38 by Stefan Monnier at 2019-10-22T20:45:23Z Merge branch 'master' of gitlab.com:monnier/typer into trunk

- - - - -

2 changed files:

- samples/hurkens.typer - src/elab.ml

Changes:

===================================== samples/hurkens.typer ===================================== @@ -15,16 +15,16 @@ ⊥ : Type; ⊥ = (p : Type) ≡> p;

-¬ : Type -> Type; +¬ : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ; ¬ t = t -> ⊥;

* = Type; -\square = Type1; +□ = Type1;

%% 𝓅 is the "powerset". %% 𝓅 S = (S -> *); FIXME: internal error! -𝓅 : \square -> \square; -𝓅 (S : \square) = (S -> Type); +𝓅 : □ -> □; +𝓅 (S : □) = (S -> *); 𝓅𝓅 S = 𝓅 (𝓅 S);

%%%% A "powerful" universe (U, σ, τ). @@ -38,11 +38,11 @@ %% %% where * is ...

-U : \square; -U = (X : \square) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule! +U : □; +U = (X : □) ≡> (𝓅𝓅 X -> X) -> 𝓅𝓅 X; % Uses the (▵,□,□) rule!

τ : 𝓅𝓅 U -> U; -τ t = lambda (X : \square) +τ t = lambda (X : □) ≡> lambda (f : (𝓅𝓅 X) -> X) -> lambda (p : 𝓅 X) -> t (lambda (y : U) -> p (f ((y (X := X) f)))); @@ -91,5 +91,10 @@ boom2 = lambda (p : 𝓅 U) %%boom : ⊥; %%boom = boom1 boom2;

+%% Summary: +%% U = (X : □) ≡> (𝓅𝓅 X → X) → 𝓅𝓅 X +%% Δ .. (y : U) = (p : U → *) ≡> σ y p → p (τσ y) +%% wf = (p : U → *) ≡> ((y : U) ≡> σ y p → p y) → p Ω +

%%% hurkens.typer ends here.

===================================== src/elab.ml ===================================== @@ -1466,6 +1466,14 @@ let rec sform_lambda kind ctx loc sargs ot =

let mklam lt1 olt2 = let nctx = ectx_extend ctx arg Variable lt1 in + let olt2 = match olt2 with + | None -> None + (* Apply a "dummy" substitution which replace #0 with #0 + * 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 let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with @@ -1566,7 +1574,7 @@ let sform_debruijn ctx loc sargs ot = match sargs with | [Integer (l,i)] -> if i < 0 || i > get_size ctx then - (sexp_error l "##DeBruijn indiex out of bounds"; + (sexp_error l "##DeBruijn index out of bounds"; sform_dummy_ret ctx loc) else let lxp = mkVar ((loc, None), i) in (lxp, Lazy)

View it on GitLab: https://gitlab.com/monnier/typer/compare/b948d4c96126d1eb4796088bc80654647e7...