Stefan pushed to branch master at Stefan / Typer

Commits: c25f821e by Stefan Monnier at 2019-07-24T01:56:09Z * src/subst.ml (subst): Fold a `Shift` into the `Identity`.

Generalize `Identity` with `Identity o` where the old `Identity` is now `Identity 0` and `Identity o` is like the old `Shift (Identity, o)`.

(mkShift): Use `Identity` when possible. (shift): Use `Identity`. (identity): Adjust to new `Identity`. (lookup, identity_p, compose): Generalize to the new `Identity o`. (substitute): Use `identity`.

* src/elab.ml (newMetavar): Use S.identity.

* src/inverse_subst.ml (is_identity): Take advantage of the new `Identity o`. (shift_inv_subst): Optimize the case when n is 0. (transfo, invertible, lookup_inv_subst, compose_inv_subst): Generalize to the new `Identity o`.

* src/lexp.ml (subst_string): Handle the new `Identity o`. (subst_eq): Generalize to the new `Identity o`.

* tests/inverse_test.ml (is_identity): Copy new def from inverse_subst.ml.

* tests/unify_test.ml (generate_testable): Use `identity`.

- - - - - 6c5475e1 by Stefan Monnier at 2019-07-24T04:40:25Z * src/subst.ml (subst): Fold the remaining Shift into Cons.

Fold `Shift` into the `Cons`, and hence remove `Shift` since it's not needed as a separate constructor any more.

(sink, substitute): Use `cons` (lookup, mkShift, cons, compose): * src/lexp.ml (subst_string, subst_eq): * src/inverse_subst.ml (transfo, is_identity, invertible) (lookup_inv_subst, compose_inv_subst): Adjust accordingly.

* tests/inverse_test.ml (is_identity): Update from src/inverse_subst.ml.

* src/opslexp.ml (lexp_whnf): Use `S.cons`.

- - - - -

7 changed files:

- src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/subst.ml - tests/inverse_test.ml - tests/unify_test.ml

Changes:

===================================== src/elab.ml ===================================== @@ -238,7 +238,7 @@ let ctx_define_rec (ctx: elab_context) decls =

let newMetavar (ctx : lexp_context) sl name t = let meta = Unif.create_metavar ctx sl t in - mkMetavar (meta, S.Identity, name) + mkMetavar (meta, S.identity, name)

let newMetalevel (ctx : lexp_context) sl loc = newMetavar ctx sl (loc, Some "ℓ") type_level

===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution

-Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -68,16 +68,17 @@ let transfo (s: Lexp.subst) : substIR option = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in match s with - | S.Cons (Var _ as v, s) -> - (match transfo s off_acc (idx + 1) imp_cnt with - | Some (tail, off, imp) -> let newVar = shiftVar v off_acc - in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off, imp) - | None -> None) - | S.Cons (Imm (Sexp.Symbol (_, "")), s) - -> transfo s off_acc (idx + 1) (imp_cnt + 1) - | S.Shift (s, offset) -> transfo s (offset + off_acc) idx imp_cnt - | S.Identity -> Some ([], off_acc, imp_cnt) (* End of recursion *) + | S.Cons (Var _ as v, s, o) -> + let off_acc = off_acc + o in + (match transfo s off_acc (idx + 1) imp_cnt with + | Some (tail, off, imp) + -> let newVar = shiftVar v off_acc + in if newVar >= off then None (* Error *) + else Some (((shiftVar v off_acc), idx)::tail, off, imp) + | None -> None) + | S.Cons (Imm (Sexp.Symbol (_, "")), s, o) + -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) + | S.Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) in transfo s 0 0 0

@@ -144,8 +145,8 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = let is_identity s = let rec is_identity s acc = match s with - | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> acc = shift + | S.Cons(Var(_, idx), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0

@@ -180,10 +181,9 @@ let inverse (s: Lexp.subst) : Lexp.subst option = * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) let rec invertible (s: subst) : bool = match s with - | S.Identity -> true - | S.Shift (s, _) -> invertible s - | S.Cons (e, s) -> (match e with Var _ -> true | _ -> e = impossible) - && invertible s + | S.Identity _ -> true + | S.Cons (e, s, _) -> (match e with Var _ -> true | _ -> e = impossible) + && invertible s

