Alice de Berny pushed to branch alice at Stefan / Typer

Commits: 809270e8 by irradiee at 2020-06-09T11:38:37-04:00 add hc equality & lexp id in hash

- - - - - 11db9c7f by irradiee at 2020-06-09T15:43:33-04:00 attempt to add hash in subst

- - - - -

3 changed files:

- src/REPL.ml - src/eval.ml - src/lexp.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -231,6 +231,7 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) + | "%collisions" | "%cl" -> (get_stats hc_table)

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> (

===================================== src/eval.ml ===================================== @@ -484,7 +484,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, (Var (vdummy, -1), dummy_hash))])) + -> Vtype (L.mkCall (e, [(Anormal, hc (Var (vdummy, -1)))])) | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt =

===================================== src/lexp.ml ===================================== @@ -59,7 +59,8 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp * surrounded context extended with the first and the second bindings. *)

type ltype = lexp - and subst = lexp S.subst +and subst = subst' * int + and subst' = lexp S.subst and lexp = lexp' * int and lexp' = | Imm of sexp (* Used for strings, ... *) @@ -159,8 +160,6 @@ type meta_subst = metavar_info U.IMap.t

let dummy_scope_level = 0

-let dummy_hash = 0 - let builtin_size = ref 0

let metavar_table = ref (U.IMap.empty : meta_subst) @@ -177,87 +176,129 @@ let metavar_lookup (id : meta_id) : metavar_info * with Not_found -> Hashtbl.add hc_table e e; e *) let lexp_hash (e, h) = h

-(* == depends on implementation when it involves non mutable types - * do not use (e, h) directly to "construct" a lexp ? - * in this case we had: ref lexp1' = ref lexp2' but not lexp1' == lexp2' ... *) let lexp_lexp' (e, h) = e

let rec apply_lxor (map : int list) : int = match map with - | [] -> 0 - | e :: l -> e lxor (apply_lxor l) - -let combine_hash e1 e2 = e1 lxor e2 + | [] -> 31 + | e :: l -> (e * 31) lxor (apply_lxor l)

