Typer Juillet 2019

typer@iro.umontreal.ca

2 participants
5 discussions

[Git][monnier/typer][master] 2 commits: Add comments from a Myers's subst experiment
by Stefan 26 Jul '19

26 Jul '19

Stefan pushed to branch master at Stefan / Typer Commits: d75ab820 by Stefan Monnier at 2019-07-27T03:38:33Z Add comments from a Myers's subst experiment * src/lexp.ml (lexp_unparse): Prefer S.cons to S.Cons. * src/subst.ml (subst): Add Myers's optimization in a comment. It probably works, but it currently bumps into another performance problem. (lookup, compose): Add commented-out Myers's optimization. * tests/inverse_test.ml (is_identity): Remove (lets the code use the version of Inverse_subst). - - - - - ff16d3ba by Stefan Monnier at 2019-07-27T03:39:04Z * samples/defmacro.typer (define-macro): New package and macro - - - - - 4 changed files: - + samples/defmacro.typer - src/lexp.ml - src/subst.ml - tests/inverse_test.ml Changes: ===================================== samples/defmacro.typer ===================================== @@ -0,0 +1,43 @@ +%%% defmacro.typer --- Convenience macro to define macros + +%% Copyright (C) 2018 Stefan Monnier + +%% Author: Stefan Monnier <monnier(a)iro.umontreal.ca> +%% Keywords: + +%% This program is free software; you can redistribute it and/or modify +%% it under the terms of the GNU General Public License as published by +%% the Free Software Foundation, either version 3 of the License, or +%% (at your option) any later version. + +%% This program is distributed in the hope that it will be useful, +%% but WITHOUT ANY WARRANTY; without even the implied warranty of +%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +%% GNU General Public License for more details. + +%% You should have received a copy of the GNU General Public License +%% along with this program. If not, see <https://www.gnu.org/licenses/>. + +%%% Commentary: + +%% + +%%% Code: + +define-macro = + let dm argsym args body = case args + | nil => body + in macro (lambda args -> case args + | nil => Sexp_error + | cons name args' + => case args' + | nil => Sexp_error + | cons args body + => IO_bind + (gensym ()) + (lambda argsym -> + quote (uquote name + = macro (lambda (uquote argsym) + -> uquote (dm argsym args body))))); + +%%% defmacro.typer ends here ===================================== src/lexp.ml ===================================== @@ -80,8 +80,8 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vname) list * lexp) SMap.t * (vname * lexp) option (* Default. *) - (* The `subst` only applies to the lexp associated - * with the metavar's "value", not to the ltype. *) + (* The `subst` will be applied to the the metavar's value when it + * gets instantiated. *) | Metavar of meta_id * subst * vname (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref @@ -135,7 +135,7 @@ type varbind = * no `eq` hash-tables, ...). * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique - * integer in order to procude a hash anyway (and we'd have to write the hash + * integer in order to produce a hash anyway (and we'd have to write the hash * function by hand, tho that might be a good idea anyway). *) @@ -260,6 +260,30 @@ 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)) +(* 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 + * the complexity of adding a `Lift` to `subst`. + *) +(* let sink_count_total = ref 0 + * let sink_count_optimizable = ref 0 + * + * let ssink l s = + * sink_count_total := 1 + !sink_count_total; + * (match s with + * | S.Cons (Var (_, 0), (S.Identity o | S.Cons (_, _, o)), 0) when o > 0 + * -> sink_count_optimizable := 1 + !sink_count_optimizable + * | _ -> ()); + * if ((!sink_count_total) mod 10000) = 0 then + * (print_string ("Optimizable = " + * ^ (string_of_int ((100 * !sink_count_optimizable) + * / !sink_count_total)) + * ^ "%\n"); + * if !sink_count_total > 100000 then + * (sink_count_total := !sink_count_total / 2; + * sink_count_optimizable := !sink_count_optimizable / 2)); + * S.sink (fun l i -> mkVar (l, i)) l s *) + let rec lexp_location e = match e with @@ -544,7 +568,7 @@ and subst_string s = match s with | 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)) ^ ")" + -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")" and lexp_name e = match e with ===================================== src/subst.ml ===================================== @@ -121,11 +121,19 @@ type db_offset = int (* DeBruijn index offset. *) 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. + (* Myers's extra pointers down the list: + * * int * 'a subst * db_offset *) +(* 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. *) (* | Lift of db_index * db_offset *) +(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *) + (* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) @@ -133,6 +141,8 @@ let lookup (mkVar : 'b -> db_index -> 'a) let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = match s with | Identity o' -> mkVar l (v + o + o') + (* Use Myers's fastlane when applicable: + * | Cons (_, _, _, sk, s, o') when v >= sk -> lookup' (o + o') s (v - sk) *) | Cons (e, s, o') -> let o = o + o' in if v > 0 then lookup' o s (v - 1) else mkShift e o @@ -171,21 +181,23 @@ let compose (mkSusp : 'a -> 'a subst -> 'a) | 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) + | Cons (e2, s2, o2) (* , sk2, s2', o2' *) + -> (* Myers's fastlane: + * if o1 >= sk2 then compose_id (o1 - sk2) s2' (o + o2') *) + if o1 > 0 then compose_id (o1 - 1) s2 (o + o2) + else Cons (e2, s2, 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) + | Cons (e2, s2, o2) (* , sk2, s2', o2' *) + -> (* Myers's fastlane: + * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) + if o1 > 0 then compose_cons (o1 - 1) s2 (o + o2) + else + (* Pull out o2's shift and compose the two Cons. *) + let s' = cons e2 s2 in + Cons (mkSusp e1 s', compose' s1 s', o + o2) in compose_cons o1 s2 0 in compose' s1 s2 ===================================== tests/inverse_test.ml ===================================== @@ -65,14 +65,6 @@ let input = ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), false):: [] -let is_identity s = - let rec is_identity s acc = - match s with - | 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 - let generateRandInput shiftMax numberOfTest = Random.self_init (); let rec generateList shiftMax numberOfTest = View it on GitLab: https://gitlab.com/monnier/typer/compare/6c5475e1fc84f67e0760b8504c9afdd1f5… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/6c5475e1fc84f67e0760b8504c9afdd1f5… You're receiving this email because of your account on gitlab.com.

1 0

Pratique pour présentation TyDe, jeudi 1 août 14h
by Stefan Monnier 25 Jul '19

25 Jul '19

Comme mentionné au lunch auourd'hui, je vais donner une présentation d'essai jeudi prochain au labo (c'est pour la conférence TyDe-2019, colocated avec ICFP), Stefan \title{Inductive types deconstructed} \subtitle{The calculus of united constructions} \begin{abstract} Algebraic data types and inductive types like those of the Calculus of Inductive Constructions (CIC) are the bread and butter of statically typed functional programming languages. They conveniently combine in a single package product types, sum types, recursive types, and indexed types. But this also makes them somewhat heavyweight: for example, tuples have to be defined as ``degenerate'' single constructor inductive types, and extraction of a single field becomes a laborious full case-analysis on the object. We consider this to be unsatisfactory. In this article, we develop an alternative presentation of CIC's inductive types where the various elements are provided separately, such that inductive types are built on top of tuples and sums rather than the other way around. The resulting language is lower-level yet we show it to be equivalent to a predicative version of the Calculus of Inductive Constructions. An additional benefit is that it can conveniently give a precise type to the default branch of \kw{case} statements. \end{abstract}

1 0

Talk about parallel parsing
by Stefan Monnier 25 Jul '19

25 Jul '19

Found it! It's called "monoidal pasing" by Edward Kmett. E.g. http://comonad.com/reader/2009/iteratees-parsec-and-monoid/ https://www.youtube.com/watch?v=Txf7swrcLYs Stefan

1 0

[Git][monnier/typer][master] 2 commits: * src/subst.ml (subst): Fold a `Shift` into the `Identity`.
by Stefan 24 Jul '19

24 Jul '19

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(a)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(a)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(a)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(a)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(a)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/8061a7de3449e4e867d523787c415755e3… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/8061a7de3449e4e867d523787c415755e3… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch dev/errors
by Jean-Alexandre Barszcz 10 Jul '19

10 Jul '19

Jean-Alexandre Barszcz pushed new branch dev/errors at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/tree/dev/errors You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juillet 2019