exception Not_invertible exception Ambiguous @@ -191,18 +191,16 @@ exception Ambiguous (* Lookup variable i in s⁻¹ *) let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match s with - | S.Identity -> i - | S.Shift (s, n) -> if i < n then - raise Not_invertible - else lookup_inv_subst (i - n) s - | S.Cons (Var (_, i'), s) when i' = i - -> (try let i'' = lookup_inv_subst i s in + | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible + | S.Identity o -> i - o + | S.Cons (Var (_, i'), s, o) when i' = i - o + -> (try let i'' = lookup_inv_subst i' s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) - | S.Cons (e, s) + | S.Cons (e, s, o) -> assert (match e with Var _ -> true | _ -> e = impossible); - 1 + lookup_inv_subst i s + 1 + lookup_inv_subst (i - o) s

(* When going under a binder, we have the rule * (λe)[s] ==> λ(e[lift s]) @@ -226,7 +224,8 @@ let shift_inv_subst n s (* We could define it as: * = compose_inv_subst s (S.shift n) * But this can fail if an element of `s` maps to a var with index < n *) - = let shift_n = match inverse (S.shift n) with + = if n = 0 then s else + let shift_n = match inverse (S.shift n) with | Some s -> s | _ -> assert (false) in Lexp.scompose s shift_n @@ -236,13 +235,14 @@ let shift_inv_subst n s * But we can try and do it more directly. *) let rec compose_inv_subst (s' : subst) (s : subst) = match s' with - | S.Cons (e, s') -> S.Cons (apply_inv_subst e s, compose_inv_subst s' s) - | S.Identity -> (match inverse s with - | Some s -> s - (* FIXME: could also be Ambiguous, depending on `s`. *) - | None -> raise Not_invertible) - | S.Shift (s', n) - -> compose_inv_subst s' (shift_inv_subst n s) + | S.Cons (e, s', o) -> + let s = shift_inv_subst o s in + (* FIXME: Why don't we ever return a Shift? *) + S.cons (apply_inv_subst e s) (compose_inv_subst s' s) + | S.Identity o -> (match inverse (shift_inv_subst o s) with + | Some s -> s + (* FIXME: could also be Ambiguous, depending on `s`. *) + | None -> raise Not_invertible)

(* Apply s⁻¹ to e. * The function presumes that `invertible s` was true.

===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language.

-Copyright (C) 2011-2018 Free Software Foundation, Inc. +Copyright (C) 2011-2019 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca Keywords: languages, lisp, dependent types. @@ -541,9 +541,10 @@ let rec lexp_unparse lxp = and lexp_string lxp = sexp_string (lexp_unparse lxp)

and subst_string s = match s with - | S.Identity -> "Id" - | S.Shift (s, n) -> "(↑"^ string_of_int n ^ " " ^ subst_string s ^ ")" - | S.Cons (l, s) -> lexp_name l ^ " · " ^ subst_string s + | S.Identity o -> "↑" ^ string_of_int o + | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s + | S.Cons (l, s, o) + -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.Cons (l, s, 0)) ^ ")"

and lexp_name e = match e with @@ -938,17 +939,17 @@ let rec eq e1 e2 = and subst_eq s1 s2 = s1 == s2 || match (s1, s2) with - | (S.Identity, S.Identity) -> true - | (S.Cons (e1, s1), S.Cons (e2, s2)) - -> eq e1 e2 && subst_eq s1 s2 - | (S.Shift (s1, o1), S.Shift (s2, o2)) - -> let o = min o1 o2 in - subst_eq (S.mkShift s1 (o1 - o)) (S.mkShift s2 (o2 - o)) - | (S.Shift (S.Cons (e1, s1), o1), S.Cons (e2, s2)) - -> eq (mkSusp e1 (S.shift o1)) e2 - && subst_eq (S.mkShift s1 o1) s2 - | (S.Cons (e1, s1), S.Shift (S.Cons (e2, s2), o2)) - -> eq e1 (mkSusp e2 (S.shift o2)) - && subst_eq s1 (S.mkShift s2 o2) + | (S.Identity o1, S.Identity o2) -> o1 = o2 + | (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2)) + -> if o1 = o2 then + eq e1 e2 && subst_eq s1 s2 + else if o1 > o2 then + let o = o1 - o2 in + eq (mkSusp e1 (S.shift o)) e2 + && subst_eq (S.mkShift s1 o) s2 + else + let o = o2 - o1 in + eq e1 (mkSusp e2 (S.shift o)) + && subst_eq s1 (S.mkShift s2 o) | _ -> false

===================================== src/opslexp.ml ===================================== @@ -152,7 +152,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.Cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d), s), + (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, d + 1)) (S.identity, 0) aargs in

===================================== src/subst.ml ===================================== @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp

-Copyright (C) 2016-2017 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc.

Author: Stefan Monnier monnier@iro.umontreal.ca

@@ -119,13 +119,11 @@ type db_offset = int (* DeBruijn index offset. *) * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) type 'a subst = (* lexp subst *) + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) (* Lift (n,m) increases indices≥N by M. * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - | Identity - | Cons of 'a * 'a subst - (* we enter a let/lambda/case/inductive (with formal args) *) - | Shift of 'a subst * db_offset (* | Lift of db_index * db_offset *)

(* Apply a substitution to a single variable. *) @@ -134,40 +132,61 @@ let lookup (mkVar : 'b -> db_index -> 'a) (s: 'a subst) (l : 'b) (v:db_index) : 'a = let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = match s with - | Identity -> mkVar l (v+o) - | Shift (s, o') -> lookup' (o+o') s v - | Cons (e, s) -> if v>0 then lookup' o s (v-1) - else mkShift e o + | Identity o' -> mkVar l (v + o + o') + | Cons (e, s, o') -> let o = o + o' in + if v > 0 then lookup' o s (v - 1) + else mkShift e o in lookup' 0 s v

let mkShift s (m:db_offset) = if m>0 then - match s with Shift (s', n) -> Shift (s', n+m) - | _ -> Shift (s, m) + match s with Identity o -> Identity (o + m) + | Cons (e, s, o) -> Cons (e, s, o + m) else s

(* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) = mkShift Identity m +let shift (m:db_offset) = Identity m + +(* Return a substitution which replaces #0 with `e` and the applies `s` + * to the rest. *) +let cons e s = Cons (e, s, 0)

(* The trivial substitution which doesn't do anything. *) -let identity = Identity +let identity = Identity 0

(* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match s with | Identity -> true | _ -> false +let identity_p s = match s with | Identity o -> o = 0 | _ -> false

(* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) let compose (mkSusp : 'a -> 'a subst -> 'a) - (s1: 'a subst) (s2: 'a subst) : 'a subst = + (s1: 'a subst) (s2: 'a subst) : 'a subst = + (* There is a bit of flexibility in what we return, in the sense + * that some shifts can be pushed more or less down. Here we + * want the shifts to float as far outside as possible. *) let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = - match s1, s2 with - | (Identity, s2) -> s2 - | (s1, Identity) -> s1 - | (s1, Shift (s2, o2)) -> mkShift (compose' s1 s2) o2 - | (Shift (s1, o1), Cons (e, s2)) -> compose' (mkShift s1 (o1-1)) s2 - | (Cons (e, s1), s2) -> Cons (mkSusp e s2, compose' s1 s2) + match s1 with + | Identity o1 + -> let rec compose_id o1 s o = match s with + | Identity o2 -> Identity (o + o1 + o2) + | Cons (e, s, o2) + -> if o1 = 0 then Cons (e, s, o + o2) + else compose_id (o1 - 1) s (o + o2) + in compose_id o1 s2 0 + | Cons (e1, s1, o1) + -> let rec compose_cons o1 s o = match s with + | Identity o2 -> Cons (e1, s1, o + o1 + o2) + | Cons (e2, s2, o2) + -> if o1 = 0 then + (* Pull out o2's shift and compose the two Cons. *) + let s2' = cons e2 s2 in + Cons (mkSusp e1 s2', compose' s1 s2', o + o2) + else + (* Cancel out o1's shift with e2 and hoist o2 out. *) + compose_cons (o1 - 1) s2 (o + o2) + in compose_cons o1 s2 0 in compose' s1 s2

(* Adjust a substitution for use under one more binder. @@ -175,11 +194,7 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) * from Δs,x to Δₜ,x. * Also known as `lift`. *) let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = - Cons (mkVar l 0, mkShift s 1) - -(* Return a substitution which replaces #0 with `e` and the applies `s` - * to the rest. *) -let cons e s = Cons (e, s) + cons (mkVar l 0) (mkShift s 1)

(* Return a substitution which replaces #0 with `e`. *) -let substitute e = Cons (e, Identity) +let substitute e = cons e identity

===================================== tests/inverse_test.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_test.ml --- Test the substitution-inversion algorithm * - * Copyright (C) 2016-2017 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -68,8 +68,8 @@ let input = let is_identity s = let rec is_identity s acc = match s with - | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> acc = shift + | S.Cons(Var(_, idx), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0

===================================== tests/unify_test.ml ===================================== @@ -1,6 +1,6 @@ (* unify_test.ml --- Test the unification algorithm * - * Copyright (C) 2016-2018 Free Software Foundation, Inc. + * Copyright (C) 2016-2019 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle tiv.crb@gmail.com * @@ -183,7 +183,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::(input_type , input_type_t , Equivalent) (* 44 *)

- ::(Metavar (0, S.Identity, (Util.dummy_location, Some "M")), + ::(Metavar (0, S.identity, (Util.dummy_location, Some "M")), Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)

::[]

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