Stefan pushed to branch master at Stefan / Typer

Commits: f33ba8a5 by Stefan Monnier at 2016-08-28T22:27:46-04:00 * btl/types.typer (length, head, tail): Make type erasable

* src/opslexp.ml (erase_type): Adjust indices after removing an erasable formal argument.

- - - - -

2 changed files:

- btl/types.typer - src/opslexp.ml

Changes:

===================================== btl/types.typer ===================================== --- a/btl/types.typer +++ b/btl/types.typer @@ -71,22 +71,22 @@ List = inductive_ (dList (a : Type)) (nil) (cons a (List a)); nil = inductive-cons List nil; cons = inductive-cons List cons;

-length : (a : Type) => List a -> Int; -length = lambda a => +length : (a : Type) ≡> List a -> Int; +length = lambda a ≡> lambda xs -> case xs | nil => 0 | cons hd tl => (1 + (length(a := a) tl));

-head : (a : Type) => List a -> a; -head = lambda a => +head : (a : Type) ≡> List a -> a; +head = lambda a ≡> lambda xs -> case xs | nil => nil | cons hd tl => hd;

-tail : (a : Type) => List a -> List a; -tail = lambda a => +tail : (a : Type) ≡> List a -> List a; +tail = lambda a ≡> lambda xs -> case xs | nil => nil

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -327,11 +327,12 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Var(v) -> E.Var(v) | L.Cons(_, s) -> E.Cons(s)

- | L.Lambda(kind, vdef, _, body) -> - if kind != P.Aerasable then - E.Lambda(vdef, erase_type body) - else - erase_type body + | L.Lambda (P.Aerasable, _, _, body) -> + (* The var shouldn't appear in body, basically, but we need + * to adjust the debruijn indices of other vars, hence the subst. *) + erase_type (L.push_susp body (S.substitute Builtin.type0)) + | L.Lambda (_, vdef, _, body) -> + E.Lambda (vdef, erase_type body)

| L.Let(l, decls, body) -> E.Let(l, (clean_decls decls), (erase_type body)) @@ -349,7 +350,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Arrow _ -> E.Type | L.SortLevel _ -> E.Type | L.Sort _ -> E.Type - (* Still useful to some extend *) + (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Inductive(l, label)

and filter_arg_list lst =

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