Stefan pushed to branch master at Stefan / Typer

Commits: e3a0fe68 by Stefan Monnier at 2019-09-13T18:31:03Z Avoid using Inverse_subst in core type checking

* src/lexp.ml (mkSLlub', mkSLsucc): New constructors with sanity checks. (sunshift): New function. * src/opslexp.ml (check'', get_type): Use it instead of Inverse_subst.

- - - - -

6 changed files:

- src/debruijn.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/subst.ml

Changes:

===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -85,8 +85,8 @@ let sort_level = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) let level0 = mkSortLevel SLz -let level1 = mkSortLevel (SLsucc level0) -let level2 = mkSortLevel (SLsucc level1) +let level1 = mkSortLevel (mkSLsucc level0) +let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2)

===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -297,8 +297,8 @@ let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (loop e1, loop e2)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e @@ -1526,7 +1526,7 @@ let sform_type ctx loc sargs ot = match sargs with | [l] -> let l, _ = infer l ctx in (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) + Inferred (mkSort (loc, Stype (SortLevel (mkSLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc

===================================== src/inverse_subst.ml ===================================== @@ -251,9 +251,10 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (apply_inv_subst e s)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (SLlub (apply_inv_subst e1 s, apply_inv_subst e2 s)) + (* Should we use mkSLlub? *) + -> mkSortLevel (mkSLlub' (apply_inv_subst e1 s, apply_inv_subst e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) | Sort (l, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e

===================================== src/lexp.ml ===================================== @@ -205,6 +205,21 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es))

+let mkSLlub' (e1, e2) = match (e1, e2) with + | (SortLevel SLz, _) | (_, SortLevel SLz) + -> U.msg_fatal "internal" U.dummy_location "lub of SLz" + | (SortLevel (SLsucc _), SortLevel (SLsucc _)) + -> U.msg_fatal "internal" U.dummy_location "lub of two SLsucc" + | ((SortLevel _ | Var _ | Metavar _ | Susp _), + (SortLevel _ | Var _ | Metavar _ | Susp _)) + -> SLlub (e1, e2) + | _ -> U.msg_fatal "internal" U.dummy_location "SLlub of non-level" + +let mkSLsucc e = match e with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> U.msg_fatal "internal" U.dummy_location "SLsucc of non-level" + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -260,6 +275,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))

+(* Shift by a negative amount! *) +let rec sunshift n = + if n = 0 then S.identity + else (assert (n >= 0); + S.cons impossible (sunshift (n - 1))) + +let _ = assert (S.identity (* Sanity check! *) + = scompose (S.shift 5) (sunshift 5)) + (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence cound be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify @@ -316,8 +340,9 @@ let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (mkSusp e1 s, mkSusp e2 s)) + | SortLevel (SLsucc e') -> mkSortLevel (mkSLsucc (mkSusp e' s)) + | SortLevel (SLlub (e1, e2)) + -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -381,8 +406,10 @@ let clean e = let rec clean s e = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (clean s e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (clean s e1, clean s e2)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) + | SortLevel (SLlub (e1, e2)) + (* FIXME: The new SLlub could have `succ` on both sides! *) + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (l, _) -> e | Builtin _ -> e

===================================== src/opslexp.ml ===================================== @@ -332,7 +332,7 @@ let rec mkSLlub ctx e1 e2 = let ce2 = level_canon (L.clean e2') in if level_leq ce1 ce2 then e1 else if level_leq ce2 ce1 then e2 - else mkSortLevel (SLlub (e1, e2)) + else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)

type sort_compose_result = SortResult of ltype @@ -535,10 +535,9 @@ let rec check'' erased ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* FIXME: We shouldn't use Inverse_subst - * in the plain `check` code! *) - (Inverse_subst.apply_inv_subst level' - (S.shift n)) + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -789,7 +788,7 @@ let rec get_type ctx e = | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (SLsucc e))) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, name), idx) as v) -> lookup_type ctx v @@ -835,9 +834,9 @@ let rec get_type ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (try Inverse_subst.apply_inv_subst level' - (S.shift n) - with _ -> level) + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) | tt -> level), DB.lctx_extend ictx v Variable t, n + 1))

===================================== src/subst.ml ===================================== @@ -159,7 +159,7 @@ let mkShift s (m:db_offset) = * context ΔₛΔₜ where Δₜ has size M. *) let shift (m:db_offset) = Identity m

-(* Return a substitution which replaces #0 with `e` and the applies `s` +(* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) let cons e s = Cons (e, s, 0)

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