clever weak hashtable (bravo, Francois!)

src/core/decl.ml

@@ -86,6 +86,11 @@ module Spr = Prop.S
 module Mpr = Prop.M
 module Hpr = Prop.H
 
+module Wpr = Hashweak.Make (struct
+  type t = prsymbol
+  let key pr = pr.pr_name.id_weak
+end)
+
 let pr_equal = (==)
 
 let create_prsymbol n = { pr_name = id_register n }
@@ -106,8 +111,9 @@ type prop_decl = prop_kind * prsymbol * fmla
 
 type decl = {
   d_node : decl_node;
-  d_syms : Sid.t;       (* idents used in declaration *)
-  d_news : Sid.t;       (* idents introduced in declaration *)
+  d_syms : Sid.t;         (* idents used in declaration *)
+  d_news : Sid.t;         (* idents introduced in declaration *)
+  d_weak : Hashweak.key;  (* weak hashtable key *)
   d_tag  : int;
 }
 
@@ -180,7 +186,6 @@ end)
 
 module Sdecl = Decl.S
 module Mdecl = Decl.M
-module Hdecl = Decl.H
 
 let d_equal = (==)
 
@@ -190,6 +195,7 @@ let mk_decl node syms news = Hsdecl.hashcons {
   d_node = node;
   d_syms = syms;
   d_news = news;
+  d_weak = Hashweak.create_key ();
   d_tag  = -1;
 }
 

src/core/decl.mli

