Alice de Berny pushed to branch alice at Stefan / Typer

Commits: a289d4c4 by irradiee at 2020-05-24T21:45:19-04:00 add hash to lexp representation

- - - - -

2 changed files:

- src/debug.ml - src/lexp.ml

Changes:

===================================== src/debug.ml ===================================== @@ -156,3 +156,8 @@ let debug_lexp_decls decls = str;

) decls + +let print_hc_table = WHC.iter (fun e -> print_int (Hashtbl.hash e); + print_string "\t"; + lexp_print e; + print_string "\n") hc_table

===================================== src/lexp.ml ===================================== @@ -60,7 +60,8 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp

type ltype = lexp and subst = lexp S.subst - and lexp = + and lexp = lexp' * int + and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort @@ -173,6 +174,60 @@ let metavar_lookup (id : meta_id) : metavar_info * let hc (e : lexp) : lexp = * try Hashtbl.find hc_table e * with Not_found -> Hashtbl.add hc_table e e; e *) + let lexp_hash (e, h) = h + + let rec apply_lxor (map : int list) : int = + match map with + | [] -> 0 + | e :: l -> e lxor (apply_lxor l) + +(* Hashtbl.hash for not lexp types + * TODO: find something else *) + let lexp'_hash expr = + match expr with + | Imm s -> Hashtbl.hash s + | SortLevel l + -> (match l with + | SLz -> Hashtbl.hash l + | SLsucc lp -> lexp_hash lp + | SLlub (lp1, lp2) -> (lexp_hash lp1) lxor (lexp_hash lp2)) + | Sort (l, s) + -> (Hashtbl.hash l) lxor + (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 + | Let (l, ds, e) + -> (Hashtbl.hash l) lxor + ((apply_lxor (List.map (fun e -> let (n, lp, lt) = e in + ((Hashtbl.hash n) lxor ((lexp_hash lp) lxor (lexp_hash lt)))) + ds)) lxor (lexp_hash e)) + | Arrow (k, v, t1, l, t2) + -> ((Hashtbl.hash k) lxor (Hashtbl.hash v)) lxor + ((lexp_hash t1) lxor ((Hashtbl.hash l) lxor (lexp_hash t2))) + | Lambda (k, v, t, e) + -> ((Hashtbl.hash k) lxor (Hashtbl.hash v)) lxor + ((lexp_hash t) lxor (lexp_hash e)) + | Inductive (l, n, a, cs) + -> ((Hashtbl.hash l) lxor (Hashtbl.hash n)) lxor + ((apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + ((Hashtbl.hash ak) lxor ((Hashtbl.hash n) lxor (lexp_hash lt)))) a)) + lxor Hashtbl.hash cs) + | Cons (t, n) -> (lexp_hash t) lxor (Hashtbl.hash n) + | Case (l, e, rt, bs, d) + -> ((Hashtbl.hash l) lxor (lexp_hash e)) lxor + ((lexp_hash rt) lxor ((Hashtbl.hash bs) lxor + (match d with + | Some (n, lp) -> (Hashtbl.hash n) lxor (lexp_hash lp) + | _ -> 0))) + | Metavar (id, s, v) + -> Hashtbl.hash expr + | Call (e, args) -> (lexp_hash e) lxor + (apply_lxor (List.map (fun e -> let (ak, lp) = e in + ((Hashtbl.hash ak) lxor (lexp_hash lp))) args)) +(* | Susp (lp, subst) -> (lexp_hash lp) lxor (Hashtbl.hash subst) *)

module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results @@ -180,11 +235,12 @@ module WHC = Weak.Make (struct type t = lexp * `compare` checks == before recursing * but (=) doesn't? *) let equal x y = (compare x y = 0) - let hash = Hashtbl.hash + let hash = lexp_hash end) -let hc_table : WHC.t = WHC.create 1000 -let hc : lexp -> lexp = WHC.merge hc_table

+(* TODO: maybe just a table ? *) +let hc_table : WHC.t = WHC.create 1000 +let hc (e : lexp') : lexp = let h = lexp'_hash e in WHC.merge hc_table (e, h)

let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) @@ -201,8 +257,8 @@ let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) - | _, [] -> f - | _ -> hc (Call (f, es)) + | _, [] -> (f, lexp'_hash f) + | _ -> hc (Call ((f, lexp'_hash f), es))

and lexp_head e = match e with @@ -231,15 +287,15 @@ let mkSLlub' (e1, e2) = match (e1, e2) with -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) - -> SLlub (e1, e2) + -> SLlub ((e1, lexp'_hash e1), (e2, lexp'_hash e2)) | _ -> Log.log_fatal ~section:"internal" ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)

let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ - -> SLsucc e + -> SLsucc (e, lexp'_hash e) | _ -> Log.log_fatal ~section:"internal" "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 @@ -271,12 +327,16 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * ... *)

+(* let mkSusp e s = let susp = mkSusp_aux e s in (susp, lexp'_hash susp) *) + +(* argh *) let rec mkSusp e s = + let (e', h) = e in if S.identity_p s then e else (* We apply the substitution eagerly to some terms. * There's no deep technical rason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) - match e with + match e' with | Imm _ -> e | Builtin _ -> e | Susp (e, s') -> mkSusp_memo e (scompose s' s) @@ -1012,4 +1072,3 @@ and subst_eq s1 s2 = eq e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) | _ -> false -

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