Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer
Commits: 61f50b42 by Soilih BEN SOILIH at 2021-11-14T21:22:37-05:00 fixing p.m in opslexp
- - - - -
1 changed file:
- src/opslexp.ml
Changes:
===================================== src/opslexp.ml ===================================== @@ -926,6 +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) + | Proj (l,lxp,lbl) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1014,6 +1015,7 @@ and get_type ctx e = | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, _name), _idx) as v) -> lookup_type ctx v + | Proj (l,lxp,lbl) -> get_type ctx lxp | Susp (e, s) -> get_type ctx (push_susp e s) | Let (l, defs, e) -> let nctx = DB.lctx_extend_rec ctx defs in @@ -1145,6 +1147,7 @@ let rec erase_type (lctx : DB.lexp_context) (lxp: lexp) : E.elexp = | L.Imm (s) -> E.Imm (s) | L.Builtin (v, _) -> E.Builtin (v) | L.Var (v) -> E.Var (v) + | L.Proj (l,lxp,lbl) -> erase_type lctx lxp | L.Cons (ty, s) -> E.Cons (arity_of_cons lctx ty s, s)
| L.Lambda (P.Aerasable, _, _, body)
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/61f50b4202e0c8fa583d914bd5247e5633...