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@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/6c5475e1fc84f67e0760b8504c9afdd1f52...