@@ -56,6 +56,7 @@ type prsymbol = private {
 module Spr : Set.S with type elt = prsymbol
 module Mpr : Map.S with type key = prsymbol
 module Hpr : Hashtbl.S with type key = prsymbol
+module Wpr : Hashweak.S with type key = prsymbol
 
 val create_prsymbol : preid -> prsymbol
 
@@ -77,8 +78,9 @@ type prop_decl = prop_kind * prsymbol * fmla
 
 type decl = private {
   d_node : decl_node;
-  d_syms : Sid.t;       (* idents used in declaration *)
-  d_news : Sid.t;       (* idents introduced in declaration *)
+  d_syms : Sid.t;         (* idents used in declaration *)
+  d_news : Sid.t;         (* idents introduced in declaration *)
+  d_weak : Hashweak.key;  (* weak hashtable key *)
   d_tag  : int;
 }
 
@@ -90,7 +92,6 @@ and decl_node =
 
 module Sdecl : Set.S with type elt = decl
 module Mdecl : Map.S with type key = decl
-module Hdecl : Hashtbl.S with type key = decl
 
 val d_equal : decl -> decl -> bool
 

src/core/env.ml

@@ -25,28 +25,25 @@ open Theory
 type env = {
   env_retrieve : retrieve_theory;
   env_memo     : (string list, theory Mnm.t) Hashtbl.t;
-  env_tag      : int;
+  env_weak     : Hashweak.key;
 }
 
 and retrieve_theory = env -> string list -> theory Mnm.t
 
-let create_env =
-  let r = ref 0 in
-  fun retrieve ->
-    incr r;
-    let env = {
-      env_retrieve = retrieve;
-      env_memo     = Hashtbl.create 17;
-      env_tag      = !r }
-    in
-    let add th m = Mnm.add th.th_name.id_string th m in
-    let m = Mnm.empty in
-    let m = add builtin_theory m in
-    let m = add (tuple_theory 0) m in
-    let m = add (tuple_theory 1) m in
-    let m = add (tuple_theory 2) m in
-    Hashtbl.add env.env_memo [] m;
-    env
+let create_env retrieve =
+  let env = {
+    env_retrieve = retrieve;
+    env_memo     = Hashtbl.create 17;
+    env_weak     = Hashweak.create_key (); }
+  in
+  let add th m = Mnm.add th.th_name.id_string th m in
+  let m = Mnm.empty in
+  let m = add builtin_theory m in
+  let m = add (tuple_theory 0) m in
+  let m = add (tuple_theory 1) m in
+  let m = add (tuple_theory 2) m in
+  Hashtbl.add env.env_memo [] m;
+  env
 
 exception TheoryNotFound of string list * string
 
@@ -65,7 +62,7 @@ let find_theory env sl s =
   with Not_found ->
     raise (TheoryNotFound (sl, s))
 
-let env_tag env = env.env_tag
+let env_weak env = env.env_weak
 
 
 (** Parsers *)

src/core/env.mli

@@ -23,7 +23,7 @@ open Theory
 
 type env
 
-val env_tag : env -> int
+val env_weak : env -> Hashweak.key
 
 type retrieve_theory = env -> string list -> theory Mnm.t
 
@@ -32,20 +32,12 @@ val create_env : retrieve_theory -> env
 exception TheoryNotFound of string list * string
 
 val find_theory : env -> string list -> string -> theory
-  (** [find_theory e p n] finds the theory named [p.n] in environment
-      [e] 
-
-      @raises [TheoryNotFound p n] if theory not present in env [e]
-
-  *)
-  
-
-
-
+  (** [find_theory e p n] finds the theory named [p.n] in environment [e]
+      @raises [TheoryNotFound p n] if theory not present in env [e] *)
 
 (** Parsers *)
 
-type read_channel = 
+type read_channel =
   ?debug:bool -> ?parse_only:bool -> ?type_only:bool ->
   env -> string -> in_channel -> theory Mnm.t
 

src/core/ident.ml

@@ -22,9 +22,10 @@ open Util
 (** Identifiers *)
 
 type ident = {
-  id_string : string;   (* non-unique name *)
-  id_origin : origin;   (* origin of the ident *)
-  id_tag    : int;      (* unique numeric tag *)
+  id_string : string;       (* non-unique name *)
+  id_origin : origin;       (* origin of the ident *)
+  id_weak   : Hashweak.key; (* weak hashtable key *)
+  id_tag    : int;          (* unique numeric tag *)
 }
 
 and origin =
@@ -54,6 +55,7 @@ let id_register id = { id with id_tag = gentag () }
 let create_ident name origin = {
   id_string = name;
   id_origin = origin;
+  id_weak   = Hashweak.create_key ();
   id_tag    = -1
 }
 

src/core/ident.mli

@@ -20,9 +20,10 @@
 (** Identifiers *)
 
 type ident = private {
-  id_string : string;   (* non-unique name *)
-  id_origin : origin;   (* origin of the ident *)
-  id_tag    : int;      (* unique numeric tag *)
+  id_string : string;       (* non-unique name *)
+  id_origin : origin;       (* origin of the ident *)
+  id_weak   : Hashweak.key; (* weak hashtable key *)
+  id_tag    : int;          (* unique numeric tag *)
 }
 
 and origin =

src/core/task.ml

@@ -27,8 +27,9 @@ open Theory
 (** Clone and meta history *)
 
 type tdecl_set = {
-  tds_set : Stdecl.t;
-  tds_tag : int;
+  tds_set  : Stdecl.t;
+  tds_weak : Hashweak.key;
+  tds_tag  : int;
 }
 
 module Hstds = Hashcons.Make (struct
@@ -39,7 +40,11 @@ module Hstds = Hashcons.Make (struct
   let tag n s = { s with tds_tag = n }
 end)
 
-let mk_tds s = Hstds.hashcons { tds_set = s; tds_tag = -1 }
+let mk_tds s = Hstds.hashcons {
+  tds_set  = s;
+  tds_weak = Hashweak.create_key ();
+  tds_tag  = -1
+}
 
 let empty_tds = mk_tds Stdecl.empty
 let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
@@ -66,12 +71,13 @@ let mm_add mm t td = if t.meta_excl
 type task = task_hd option
 
 and task_hd = {
-  task_decl  : tdecl;       (* last declaration *)
-  task_prev  : task;        (* context *)
-  task_known : known_map;   (* known identifiers *)
-  task_clone : clone_map;   (* cloning history *)
-  task_meta  : meta_map;    (* meta properties *)
-  task_tag   : int;         (* unique task tag *)
+  task_decl  : tdecl;        (* last declaration *)
+  task_prev  : task;         (* context *)
+  task_known : known_map;    (* known identifiers *)
+  task_clone : clone_map;    (* cloning history *)
+  task_meta  : meta_map;     (* meta properties *)
+  task_weak  : Hashweak.key; (* weak hashtable key *)
+  task_tag   : int;          (* unique task tag *)
 }
 
 let task_hd_equal = (==)
@@ -101,6 +107,7 @@ let mk_task decl prev known clone meta = Some (Hstask.hashcons {
   task_known = known;
   task_clone = clone;
   task_meta  = meta;
+  task_weak  = Hashweak.create_key ();
   task_tag   = -1;
 })
 

src/core/task.mli

@@ -27,8 +27,9 @@ open Theory
 (** Clone and meta history *)
 
 type tdecl_set = private {
-  tds_set : Stdecl.t;
-  tds_tag : int;
+  tds_set  : Stdecl.t;
+  tds_weak : Hashweak.key;
+  tds_tag  : int;
 }
 
 val tds_equal : tdecl_set -> tdecl_set -> bool
@@ -41,12 +42,13 @@ type meta_map = tdecl_set Mmeta.t
 type task = task_hd option
 
 and task_hd = private {
-  task_decl  : tdecl;       (* last declaration *)
-  task_prev  : task;        (* context *)
-  task_known : known_map;   (* known identifiers *)
-  task_clone : clone_map;   (* cloning history *)
-  task_meta  : meta_map;    (* meta properties *)
-  task_tag   : int;         (* unique task tag *)
+  task_decl  : tdecl;        (* last declaration *)
+  task_prev  : task;         (* context *)
+  task_known : known_map;    (* known identifiers *)
+  task_clone : clone_map;    (* cloning history *)
+  task_meta  : meta_map;     (* meta properties *)
+  task_weak  : Hashweak.key; (* weak hashtable key *)
+  task_tag   : int;          (* unique task tag *)
 }
 
 val task_equal : task -> task -> bool

src/core/term.ml

@@ -63,6 +63,11 @@ module Sls = Lsym.S
 module Mls = Lsym.M
 module Hls = Lsym.H
 
+module Wls = Hashweak.Make (struct
+  type t = lsymbol
+  let key ls = ls.ls_name.id_weak
+end)
+
 let ls_equal = (==)
 
 let create_lsymbol name args value = {
@@ -443,7 +448,6 @@ end)
 module Sterm = Term.S
 module Mterm = Term.M
 module Hterm = Term.H
-module Wterm = Term.W
 
 module Hsfmla = Hashcons.Make (struct
 

src/core/term.mli

@@ -48,6 +48,7 @@ type lsymbol = private {
 module Sls : Set.S with type elt = lsymbol
 module Mls : Map.S with type key = lsymbol
 module Hls : Hashtbl.S with type key = lsymbol
+module Wls : Hashweak.S with type key = lsymbol
 
 val ls_equal : lsymbol -> lsymbol -> bool
 
@@ -71,8 +72,8 @@ exception PredicateSymbolExpected of lsymbol
 type pattern = private {
   pat_node : pattern_node;
   pat_vars : Svs.t;
-  pat_ty : ty;
-  pat_tag : int;
+  pat_ty   : ty;
+  pat_tag  : int;
 }
 
 and pattern_node = private
@@ -173,7 +174,6 @@ and trigger = expr list
 
 module Mterm : Map.S with type key = term
 module Sterm : Set.S with type elt = term
-module Wterm : Hashweak.S with type key = term
 module Mfmla : Map.S with type key = fmla
 module Sfmla : Set.S with type elt = fmla
 

src/core/theory.ml

@@ -226,7 +226,6 @@ end)
 module Stdecl = Tdecl.S
 module Mtdecl = Tdecl.M
 module Htdecl = Tdecl.H
-module Wtdecl = Tdecl.W
 
 let td_equal = (==)
 

src/core/theory.mli

@@ -98,7 +98,6 @@ and tdecl_node = private
 module Stdecl : Set.S with type elt = tdecl
 module Mtdecl : Map.S with type key = tdecl
 module Htdecl : Hashtbl.S with type key = tdecl
-module Wtdecl : Hashweak.S with type key = tdecl
 
 val td_equal : tdecl -> tdecl -> bool
 

src/core/trans.ml

@@ -42,15 +42,15 @@ let compose_l f g x = list_apply g (f x)
 
 let apply f x = f x
 
-module WHtask = Hashweak.Make (struct
+module Wtask = Hashweak.Make (struct
   type t = task_hd
-  let tag t = t.task_tag
+  let key t = t.task_weak
 end)
 
-let store fn = WHtask.memoize_option 63 fn
+let store fn = Wtask.memoize_option fn
 
 let fold fn v =
-  let h = WHtask.create 63 in
+  let h = Wtask.create () in
   let rewind acc task =
 (*
     Format.printf "%c%d." (match task.task_decl.td_node with
@@ -58,11 +58,11 @@ let fold fn v =
     | Use _  -> 'U' | Meta _  -> 'M') task.task_tag;
 *)
     let acc = fn task acc in
-    WHtask.set h task acc;
+    Wtask.set h task acc;
     acc
   in
   let current task =
-    try Some (WHtask.find h task)
+    try Some (Wtask.find h task)
     with Not_found -> None
   in
   let rec accum todo = function
@@ -82,13 +82,13 @@ let fold_map_l fn v t = conv_res (List.rev_map snd) (fold_l fn (v, t))
 let map   fn = fold   (fun t1 t2 -> fn t1 t2)
 let map_l fn = fold_l (fun t1 t2 -> fn t1 t2)
 
-module WHdecl = Hashweak.Make (struct
+module Wdecl = Hashweak.Make (struct
   type t = decl
-  let tag d = d.d_tag
+  let key d = d.d_weak
 end)
 
 let gen_decl add fn =
-  let fn = WHdecl.memoize 63 fn in
+  let fn = Wdecl.memoize fn in
   let fn task acc = match task.task_decl.td_node with
     | Decl d -> List.fold_left add acc (fn d)
     | _ -> add_tdecl acc task.task_decl
@@ -96,7 +96,7 @@ let gen_decl add fn =
   map fn
 
 let gen_decl_l add fn =
-  let fn = WHdecl.memoize 63 fn in
+  let fn = Wdecl.memoize fn in
   let fn task acc = match task.task_decl.td_node with
     | Decl d -> List.rev_map (List.fold_left add acc) (fn d)
     | _ -> [add_tdecl acc task.task_decl]
@@ -113,7 +113,7 @@ let apply_to_goal fn d = match d.d_node with
   | _ -> assert false
 
 let gen_goal add fn =
-  let fn = WHdecl.memoize 5 (apply_to_goal fn) in
+  let fn = Wdecl.memoize (apply_to_goal fn) in
   let rec pass task = match task with
     | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
         List.fold_left add prev (fn d)
@@ -124,7 +124,7 @@ let gen_goal add fn =
   pass
 
 let gen_goal_l add fn =
-  let fn = WHdecl.memoize 5 (apply_to_goal fn) in
+  let fn = Wdecl.memoize (apply_to_goal fn) in
   let rec pass task = match task with
     | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
         List.rev_map (List.fold_left add prev) (fn d)
@@ -145,15 +145,15 @@ let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
 
 module Wtds = Hashweak.Make (struct
   type t = tdecl_set
-  let tag s = s.tds_tag
+  let key s = s.tds_weak
 end)
 
 let on_theory th fn =
-  let fn = Wtds.memoize 17 fn in
+  let fn = Wtds.memoize fn in
   fun task -> fn (find_clone task th) task
 
 let on_meta t fn =
-  let fn = Wtds.memoize 17 fn in
+  let fn = Wtds.memoize fn in
   fun task -> fn (find_meta task t) task
 
 let on_theories tl fn =
@@ -179,7 +179,7 @@ open Env
 
 module Wenv = Hashweak.Make (struct
   type t = env
-  let tag = env_tag
+  let key = env_weak
 end)
 
 exception UnknownTrans of string
@@ -198,11 +198,11 @@ let register_transform_l s p =
 
 let register_env_transform s p =
   if Hashtbl.mem transforms s then raise (KnownTrans s);
-  Hashtbl.replace transforms s (Wenv.memoize 3 p)
+  Hashtbl.replace transforms s (Wenv.memoize p)
 
 let register_env_transform_l s p =
   if Hashtbl.mem transforms_l s then raise (KnownTrans s);
-  Hashtbl.replace transforms_l s (Wenv.memoize 3 p)
+  Hashtbl.replace transforms_l s (Wenv.memoize p)
 
 let lookup_transform s =
   try Hashtbl.find transforms s with Not_found -> raise (UnknownTrans s)

src/core/ty.ml

@@ -49,6 +49,7 @@ type tysymbol = {
 
 and ty = {
   ty_node : ty_node;
+  ty_weak : Hashweak.key;
   ty_tag : int;
 }
 
@@ -64,7 +65,11 @@ end)
 module Sts = Tsym.S
 module Mts = Tsym.M
 module Hts = Tsym.H
-module Wts = Tsym.W
+
+module Wts = Hashweak.Make (struct
+  type t = tysymbol
+  let key ts = ts.ts_name.id_weak
+end)
 
 let ts_equal = (==)
 let ty_equal = (==)
@@ -105,9 +110,18 @@ module Ty = StructMake (Tty)
 module Sty = Ty.S
 module Mty = Ty.M
 module Hty = Ty.H
-module Wty = Ty.W
 
-let mk_ty n = { ty_node = n; ty_tag = -1 }
+module Wty = Hashweak.Make (struct
+  type t = ty
+  let key ty = ty.ty_weak
+end)
+
+let mk_ty n = {
+  ty_node = n;
+  ty_weak = Hashweak.create_key ();
+  ty_tag  = -1
+}
+
 let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
 let ty_app s tl = Hsty.hashcons (mk_ty (Tyapp (s, tl)))
 

src/core/ty.mli

@@ -43,6 +43,7 @@ type tysymbol = private {
 
 and ty = private {
   ty_node : ty_node;
+  ty_weak : Hashweak.key;
   ty_tag  : int;
 }
 
@@ -55,7 +56,7 @@ module Mts : Map.S with type key = tysymbol
 module Hts : Hashtbl.S with type key = tysymbol
 module Wts : Hashweak.S with type key = tysymbol
 
-module Tty : Hashweak.Tagged with type t = ty
+module Tty : Util.Tagged with type t = ty
 
 module Sty : Set.S with type elt = ty
 module Mty : Map.S with type key = ty

src/transform/encoding_bridge.ml

@@ -70,7 +70,7 @@ let load_prelude kept env =
     task_tdecls task in
   task,
   { kept = kept;
-    clone_builtin = Wts.memoize 7 clone_builtin;
+    clone_builtin = Wts.memoize clone_builtin;
     specials = specials;
     trans_lsymbol = Hls.create 17;
     trans_tsymbol = trans_tsymbol}

src/transform/encoding_simple.ml

@@ -69,7 +69,7 @@ let init_tenv kept =
   in
   task,
   { kept          = kept;
-    declare_kept  = Wts.memoize 7 declare_kept;
+    declare_kept  = Wts.memoize declare_kept;
     specials      = specials;
     ty_uni        = ty_uni;
     trans_lsymbol = Hls.create 17 }

src/util/hashweak.ml

@@ -17,6 +17,44 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module Weak : sig
+
+  type key
+
+  type 'a t
+
+  val create_key : unit -> key
+
+  val create : unit -> 'a t
+    (* create a hashtbl with weak keys *)
+
+  val find : 'a t -> key -> 'a
+    (* find the value bound to a key.
+       Raises Not_found if there is no binding *)
+
+  val mem : 'a t -> key -> bool
+    (* test if a key is bound *)
+
+  val set : 'a t -> key -> 'a -> unit
+    (* bind the key _once_ with the given value *)
+
+end = struct
+
+  type key = ((int,Obj.t) Hashtbl.t) Lazy.t
+
+  type 'a t = int
+
+  let create_key () = lazy (Hashtbl.create 3)
+
+  let create = let c = ref (-1) in fun () -> incr c; !c
+
+  let find t k  = Obj.obj (Hashtbl.find (Lazy.force k) t)
+  let mem t k   = Hashtbl.mem (Lazy.force k) t
+  let set t k v = Hashtbl.replace (Lazy.force k) t (Obj.repr v)
+
+end
+
+include Weak
 
 module type S = sig
 
@@ -24,7 +62,7 @@ module type S = sig
 
   type 'a t
 
-  val create : int -> 'a t
+  val create : unit -> 'a t
     (* create a hashtbl with weak keys *)
 
   val find : 'a t -> key -> 'a
@@ -37,64 +75,53 @@ module type S = sig
   val set : 'a t -> key -> 'a -> unit
     (* bind the key _once_ with the given value *)
 
-  val memoize : int -> (key -> 'a) -> (key -> 'a)
+  val memoize : (key -> 'a) -> (key -> 'a)
     (* create a memoizing function *)
 
-  val memoize_option : int -> (key option -> 'a) -> (key option -> 'a)
+  val memoize_option : (key option -> 'a) -> (key option -> 'a)
     (* memoizing functions on option types *)
 
 end
 
-module type Tagged =
+module type Weakey =
 sig
   type t
-  val tag : t -> int
+  val key : t -> Weak.key
 end
 
-module Make (S : Tagged) = struct
+module Make (S : Weakey) = struct
+
   type key = S.t
 
-  type 'a t = {
-    table : (int,'a) Hashtbl.t;
-    final : S.t -> unit;
-  }
-
-  let create n =
-    let table = Hashtbl.create n in
-    let w = Weak.create 1 in
-    Weak.set w 0 (Some table);
-    let final x = match Weak.get w 0 with
-      | Some h -> Hashtbl.remove h (S.tag x)
-      | None -> ()
-    in
-    { table = table; final = final }
-
-  let add_tag  h = Hashtbl.add  h.table
-  let mem_tag  h = Hashtbl.mem  h.table
-  let find_tag h = Hashtbl.find h.table
-
-  let set_tag h t e v =
-    assert (not (mem_tag h t));
-    Gc.finalise h.final e;
-    add_tag h t v
-
-  let set  h e = set_tag  h (S.tag e) e
-  let mem  h e = mem_tag  h (S.tag e)
-  let find h e = find_tag h (S.tag e)
-
-  let memoize n fn =
-    let h = create n in fun e ->
-      let t = S.tag e in
-      try find_tag h t
+  type 'a t = 'a Weak.t
+
+  let create = Weak.create
+
+  let set_key  h = Weak.set  h
+  let mem_key  h = Weak.mem  h
+  let find_key h = Weak.find h
+
+  let set_key h k v =
+    assert (not (mem_key h k));
+    set_key h k v
+
+  let set  h e = set_key  h (S.key e)
+  let mem  h e = mem_key  h (S.key e)
+  let find h e = find_key h (S.key e)
+
+  let memoize fn =
+    let h = create () in fun e ->
+      let k = S.key e in
+      try find_key h k
       with Not_found ->
         let v = fn e in
-        set_tag h t e v;
+        set_key h k v;
         v
 
-  let memoize_option n fn =
+  let memoize_option fn =
     let v = lazy (fn None) in
-    let fn e = fn (Some e) in 
-    let fn = memoize n fn in
+    let fn e = fn (Some e) in
+    let fn = memoize fn in
     function
       | Some e -> fn e
       | None -> Lazy.force v

src/util/hashweak.mli

@@ -19,13 +19,32 @@
 
 (** Hashtable with weak key used for memoization *)
 
+type key
+
+type 'a t
+
+val create_key : unit -> key
+
+val create : unit -> 'a t
+  (* create a hashtbl with weak keys *)
+
+val find : 'a t -> key -> 'a
+  (* find the value bound to a key.
+     Raises Not_found if there is no binding *)
+
+val mem : 'a t -> key -> bool
+  (* test if a key is bound *)
+
+val set : 'a t -> key -> 'a -> unit
+  (* assign the key to the given value *)
+
 module type S = sig
 
   type key
 
   type 'a t
 
-  val create : int -> 'a t
+  val create : unit -> 'a t
     (* create a hashtbl with weak keys *)
 
   val find : 'a t -> key -> 'a
@@ -38,18 +57,19 @@ module type S = sig
   val set : 'a t -> key -> 'a -> unit
     (* bind the key _once_ with the given value *)
 
-  val memoize : int -> (key -> 'a) -> (key -> 'a)
+  val memoize : (key -> 'a) -> (key -> 'a)
     (* create a memoizing function *)