-let smap_hash e smap = - (combine_hash - (apply_lxor - (List.map (fun e -> let (ak, n, lt) = e in - (combine_hash (Hashtbl.hash ak) - (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) - e)) (Hashtbl.hash smap)) +let combine_hash e1 e2 = (e1 * 31) lxor e2

(* Hashtbl.hash for not lexp types * TODO: - find something else - * - extract the first arg of 2 arg types ? (SMap)*) + * - extract the first arg of 2 arg types ? (SMap) *) let lexp'_hash (expr : lexp') = match expr with - | Imm s -> Hashtbl.hash s + | Imm s -> combine_hash 1 (Hashtbl.hash s) | SortLevel l - -> (match l with + -> combine_hash 2 (match l with | SLz -> Hashtbl.hash l | SLsucc lp -> lexp_hash lp | SLlub (lp1, lp2) -> combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) - -> combine_hash (Hashtbl.hash l) + -> combine_hash 3 (combine_hash (Hashtbl.hash l) (match s with | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s - | StypeLevel -> Hashtbl.hash s) - | Builtin (v, t, m) as e -> Hashtbl.hash e - | Var v -> Hashtbl.hash v + | StypeLevel -> Hashtbl.hash s)) + | Builtin (v, t, m) as e -> combine_hash 4 (Hashtbl.hash e) + | Var v -> combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> combine_hash (Hashtbl.hash l) + -> combine_hash 6 (combine_hash (Hashtbl.hash l) (combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in (combine_hash (Hashtbl.hash n) (combine_hash (lexp_hash lp) (lexp_hash lt)))) - ds)) (lexp_hash e)) + ds)) (lexp_hash e))) | Arrow (k, v, t1, l, t2) - -> combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t1) (combine_hash (Hashtbl.hash l) (lexp_hash t2))) + -> combine_hash 7 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (combine_hash (lexp_hash t1) (combine_hash (Hashtbl.hash l) (lexp_hash t2)))) | Lambda (k, v, t, e) - -> combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) - (combine_hash (lexp_hash t) (lexp_hash e)) + -> combine_hash 8 (combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (combine_hash (lexp_hash t) (lexp_hash e))) | Inductive (l, n, a, cs) - -> combine_hash (combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + -> combine_hash 9 (combine_hash (combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) (combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in (combine_hash (Hashtbl.hash ak) (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) - (Hashtbl.hash cs)) (* here *) - | Cons (t, n) -> combine_hash (lexp_hash t) (Hashtbl.hash n) + (Hashtbl.hash cs))) + | Cons (t, n) -> combine_hash 10 (combine_hash (lexp_hash t) (Hashtbl.hash n)) | Case (l, e, rt, bs, d) - -> combine_hash (combine_hash (Hashtbl.hash l) (lexp_hash e)) + -> combine_hash 11 (combine_hash (combine_hash (Hashtbl.hash l) (lexp_hash e)) (combine_hash (lexp_hash rt) (combine_hash (Hashtbl.hash bs) (match d with | Some (n, lp) -> combine_hash (Hashtbl.hash n) (lexp_hash lp) - | _ -> 0))) + | _ -> 0)))) | Metavar (id, s, v) - -> Hashtbl.hash expr - | Call (e, args) -> combine_hash (lexp_hash e) + -> combine_hash 12 (Hashtbl.hash expr) + | Call (e, args) -> combine_hash 13 (combine_hash (lexp_hash e) (apply_lxor (List.map (fun e -> let (ak, lp) = e in - (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args)) - | Susp (lp, subst) -> combine_hash (lexp_hash lp) (Hashtbl.hash subst) + (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) + | Susp (lp, subst) -> combine_hash 14 (combine_hash (lexp_hash lp) (Hashtbl.hash subst))

let compare_hash x y = let (x', h1) = x in let (y', h2) = y in compare h1 h2 = 0

+let hc_eq e1 e2 = + e1 == e2 || + match (lexp_lexp' e1, lexp_lexp' e2) with + | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 + | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 + | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 + | (Imm s1, Imm s2) -> s1 = s2 + | (SortLevel SLz, SortLevel SLz) -> true + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> e1 == e2 + | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) + -> e11 == e12 && e21 == e22 + | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true + | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 + | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Var (_, i1), Var (_, i2)) -> i1 = i2 + | ((Susp (e1, s1) as e), _) -> compare e (lexp_lexp' e2) = 0 + | (_, (Susp (e2, s2) as e)) -> compare (lexp_lexp' e1) e = 0 + | (Let (_, defs1, e1), Let (_, defs2, e2)) + -> e1 == e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) + -> t1 == t2 && e1 == e2) + defs1 defs2 + | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + -> ak1 = ak2 && t11 == t12 && t21 == t22 + | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + -> ak1 = ak2 && t1 == t2 && e1 == e2 + | (Call (e1, as1), Call (e2, as2)) + -> e1 == e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) + -> ak1 = ak2 && e1 == e2) + as1 as2 + | (Inductive (_, l1, as1, cases1), Inductive (_, l2, as2, cases2)) + -> l1 = l2 + && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) + -> ak1 = ak2 && e1 == e2) + as1 as2 + && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) + -> ak1 = ak2 && e1 == e2)) + cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 + | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) + -> e1 == e2 && r1 == r2 + && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) + -> e1 == e2 && List.for_all2 (fun (ak1, _) (ak2, _) + -> ak1 = ak2) + fields1 fields2) + cases1 cases2 + && (match (def1, def2) with + | (Some (_, e1), Some (_, e2)) -> e1 == e2 + | _ -> def1 = def2) + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && compare s1 s2 = 0 + | _ -> false + module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results * in an *enormous* slowdown. Apparently * `compare` checks == before recursing * but (=) doesn't? *) - let equal x y = (compare (lexp_lexp' x) (lexp_lexp' y) = 0) + let equal x y = hc_eq x y let hash = lexp_hash end)

@@ -265,6 +306,15 @@ let hc_table : WHC.t = WHC.create 1000 let hc (e : lexp') : lexp = let lp = (e, lexp'_hash e) in WHC.merge hc_table lp

+let get_stats table = + let (tl, ne, sumb, smallb, medianb, bigb) = WHC.stats table in + Printf.printf "\n\ttable length: %i\n + number of entries: %i\n + sum of bucket lengths: %i\n + smallest bucket length: %i\n + median bucket length: %i\n + biggest bucket length: %i\n" tl ne sumb smallb medianb bigb + let impossible = hc (Imm Sexp.dummy_epsilon)

let mkImm s = hc (Imm s) @@ -336,7 +386,42 @@ let mkSLsucc e = (* FIXME: We'd like to make this table "weak" to avoid memory leaks, * but Weak.Make doesn't cut it because we need to index with a pair * that is transient and hence immediately GC'd. *) -let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 + +(* try... *) +type subst_pair = ((lexp * subst) * lexp) + +let subst_hash (s, h) = h + + let hcs_eq sb1 sb2 = + sb1 == sb2 || + match (sb1, sb2) with + | (((l1, S.Identity off), l2), ((l1', S.Identity off'), l2')) + -> l1 == l1' && off = off' && l2 == l2' + | (((l1, S.Cons (lp1, lps1, off1)), l2), ((l1', S.Cons (lp2, lps2, off2)), l2')) + -> l1 == l1' && lp1 == lp2 && lps1 == lps2 && off1 = off2 && l2 == l2' + | _ -> false + + let subst'_hash sb : int = + match sb with + | ((l1, S.Identity off), l2) + -> combine_hash 1 (combine_hash (lexp_hash l1) + (combine_hash (Hashtbl.hash off) (lexp_hash l2))) + | ((l1, S.Cons (lp, sb, off)), l2) + -> combine_hash 2 (combine_hash (lexp_hash l1) + (combine_hash (combine_hash (lexp_hash lp) (subst_hash sb)) + (combine_hash (Hashtbl.hash off) (lexp_hash l2)))) + + module WHCS = Hashtbl.Make (struct type t = subst_pair + let equal x y = hcs_eq x y + let hash = subst_hash + end) + +let hcs_table : WHCS.t = WHCS.create 1000 + +(* let hcs (s : subst') : subst = + let sb = (s, subst'_hash s) in WHCS.merge hcsb_table sb *) + +(******)

(* When computing the type of "load"ed modules * we end up building substitutions of the form

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/3376edace9286d4aff35fb4f87be0628e...