diff --git a/src/core/decl.ml b/src/core/decl.ml
index 91f296a1e2d413594834bb40441d6866110086a5..84a0e80a2031dceee24c71a0829de0e054a1f916 100644
--- a/src/core/decl.ml
+++ b/src/core/decl.ml
@@ -77,7 +77,7 @@ type prsymbol = {
pr_name : ident;
}
-module Prop = StructMake (struct
+module Prop = WeakStructMake (struct
type t = prsymbol
let tag pr = pr.pr_name.id_tag
end)
@@ -85,14 +85,12 @@ end)
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)
+module Wpr = Prop.W
let pr_equal = (==)
+let pr_hash pr = id_hash pr.pr_name
+
let create_prsymbol n = { pr_name = id_register n }
type ind_decl = lsymbol * (prsymbol * fmla) list
@@ -113,8 +111,7 @@ type decl = {
d_node : decl_node;
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;
+ d_tag : Hashweak.tag; (* unique magical tag *)
}
and decl_node =
@@ -154,17 +151,15 @@ module Hsdecl = Hashcons.Make (struct
| _,_ -> false
let hs_td (ts,td) = match td with
- | Tabstract -> ts.ts_name.id_tag
- | Talgebraic l ->
- let tag fs = fs.ls_name.id_tag in
- 1 + Hashcons.combine_list tag ts.ts_name.id_tag l
+ | Tabstract -> ts_hash ts
+ | Talgebraic l -> 1 + Hashcons.combine_list ls_hash (ts_hash ts) l
- let hs_ld (ls,ld) = Hashcons.combine ls.ls_name.id_tag
- (Hashcons.combine_option (fun (_,f) -> f.f_tag) ld)
+ let hs_ld (ls,ld) = Hashcons.combine (ls_hash ls)
+ (Hashcons.combine_option (fun (_,f) -> f_hash f) ld)
- let hs_prop (pr,f) = Hashcons.combine pr.pr_name.id_tag f.f_tag
+ let hs_prop (pr,f) = Hashcons.combine (pr_hash pr) (f_hash f)
- let hs_ind (ps,al) = Hashcons.combine_list hs_prop ps.ls_name.id_tag al
+ let hs_ind (ps,al) = Hashcons.combine_list hs_prop (ls_hash ps) al
let hs_kind = function
| Plemma -> 11 | Paxiom -> 13 | Pgoal -> 17 | Pskip -> 19
@@ -175,28 +170,30 @@ module Hsdecl = Hashcons.Make (struct
| Dind l -> Hashcons.combine_list hs_ind 7 l
| Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
- let tag n d = { d with d_tag = n }
+ let tag n d = { d with d_tag = Hashweak.create_tag n }
end)
-module Decl = StructMake (struct
+module Decl = WeakStructMake (struct
type t = decl
let tag d = d.d_tag
end)
module Sdecl = Decl.S
module Mdecl = Decl.M
+module Wdecl = Decl.W
let d_equal = (==)
+let d_hash d = Hashweak.tag_hash d.d_tag
+
(** Declaration constructors *)
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;
+ d_tag = Hashweak.dummy_tag;
}
exception IllegalTypeAlias of tysymbol
diff --git a/src/core/decl.mli b/src/core/decl.mli
index 7a6271b9d2a81d4fcf1cdc0256cf812fa8147499..2113c2023fed0708de3c11540a7d4a34ff1a15a1 100644
--- a/src/core/decl.mli
+++ b/src/core/decl.mli
@@ -62,6 +62,8 @@ val create_prsymbol : preid -> prsymbol
val pr_equal : prsymbol -> prsymbol -> bool
+val pr_hash : prsymbol -> int
+
type ind_decl = lsymbol * (prsymbol * fmla) list
(* Proposition declaration *)
@@ -80,8 +82,7 @@ type decl = private {
d_node : decl_node;
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;
+ d_tag : Hashweak.tag; (* unique magical tag *)
}
and decl_node =
@@ -92,8 +93,10 @@ and decl_node =
module Sdecl : Set.S with type elt = decl
module Mdecl : Map.S with type key = decl
+module Wdecl : Hashweak.S with type key = decl
val d_equal : decl -> decl -> bool
+val d_hash : decl -> int
(** {2 Declaration constructors} *)
diff --git a/src/core/env.ml b/src/core/env.ml
index 36d3863e67d7de126615d0383c0408f2aad6069f..32c57222bbb0912d614dd88d4546eab90fd63b29 100644
--- a/src/core/env.ml
+++ b/src/core/env.ml
@@ -25,16 +25,16 @@ open Theory
type env = {
env_retrieve : retrieve_theory;
env_memo : (string list, theory Mnm.t) Hashtbl.t;
- env_weak : Hashweak.key;
+ env_tag : Hashweak.tag;
}
and retrieve_theory = env -> string list -> theory Mnm.t
-let create_env retrieve =
+let create_env = let c = ref (-1) in fun retrieve ->
let env = {
env_retrieve = retrieve;
env_memo = Hashtbl.create 17;
- env_weak = Hashweak.create_key (); }
+ env_tag = (incr c; Hashweak.create_tag !c) }
in
let add th m = Mnm.add th.th_name.id_string th m in
let m = Mnm.empty in
@@ -62,7 +62,7 @@ let find_theory env sl s =
with Not_found ->
raise (TheoryNotFound (sl, s))
-let env_weak env = env.env_weak
+let env_tag env = env.env_tag
(** Parsers *)
diff --git a/src/core/env.mli b/src/core/env.mli
index 7973ebb418a0ab82c08478d2e5daebbd27ee67cf..f5e32cc9d8a50655f8fcf3abde6ab0fc9a62b8e9 100644
--- a/src/core/env.mli
+++ b/src/core/env.mli
@@ -23,7 +23,7 @@ open Theory
type env
-val env_weak : env -> Hashweak.key
+val env_tag : env -> Hashweak.tag
type retrieve_theory = env -> string list -> theory Mnm.t
diff --git a/src/core/ident.ml b/src/core/ident.ml
index 0f08d03a6a191566929607581107e8cd599a86db..7b53f2227ead296c5d575efee40aa40c1433d864 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -24,8 +24,7 @@ open Util
type ident = {
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 *)
+ id_tag : Hashweak.tag; (* unique magical tag *)
}
and origin =
@@ -33,7 +32,7 @@ and origin =
| Derived of ident
| Fresh
-module Id = StructMake (struct
+module Id = WeakStructMake (struct
type t = ident
let tag id = id.id_tag
end)
@@ -46,24 +45,24 @@ type preid = ident
let id_equal = (==)
-(* constructors *)
+let id_hash id = Hashweak.tag_hash id.id_tag
-let gentag = let r = ref 0 in fun () -> incr r; !r
+(* constructors *)
-let id_register id = { id with id_tag = gentag () }
+let id_register = let r = ref 0 in fun id ->
+ { id with id_tag = (incr r; Hashweak.create_tag !r) }
let create_ident name origin = {
id_string = name;
id_origin = origin;
- id_weak = Hashweak.create_key ();
- id_tag = -1
+ id_tag = Hashweak.dummy_tag;
}
let id_fresh nm = create_ident nm Fresh
let id_user nm loc = create_ident nm (User loc)
let id_derive nm id = create_ident nm (Derived id)
let id_clone id = create_ident id.id_string (Derived id)
-let id_dup id = { id with id_tag = -1 }
+let id_dup id = { id with id_tag = Hashweak.dummy_tag }
let rec id_derived_from i1 i2 = id_equal i1 i2 ||
(match i1.id_origin with
@@ -80,7 +79,7 @@ let rec id_from_user i =
type ident_printer = {
indices : (string, int) Hashtbl.t;
- values : (int, string) Hashtbl.t;
+ values : string Hid.t;
sanitizer : string -> string;
blacklist : string list;
}
@@ -107,31 +106,31 @@ let create_ident_printer ?(sanitizer = same) sl =
let indices = Hashtbl.create 1997 in
List.iter (reserve indices) sl;
{ indices = indices;
- values = Hashtbl.create 1997;
+ values = Hid.create 1997;
sanitizer = sanitizer;
blacklist = sl }
let id_unique printer ?(sanitizer = same) id =
try
- Hashtbl.find printer.values id.id_tag
+ Hid.find printer.values id
with Not_found ->
let name = sanitizer (printer.sanitizer id.id_string) in
let name = find_unique printer.indices name in
- Hashtbl.replace printer.values id.id_tag name;
+ Hid.replace printer.values id name;
name
let string_unique printer s = find_unique printer.indices s
let forget_id printer id =
try
- let name = Hashtbl.find printer.values id.id_tag in
+ let name = Hid.find printer.values id in
Hashtbl.remove printer.indices name;
- Hashtbl.remove printer.values id.id_tag
+ Hid.remove printer.values id
with Not_found -> ()
let forget_all printer =
+ Hid.clear printer.values;
Hashtbl.clear printer.indices;
- Hashtbl.clear printer.values;
List.iter (reserve printer.indices) printer.blacklist
(** Sanitizers *)
diff --git a/src/core/ident.mli b/src/core/ident.mli
index daf226b461ee6c3c85400ba574421a4da78f9129..16049a845986ee2fdf293411d4b012714a48ef57 100644
--- a/src/core/ident.mli
+++ b/src/core/ident.mli
@@ -22,8 +22,7 @@
type ident = private {
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 *)
+ id_tag : Hashweak.tag; (* unique magical tag *)
}
and origin =
@@ -37,6 +36,8 @@ module Hid : Hashtbl.S with type key = ident
val id_equal : ident -> ident -> bool
+val id_hash : ident -> int
+
(* a user-created type of unregistered identifiers *)
type preid
diff --git a/src/core/task.ml b/src/core/task.ml
index 0d22713a85d72213850219b9eadd53d6c761bf40..a42c48339334c6f58afc4db045119bf51f40ae28 100644
--- a/src/core/task.ml
+++ b/src/core/task.ml
@@ -27,23 +27,21 @@ open Theory
(** Clone and meta history *)
type tdecl_set = {
- tds_set : Stdecl.t;
- tds_weak : Hashweak.key;
- tds_tag : int;
+ tds_set : Stdecl.t;
+ tds_tag : Hashweak.tag;
}
module Hstds = Hashcons.Make (struct
type t = tdecl_set
let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
- let hs_td td acc = Hashcons.combine acc td.td_tag
+ let hs_td td acc = Hashcons.combine acc (td_hash td)
let hash s = Stdecl.fold hs_td s.tds_set 0
- let tag n s = { s with tds_tag = n }
+ let tag n s = { s with tds_tag = Hashweak.create_tag n }
end)
let mk_tds s = Hstds.hashcons {
- tds_set = s;
- tds_weak = Hashweak.create_key ();
- tds_tag = -1
+ tds_set = s;
+ tds_tag = Hashweak.dummy_tag;
}
let empty_tds = mk_tds Stdecl.empty
@@ -51,6 +49,7 @@ let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
let tds_singleton td = mk_tds (Stdecl.singleton td)
let tds_equal = (==)
+let tds_hash tds = Hashweak.tag_hash tds.tds_tag
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
@@ -76,29 +75,29 @@ and task_hd = {
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 *)
+ task_tag : Hashweak.tag; (* unique magical tag *)
}
let task_hd_equal = (==)
+let task_hd_hash t = Hashweak.tag_hash t.task_tag
+
let task_equal t1 t2 = match t1, t2 with
| Some t1, Some t2 -> task_hd_equal t1 t2
| None, None -> true
| _ -> false
+let task_hash t = option_apply 0 (fun t -> task_hd_hash t + 1) t
+
module Hstask = Hashcons.Make (struct
type t = task_hd
let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
task_equal t1.task_prev t2.task_prev
- let hash task =
- let decl = task.task_decl.td_tag in
- let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
- Hashcons.combine decl prev
+ let hash t = Hashcons.combine (td_hash t.task_decl) (task_hash t.task_prev)
- let tag i task = { task with task_tag = i }
+ let tag i task = { task with task_tag = Hashweak.create_tag i }
end)
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
@@ -107,8 +106,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;
+ task_tag = Hashweak.dummy_tag;
})
let task_known = option_apply Mid.empty (fun t -> t.task_known)
diff --git a/src/core/task.mli b/src/core/task.mli
index fab3671a52fae55c49031ff39968382af4c72e3d..319e5a2f851283bd8ecde013578e78bc1683baec 100644
--- a/src/core/task.mli
+++ b/src/core/task.mli
@@ -27,12 +27,12 @@ open Theory
(** Clone and meta history *)
type tdecl_set = private {
- tds_set : Stdecl.t;
- tds_weak : Hashweak.key;
- tds_tag : int;
+ tds_set : Stdecl.t;
+ tds_tag : Hashweak.tag;
}
val tds_equal : tdecl_set -> tdecl_set -> bool
+val tds_hash : tdecl_set -> int
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
@@ -47,13 +47,15 @@ and task_hd = private {
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 *)
+ task_tag : Hashweak.tag; (* unique magical tag *)
}
val task_equal : task -> task -> bool
val task_hd_equal : task_hd -> task_hd -> bool
+val task_hash : task -> int
+val task_hd_hash : task_hd -> int
+
val task_known : task -> known_map
val task_clone : task -> clone_map
val task_meta : task -> meta_map
diff --git a/src/core/term.ml b/src/core/term.ml
index 0e50708353dac977a3aed3901d9315de022fa1d4..6a2d710169840c8b43ce18cff86284fd332827d7 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -28,7 +28,7 @@ type vsymbol = {
vs_ty : ty;
}
-module Vsym = StructMake (struct
+module Vsym = WeakStructMake (struct
type t = vsymbol
let tag vs = vs.vs_name.id_tag
end)
@@ -39,6 +39,8 @@ module Hvs = Vsym.H
let vs_equal = (==)
+let vs_hash vs = id_hash vs.vs_name
+
let create_vsymbol name ty = {
vs_name = id_register name;
vs_ty = ty;
@@ -54,7 +56,7 @@ type lsymbol = {
ls_value : ty option;
}
-module Lsym = StructMake (struct
+module Lsym = WeakStructMake (struct
type t = lsymbol
let tag ls = ls.ls_name.id_tag
end)
@@ -62,14 +64,12 @@ end)
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)
+module Wls = Lsym.W
let ls_equal = (==)
+let ls_hash ls = id_hash ls.ls_name
+
let create_lsymbol name args value = {
ls_name = id_register name;
ls_args = args;
@@ -104,6 +104,8 @@ and pattern_node =
let pat_equal = (==)
+let pat_hash p = p.pat_tag
+
module Hspat = Hashcons.Make (struct
type t = pattern
@@ -121,16 +123,14 @@ module Hspat = Hashcons.Make (struct
let equal p1 p2 =
equal_node p1.pat_node p2.pat_node && ty_equal p1.pat_ty p2.pat_ty
- let hash_pattern p = p.pat_tag
-
let hash_node = function
| Pwild -> 0
- | Pvar v -> v.vs_name.id_tag
- | Papp (s, pl) -> Hashcons.combine_list hash_pattern s.ls_name.id_tag pl
- | Por (p, q) -> Hashcons.combine (hash_pattern p) (hash_pattern q)
- | Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
+ | Pvar v -> vs_hash v
+ | Papp (s, pl) -> Hashcons.combine_list pat_hash (ls_hash s) pl
+ | Por (p, q) -> Hashcons.combine (pat_hash p) (pat_hash q)
+ | Pas (p, v) -> Hashcons.combine (pat_hash p) (vs_hash v)
- let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
+ let hash p = Hashcons.combine (hash_node p.pat_node) (ty_hash p.pat_ty)
let tag n p = { p with pat_tag = n }
end)
@@ -333,6 +333,9 @@ and expr =
let t_equal = (==)
let f_equal = (==)
+let t_hash t = t.t_tag
+let f_hash f = f.f_tag
+
(* expr and trigger equality *)
let e_equal e1 e2 = match e1, e2 with
@@ -364,7 +367,7 @@ let bnd_equal b1 b2 =
b1.bv_bound = b2.bv_bound && Mint.equal t_equal b1.bv_defer b2.bv_defer
let bnd_hash bv =
- Mint.fold (fun i t a -> Hashcons.combine2 i t.t_tag a) bv.bv_defer
+ Mint.fold (fun i t a -> Hashcons.combine2 i (t_hash t) a) bv.bv_defer
let bnd_map fn bv = { bv with bv_defer = Mint.map fn bv.bv_defer }
let bnd_fold fn acc bv = Mint.fold (fun _ t a -> fn a t) bv.bv_defer acc
@@ -412,29 +415,27 @@ module Hsterm = Hashcons.Make (struct
list_all2 (=) t1.t_label t2.t_label
let t_hash_branch (p,b,t) =
- Hashcons.combine p.pat_tag (bnd_hash b t.t_tag)
+ Hashcons.combine (pat_hash p) (bnd_hash b (t_hash t))
let t_hash_bound (v,b,t) =
- Hashcons.combine v.vs_name.id_tag (bnd_hash b t.t_tag)
+ Hashcons.combine (vs_hash v) (bnd_hash b (t_hash t))
let f_hash_bound (v,b,f) =
- Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
-
- let t_hash t = t.t_tag
+ Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
let t_hash_node = function
| Tbvar n -> n
- | Tvar v -> v.vs_name.id_tag
+ | Tvar v -> vs_hash v
| Tconst c -> Hashtbl.hash c
- | Tapp (f,tl) -> Hashcons.combine_list t_hash (f.ls_name.id_tag) tl
- | Tif (f,t,e) -> Hashcons.combine2 f.f_tag t.t_tag e.t_tag
- | Tlet (t,bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
- | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
+ | Tapp (f,tl) -> Hashcons.combine_list t_hash (ls_hash f) tl
+ | Tif (f,t,e) -> Hashcons.combine2 (f_hash f) (t_hash t) (t_hash e)
+ | Tlet (t,bt) -> Hashcons.combine (t_hash t) (t_hash_bound bt)
+ | Tcase (t,bl) -> Hashcons.combine_list t_hash_branch (t_hash t) bl
| Teps f -> f_hash_bound f
let hash t =
Hashcons.combine (t_hash_node t.t_node)
- (Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
+ (Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
let tag n t = { t with t_tag = n }
@@ -484,34 +485,30 @@ module Hsfmla = Hashcons.Make (struct
f_equal_node f1.f_node f2.f_node &&
list_all2 (=) f1.f_label f2.f_label
- let v_hash v = v.vs_name.id_tag
-
- let t_hash t = t.t_tag
-
let f_hash_branch (p,b,f) =
- Hashcons.combine p.pat_tag (bnd_hash b f.f_tag)
+ Hashcons.combine (pat_hash p) (bnd_hash b (f_hash f))
let f_hash_bound (v,b,f) =
- Hashcons.combine v.vs_name.id_tag (bnd_hash b f.f_tag)
+ Hashcons.combine (vs_hash v) (bnd_hash b (f_hash f))
- let tr_hash = function Term t -> t.t_tag | Fmla f -> f.f_tag
+ let e_hash = function Term t -> t_hash t | Fmla f -> f_hash f
let f_hash_quant (vl,b,tl,f) =
- let h = bnd_hash b f.f_tag in
- let h = Hashcons.combine_list v_hash h vl in
- List.fold_left (Hashcons.combine_list tr_hash) h tl
+ let h = bnd_hash b (f_hash f) in
+ let h = Hashcons.combine_list vs_hash h vl in
+ List.fold_left (Hashcons.combine_list e_hash) h tl
let f_hash_node = function
- | Fapp (p,tl) -> Hashcons.combine_list t_hash p.ls_name.id_tag tl
+ | Fapp (p,tl) -> Hashcons.combine_list t_hash (ls_hash p) tl
| Fquant (q,bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_quant bf)
| Fbinop (op,f1,f2) ->
- Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
- | Fnot f -> Hashcons.combine 1 f.f_tag
+ Hashcons.combine2 (Hashtbl.hash op) (f_hash f1) (f_hash f2)
+ | Fnot f -> Hashcons.combine 1 (f_hash f)
| Ftrue -> 0
| Ffalse -> 1
- | Fif (f1,f2,f3) -> Hashcons.combine2 f1.f_tag f2.f_tag f3.f_tag
- | Flet (t,bf) -> Hashcons.combine t.t_tag (f_hash_bound bf)
- | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch t.t_tag bl
+ | Fif (f1,f2,f3) -> Hashcons.combine2 (f_hash f1) (f_hash f2) (f_hash f3)
+ | Flet (t,bf) -> Hashcons.combine (t_hash t) (f_hash_bound bf)
+ | Fcase (t,bl) -> Hashcons.combine_list f_hash_branch (t_hash t) bl
let hash f =
Hashcons.combine_list Hashtbl.hash (f_hash_node f.f_node) f.f_label
diff --git a/src/core/term.mli b/src/core/term.mli
index 1bd4a08ad60ca100ea7b83fe112bb2438669c36c..2fdc9be08bdfb07052103622df5521ab3b8da7be 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -34,6 +34,7 @@ module Mvs : Map.S with type key = vsymbol
module Hvs : Hashtbl.S with type key = vsymbol
val vs_equal : vsymbol -> vsymbol -> bool
+val vs_hash : vsymbol -> int
val create_vsymbol : preid -> ty -> vsymbol
@@ -51,6 +52,7 @@ module Hls : Hashtbl.S with type key = lsymbol
module Wls : Hashweak.S with type key = lsymbol
val ls_equal : lsymbol -> lsymbol -> bool
+val ls_hash : lsymbol -> int
val create_lsymbol : preid -> ty list -> ty option -> lsymbol
val create_fsymbol : preid -> ty list -> ty -> lsymbol
@@ -84,6 +86,7 @@ and pattern_node = private
| Pas of pattern * vsymbol
val pat_equal : pattern -> pattern -> bool
+val pat_hash : pattern -> int
(** smart constructors for patterns *)
@@ -172,10 +175,13 @@ and expr =
and trigger = expr list
-module Mterm : Map.S with type key = term
module Sterm : Set.S with type elt = term
-module Mfmla : Map.S with type key = fmla
+module Mterm : Map.S with type key = term
+module Hterm : Hashtbl.S with type key = term
+
module Sfmla : Set.S with type elt = fmla
+module Mfmla : Map.S with type key = fmla
+module Hfmla : Hashtbl.S with type key = fmla
val t_equal : term -> term -> bool
val f_equal : fmla -> fmla -> bool
@@ -183,6 +189,9 @@ val e_equal : expr -> expr -> bool
val tr_equal : trigger list -> trigger list -> bool
+val t_hash : term -> int
+val f_hash : fmla -> int
+
(** close bindings *)
val t_close_bound : vsymbol -> term -> term_bound
diff --git a/src/core/theory.ml b/src/core/theory.ml
index 63ae4b84df6e265a95771f7b8dccff94e66e8201..73622fbd8aaaa05970b17fd7e65762d6f8440dd8 100644
--- a/src/core/theory.ml
+++ b/src/core/theory.ml
@@ -109,7 +109,9 @@ module Smeta = SMmeta.S
module Mmeta = SMmeta.M
module Hmeta = SMmeta.H
-let meta_equal m1 m2 = m1.meta_tag = m2.meta_tag
+let meta_equal = (==)
+
+let meta_hash m = m.meta_tag
exception KnownMeta of meta
exception UnknownMeta of string
@@ -193,23 +195,23 @@ module Hstdecl = Hashcons.Make (struct
t1 = t2 && list_all2 eq_marg al1 al2
| _,_ -> false
- let hs_cl_ts _ ts acc = Hashcons.combine acc ts.ts_name.id_tag
- let hs_cl_ls _ ls acc = Hashcons.combine acc ls.ls_name.id_tag
- let hs_cl_pr _ pr acc = Hashcons.combine acc pr.pr_name.id_tag
+ let hs_cl_ts _ ts acc = Hashcons.combine acc (ts_hash ts)
+ let hs_cl_ls _ ls acc = Hashcons.combine acc (ls_hash ls)
+ let hs_cl_pr _ pr acc = Hashcons.combine acc (pr_hash pr)
let hs_ta = function
- | MAts ts -> ts.ts_name.id_tag
- | MAls ls -> ls.ls_name.id_tag
- | MApr pr -> pr.pr_name.id_tag
+ | MAts ts -> ts_hash ts
+ | MAls ls -> ls_hash ls
+ | MApr pr -> pr_hash pr
| MAstr s -> Hashtbl.hash s
| MAint i -> Hashtbl.hash i
let hash td = match td.td_node with
- | Decl d -> d.d_tag
- | Use th -> th.th_name.id_tag
+ | Decl d -> d_hash d
+ | Use th -> id_hash th.th_name
| Clone (th,tm,lm,pm) ->
Mts.fold hs_cl_ts tm (Mls.fold hs_cl_ls lm
- (Mpr.fold hs_cl_pr pm th.th_name.id_tag))
+ (Mpr.fold hs_cl_pr pm (id_hash th.th_name)))
| Meta (t,al) -> Hashcons.combine_list hs_ta (Hashtbl.hash t) al
let tag n td = { td with td_tag = n }
@@ -228,6 +230,7 @@ module Mtdecl = Tdecl.M
module Htdecl = Tdecl.H
let td_equal = (==)
+let td_hash td = td.td_tag
(** Constructors and utilities *)
diff --git a/src/core/theory.mli b/src/core/theory.mli
index 109bcfff0bc3e99ee3a5c2f8265947313d7c52f7..c4892467998bebf8dab1db44dd1c1ee220bd28d3 100644
--- a/src/core/theory.mli
+++ b/src/core/theory.mli
@@ -66,6 +66,7 @@ module Mmeta : Map.S with type key = meta
module Hmeta : Hashtbl.S with type key = meta
val meta_equal : meta -> meta -> bool
+val meta_hash : meta -> int
val register_meta : string -> meta_arg_type list -> meta
val register_meta_excl : string -> meta_arg_type list -> meta
@@ -100,6 +101,7 @@ module Mtdecl : Map.S with type key = tdecl
module Htdecl : Hashtbl.S with type key = tdecl
val td_equal : tdecl -> tdecl -> bool
+val td_hash : tdecl -> int
(** Constructors and utilities *)
@@ -132,7 +134,6 @@ val add_ind_decls : theory_uc -> ind_decl list -> theory_uc
(** Use *)
val create_use : theory -> tdecl
-
val use_export : theory_uc -> theory -> theory_uc
(** Clone *)
diff --git a/src/core/trans.ml b/src/core/trans.ml
index 27881566c7e2d920e519d4fbf584a87e757ce74f..f7a95074eb6ec950307c649271e94438b72b50d1 100644
--- a/src/core/trans.ml
+++ b/src/core/trans.ml
@@ -44,13 +44,13 @@ let apply f x = f x
module Wtask = Hashweak.Make (struct
type t = task_hd
- let key t = t.task_weak
+ let tag t = t.task_tag
end)
-let store fn = Wtask.memoize_option fn
+let store fn = Wtask.memoize_option 63 fn
let fold fn v =
- let h = Wtask.create () in
+ let h = Wtask.create 63 in
let rewind acc task =
(*
Format.printf "%c%d." (match task.task_decl.td_node with
@@ -82,13 +82,8 @@ 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 Wdecl = Hashweak.Make (struct
- type t = decl
- let key d = d.d_weak
-end)
-
let gen_decl add fn =
- let fn = Wdecl.memoize fn in
+ let fn = Wdecl.memoize 63 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 +91,7 @@ let gen_decl add fn =
map fn
let gen_decl_l add fn =
- let fn = Wdecl.memoize fn in
+ let fn = Wdecl.memoize 63 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 +108,7 @@ let apply_to_goal fn d = match d.d_node with
| _ -> assert false
let gen_goal add fn =
- let fn = Wdecl.memoize (apply_to_goal fn) in
+ let fn = Wdecl.memoize 5 (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 +119,7 @@ let gen_goal add fn =
pass
let gen_goal_l add fn =
- let fn = Wdecl.memoize (apply_to_goal fn) in
+ let fn = Wdecl.memoize 5 (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 +140,15 @@ let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
module Wtds = Hashweak.Make (struct
type t = tdecl_set
- let key s = s.tds_weak
+ let tag s = s.tds_tag
end)
let on_theory th fn =
- let fn = Wtds.memoize fn in
+ let fn = Wtds.memoize 17 fn in
fun task -> fn (find_clone task th) task
let on_meta t fn =
- let fn = Wtds.memoize fn in
+ let fn = Wtds.memoize 17 fn in
fun task -> fn (find_meta task t) task
let on_theories tl fn =
@@ -179,7 +174,7 @@ open Env
module Wenv = Hashweak.Make (struct
type t = env
- let key = env_weak
+ let tag = env_tag
end)
exception UnknownTrans of string
@@ -198,11 +193,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 p)
+ Hashtbl.replace transforms s (Wenv.memoize 3 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 p)
+ Hashtbl.replace transforms_l s (Wenv.memoize 3 p)
let lookup_transform s =
try Hashtbl.find transforms s with Not_found -> raise (UnknownTrans s)
diff --git a/src/core/ty.ml b/src/core/ty.ml
index 7f6aa1d85a8d9e2599844ad92c2610641438b846..bc52d3cc6894e4482976d0edffb80379a3522e4d 100644
--- a/src/core/ty.ml
+++ b/src/core/ty.ml
@@ -26,7 +26,7 @@ type tvsymbol = {
tv_name : ident;
}
-module Tvar = StructMake (struct
+module Tvar = WeakStructMake (struct
type t = tvsymbol
let tag tv = tv.tv_name.id_tag
end)
@@ -37,6 +37,8 @@ module Htv = Tvar.H
let tv_equal = (==)
+let tv_hash tv = id_hash tv.tv_name
+
let create_tvsymbol n = { tv_name = id_register n }
(* type symbols and types *)
@@ -49,15 +51,14 @@ type tysymbol = {
and ty = {
ty_node : ty_node;
- ty_weak : Hashweak.key;
- ty_tag : int;
+ ty_tag : Hashweak.tag;
}
and ty_node =
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
-module Tsym = StructMake (struct
+module Tsym = WeakStructMake (struct
type t = tysymbol
let tag ts = ts.ts_name.id_tag
end)
@@ -65,15 +66,14 @@ end)
module Sts = Tsym.S
module Mts = Tsym.M
module Hts = Tsym.H
-
-module Wts = Hashweak.Make (struct
- type t = tysymbol
- let key ts = ts.ts_name.id_weak
-end)
+module Wts = Tsym.W
let ts_equal = (==)
let ty_equal = (==)
+let ts_hash ts = id_hash ts.ts_name
+let ty_hash ty = Hashweak.tag_hash ty.ty_tag
+
let mk_ts name args def = {
ts_name = name;
ts_args = args;
@@ -91,35 +91,26 @@ module Hsty = Hashcons.Make (struct
ts_equal s1 s2 && List.for_all2 ty_equal l1 l2
| _ -> false
- let hash_ty ty = ty.ty_tag
-
let hash ty = match ty.ty_node with
- | Tyvar v -> v.tv_name.id_tag
- | Tyapp (s,tl) -> Hashcons.combine_list hash_ty s.ts_name.id_tag tl
+ | Tyvar v -> tv_hash v
+ | Tyapp (s,tl) -> Hashcons.combine_list ty_hash (ts_hash s) tl
- let tag n ty = { ty with ty_tag = n }
+ let tag n ty = { ty with ty_tag = Hashweak.create_tag n }
end)
-module Tty = struct
+module Ty = WeakStructMake (struct
type t = ty
let tag ty = ty.ty_tag
-end
-
-module Ty = StructMake (Tty)
+end)
module Sty = Ty.S
module Mty = Ty.M
module Hty = Ty.H
-
-module Wty = Hashweak.Make (struct
- type t = ty
- let key ty = ty.ty_weak
-end)
+module Wty = Ty.W
let mk_ty n = {
ty_node = n;
- ty_weak = Hashweak.create_key ();
- ty_tag = -1
+ ty_tag = Hashweak.dummy_tag;
}
let ty_var n = Hsty.hashcons (mk_ty (Tyvar n))
diff --git a/src/core/ty.mli b/src/core/ty.mli
index 2bdeced92d02bec26a3c1e6b0caef8b1da9e00f8..070292a5f9200660763e3a3fa5c8099871f871bb 100644
--- a/src/core/ty.mli
+++ b/src/core/ty.mli
@@ -31,6 +31,8 @@ module Htv : Hashtbl.S with type key = tvsymbol
val tv_equal : tvsymbol -> tvsymbol -> bool
+val tv_hash : tvsymbol -> int
+
val create_tvsymbol : preid -> tvsymbol
(* type symbols and types *)
@@ -43,8 +45,7 @@ type tysymbol = private {
and ty = private {
ty_node : ty_node;
- ty_weak : Hashweak.key;
- ty_tag : int;
+ ty_tag : Hashweak.tag;
}
and ty_node = private
@@ -56,8 +57,6 @@ 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 : Util.Tagged with type t = ty
-
module Sty : Set.S with type elt = ty
module Mty : Map.S with type key = ty
module Hty : Hashtbl.S with type key = ty
@@ -66,6 +65,9 @@ module Wty : Hashweak.S with type key = ty
val ts_equal : tysymbol -> tysymbol -> bool
val ty_equal : ty -> ty -> bool
+val ts_hash : tysymbol -> int
+val ty_hash : ty -> int
+
exception BadTypeArity of tysymbol * int * int
exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVar of tvsymbol
diff --git a/src/programs/pgm_effect.ml b/src/programs/pgm_effect.ml
index a531f037ab4fb4b147b65dea0c8ea3e675027105..f3955de0ddaff6d7f19459c81a31c94af7c43e7d 100644
--- a/src/programs/pgm_effect.ml
+++ b/src/programs/pgm_effect.ml
@@ -49,21 +49,11 @@ module Reference = struct
type t = reference
- module Vsym = OrderedHash(struct
- type t = vsymbol
- let tag vs = vs.vs_name.id_tag
- end)
-
- module Lsym = OrderedHash(struct
- type t = lsymbol
- let tag ls = ls.ls_name.id_tag
- end)
-
let compare r1 r2 = match r1, r2 with
- | Rlocal v1, Rlocal v2 -> Vsym.compare v1 v2
- | Rglobal l1, Rglobal l2 -> Lsym.compare l1 l2
- | Rlocal _, Rglobal _ -> -1
- | Rglobal _, Rlocal _ -> 1
+ | Rlocal v1, Rlocal v2 -> compare (vs_hash v1) (vs_hash v2)
+ | Rglobal l1, Rglobal l2 -> compare (ls_hash l1) (ls_hash l2)
+ | Rlocal _, Rglobal _ -> -1
+ | Rglobal _, Rlocal _ -> 1
let equal r1 r2 = compare r1 r2 = 0
diff --git a/src/transform/encoding_bridge.ml b/src/transform/encoding_bridge.ml
index efb226ff391f892c82d7760e1ae5eb1a66226ebd..b7fe1e1f151ab98d5ab57aeb18867e81ed229bdd 100644
--- a/src/transform/encoding_bridge.ml
+++ b/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 clone_builtin;
+ clone_builtin = Wts.memoize 7 clone_builtin;
specials = specials;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol}
diff --git a/src/transform/encoding_instantiate.ml b/src/transform/encoding_instantiate.ml
index 8cc33066178bea224bb0072d169f2871087b4565..347707adc4e06b0b5157a8570f77e9693a2f4398 100644
--- a/src/transform/encoding_instantiate.ml
+++ b/src/transform/encoding_instantiate.ml
@@ -40,7 +40,11 @@ let ty_dumb = ty_var tv_dumb
instantié. Un tag sur un logique polymorphe doit être un tag sur toute
la famille de fonctions *)
-module OHTyl = OrderedHashList(Tty)
+module OHTyl = OrderedHashList(struct
+ type t = ty
+ let tag = ty_hash
+end)
+
module Mtyl = Map.Make(OHTyl)
type tenv_aux = {
diff --git a/src/transform/encoding_simple.ml b/src/transform/encoding_simple.ml
index 826b866ade994d7ed19ccb330e439f01070ecac0..24e6fe9ce92a2835ad243659802315c8e505598d 100644
--- a/src/transform/encoding_simple.ml
+++ b/src/transform/encoding_simple.ml
@@ -69,7 +69,7 @@ let init_tenv kept =
in
task,
{ kept = kept;
- declare_kept = Wts.memoize declare_kept;
+ declare_kept = Wts.memoize 7 declare_kept;
specials = specials;
ty_uni = ty_uni;
trans_lsymbol = Hls.create 17 }
diff --git a/src/transform/hypothesis_selection.ml b/src/transform/hypothesis_selection.ml
index 8555aca012cab167f08bf3fb500b6082bfa8ab66..cf50fb74cda0d47d1826c0b81160aefff3507986 100644
--- a/src/transform/hypothesis_selection.ml
+++ b/src/transform/hypothesis_selection.ml
@@ -38,41 +38,29 @@ end
open Graph
module GP = Graph.Persistent.Digraph.ConcreteLabeled(
struct
- type t = Term.lsymbol
- let compare x y = compare x.ls_name.id_tag y.ls_name.id_tag
- let hash x = x.ls_name.id_tag
- let equal x y = x.ls_name.id_tag = y.ls_name.id_tag
+ type t = lsymbol
+ let compare x y = compare (ls_hash x) (ls_hash y)
+ let hash = ls_hash
+ let equal = ls_equal
end)(Int_Dft)
(** a way to compare/hash expressions *)
module ExprNode = struct
type t = Term.expr
+
let compare x y = match x,y with
- | Term t1, Term t2 -> compare t1.t_tag t2.t_tag
- | Fmla f1, Fmla f2 -> compare f1.f_tag f2.f_tag
+ | Term t1, Term t2 -> compare (t_hash t1) (t_hash t2)
+ | Fmla f1, Fmla f2 -> compare (f_hash f1) (f_hash f2)
| Term _, Fmla _ -> -1
| Fmla _, Term _ -> 1
+
let hash x = match x with
- | Term t -> t.t_tag
- | Fmla f -> f.f_tag
+ | Term t -> 2 * (t_hash t)
+ | Fmla f -> 2 * (f_hash f) + 1
+
let equal x y = compare x y == 0
end
module GC = Graph.Persistent.Graph.Concrete(ExprNode)
-module SymbHashtbl =
- Hashtbl.Make(struct type t = Term.lsymbol
- let equal x y = x.ls_name.id_tag = y.ls_name.id_tag
- let hash x = x.ls_name.id_tag
- end)
-module FmlaHashtbl =
- Hashtbl.Make(struct type t = Term.fmla
- let equal x y = x.f_tag = y.f_tag
- let hash x = x.f_tag
- end)
-module TermHashtbl =
- Hashtbl.Make(struct type t = Term.term
- let equal x y = x.t_tag = y.t_tag
- let hash x = x.t_tag
- end)
module Sls = Set.Make(GP.V)
module Sexpr = Set.Make(ExprNode)
@@ -189,12 +177,12 @@ module NF = struct (* add memoization, one day ? *)
let var,_,f = f_open_quant f_bound in
traverse fmlaTable old_fmla (var@vars) f
| _ ->
- if FmlaHashtbl.mem fmlaTable fmla then
- [[FmlaHashtbl.find fmlaTable fmla]]
+ if Hfmla.mem fmlaTable fmla then
+ [[Hfmla.find fmlaTable fmla]]
else
let new_fmla = create_fmla vars in
- FmlaHashtbl.add fmlaTable old_fmla new_fmla;
- FmlaHashtbl.add fmlaTable new_fmla new_fmla;
+ Hfmla.add fmlaTable old_fmla new_fmla;
+ Hfmla.add fmlaTable new_fmla new_fmla;
[[new_fmla]]
(** skips prenex quantifiers *)
@@ -244,21 +232,21 @@ end
(** module used to compute the graph of relations between constants *)
module GraphConstant = struct
-
+
(** memoizing for formulae and terms, and then expressions *)
let rec findF fTbl fmla = try
- FmlaHashtbl.find fTbl fmla
+ Hfmla.find fTbl fmla
with Not_found ->
let new_v = GC.V.create (Fmla fmla) in
- FmlaHashtbl.add fTbl fmla new_v;
+ Hfmla.add fTbl fmla new_v;
(* Format.eprintf "generating new vertex : %a@."
Pretty.print_fmla fmla; *)
new_v
and findT tTbl term = try
- TermHashtbl.find tTbl term
+ Hterm.find tTbl term
with Not_found ->
let new_v = GC.V.create (Term term) in
- TermHashtbl.add tTbl term new_v;
+ Hterm.add tTbl term new_v;
(* Format.eprintf "generating new vertex : %a@."
Pretty.print_fmla fmla; *)
new_v
@@ -321,7 +309,7 @@ module GraphConstant = struct
List.fold_left (analyse_clause fTbl tTbl) gc clauses
(** processes a single task_head. *)
- let update fmlaTable fTbl tTbl gc task_head =
+ let update fmlaTable fTbl tTbl gc task_head =
match task_head.task_decl.Theory.td_node with
| Theory.Decl {d_node = Dprop(_,_,prop_decl)} ->
analyse_prop fmlaTable fTbl tTbl gc prop_decl
@@ -349,10 +337,10 @@ module GraphPredicate = struct
with Exit p -> p
let find symbTbl x = try
- SymbHashtbl.find symbTbl x
+ Hls.find symbTbl x
with Not_found ->
let new_v = GP.V.create x in
- SymbHashtbl.add symbTbl x new_v;
+ Hls.add symbTbl x new_v;
(* Format.eprintf "generating new vertex : %a@." Pretty.print_ls x; *)
new_v
@@ -524,7 +512,7 @@ module Select = struct
| (_,`Negative) -> true
| (_,`Positive) -> false in
let find_secure symbTbl x =
- try SymbHashtbl.find symbTbl x
+ try Hls.find symbTbl x
with Not_found ->
Format.eprintf "failure finding %a !@." Pretty.print_ls x;
raise Not_found in
@@ -555,7 +543,7 @@ module Select = struct
List.fold_left Util.merge_list []
(List.map (build_relevant_variables gc) goal_clauses) in
function fmla ->
- let rec is_close_enough x l count = match (l,count) with
+ let rec is_close_enough x l count = match (l,count) with
| _,n when n < 0 -> false
| y::_,_ when Sexpr.mem x y -> true
| _::ys,count -> is_close_enough x ys (count-1)
@@ -609,7 +597,7 @@ let transformation fmlaTable fTbl tTbl symbTbl task =
(* first, collect data in 2 graphes *)
let (gc,gp,goal_option) =
Trans.apply (collect_info fmlaTable fTbl tTbl symbTbl) task in
- Format.fprintf Format.err_formatter "graph: @\n@\n%a@\n@." Dot_.fprint_graph gc;
+ Format.fprintf Format.err_formatter "graph: @\n@\n%a@\n@." Dot_.fprint_graph gc;
(* get the goal *)
let goal_fmla = match goal_option with
| None -> failwith "no goal !"
@@ -622,10 +610,10 @@ let transformation fmlaTable fTbl tTbl symbTbl task =
(** the transformation to be registered *)
let hypothesis_selection = (* create lots of hashtables... *)
- let fmlaTable = FmlaHashtbl.create 17 in
- let fTbl = FmlaHashtbl.create 17 in
- let tTbl = TermHashtbl.create 17 in
- let symbTbl = SymbHashtbl.create 17 in
+ let fmlaTable = Hfmla.create 17 in
+ let fTbl = Hfmla.create 17 in
+ let tTbl = Hterm.create 17 in
+ let symbTbl = Hls.create 17 in
Trans.store (transformation fmlaTable fTbl tTbl symbTbl)
let _ = Trans.register_transform "hypothesis_selection" hypothesis_selection
diff --git a/src/util/hashweak.ml b/src/util/hashweak.ml
index eb9121f32576b3e1ab840de39e0d38b7b24df003..bf37dba99f3b6d16d9caada8ecc10ca1a303d91e 100644
--- a/src/util/hashweak.ml
+++ b/src/util/hashweak.ml
@@ -17,17 +17,19 @@
(* *)
(**************************************************************************)
-module Weak : sig
+module type S = sig
type key
type 'a t
- val create_key : unit -> key
-
- val create : unit -> 'a t
+ val create : int -> 'a t
(* create a hashtbl with weak keys *)
+ val clear : 'a t -> unit
+
+ val copy : 'a t -> 'a t
+
val find : 'a t -> key -> 'a
(* find the value bound to a key.
Raises Not_found if there is no binding *)
@@ -38,90 +40,121 @@ module Weak : sig
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
+ val remove : 'a t -> key -> unit
+ (* remove the value *)
- type 'a t = int
+ val iter : (key -> 'a -> unit) -> 'a t -> unit
- let create_key () = lazy (Hashtbl.create 3)
+ val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
- let create = let c = ref (-1) in fun () -> incr c; !c
+ val iterk : (key -> unit) -> 'a t -> unit
- 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)
+ val foldk : (key -> 'b -> 'b) -> 'a t -> 'b -> 'b
-end
-
-include Weak
-
-module type S = sig
+ val length : 'a t -> int
- type key
+ val memoize : int -> (key -> 'a) -> (key -> 'a)
+ (* create a memoizing function *)
- type 'a t
+ val memoize_option : int -> (key option -> 'a) -> (key option -> 'a)
+ (* memoizing functions on option types *)
- val create : unit -> 'a t
- (* create a hashtbl with weak keys *)
+end
- val find : 'a t -> key -> 'a
- (* find the value bound to a key.
- Raises Not_found if there is no binding *)
+type tag = {
+ tag_map : ((int,Obj.t) Hashtbl.t) Lazy.t;
+ tag_tag : int;
+}
- val mem : 'a t -> key -> bool
- (* test if a key is bound *)
+let create_tag tag = {
+ tag_map = lazy (Hashtbl.create 3);
+ tag_tag = tag;
+}
- val set : 'a t -> key -> 'a -> unit
- (* bind the key _once_ with the given value *)
+let dummy_tag = {
+ tag_map = lazy (failwith "dummy tag");
+ tag_tag = -1;
+}
- val memoize : (key -> 'a) -> (key -> 'a)
- (* create a memoizing function *)
+let tag_hash k = assert (k != dummy_tag); k.tag_tag
- val memoize_option : (key option -> 'a) -> (key option -> 'a)
- (* memoizing functions on option types *)
+let tag_equal k1 k2 = k1.tag_tag = k2.tag_tag
-end
+let tag_compare k1 k2 = Pervasives.compare k1.tag_tag k2.tag_tag
module type Weakey =
sig
type t
- val key : t -> Weak.key
+ val tag : t -> tag
end
module Make (S : Weakey) = struct
type key = S.t
- type 'a t = 'a Weak.t
+ module H = Weak.Make (struct
+ type t = S.t
+ let hash k = (S.tag k).tag_tag
+ let equal k1 k2 = S.tag k1 == S.tag k2
+ end)
+
+ type 'a t = {
+ tbl_set : H.t;
+ tbl_tag : int;
+ }
+
+ let tag_map k = Lazy.force (S.tag k).tag_map
+
+ let find (t : 'a t) k : 'a =
+ Obj.obj (Hashtbl.find (tag_map k) t.tbl_tag)
+
+ let mem t k = Hashtbl.mem (tag_map k) t.tbl_tag
+
+ let set (t : 'a t) k (v : 'a) =
+ Hashtbl.replace (tag_map k) t.tbl_tag (Obj.repr v);
+ H.add t.tbl_set k
+
+ let remove t k =
+ Hashtbl.remove (tag_map k) t.tbl_tag;
+ H.remove t.tbl_set k
+
+ let iterk fn t = H.iter fn t.tbl_set
+ let foldk fn t = H.fold fn t.tbl_set
+
+ let iter fn t = H.iter (fun k -> fn k (find t k)) t.tbl_set
+ let fold fn t = H.fold (fun k -> fn k (find t k)) t.tbl_set
+
+ let tbl_final t = iterk (fun k -> Hashtbl.remove (tag_map k) t.tbl_tag) t
- let create = Weak.create
+ let create = let c = ref (-1) in fun n ->
+ let t = {
+ tbl_set = H.create n;
+ tbl_tag = (incr c; !c) }
+ in
+ Gc.finalise tbl_final t;
+ t
- let set_key h = Weak.set h
- let mem_key h = Weak.mem h
- let find_key h = Weak.find h
+ let clear t = tbl_final t; H.clear t.tbl_set
- let set_key h k v =
- assert (not (mem_key h k));
- set_key h k v
+ let length t = H.count t.tbl_set
- 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 copy t =
+ let t' = create (length t) in
+ iter (set t') t;
+ t'
- let memoize fn =
- let h = create () in fun e ->
- let k = S.key e in
- try find_key h k
+ let memoize n fn =
+ let h = create n in fun e ->
+ try find h e
with Not_found ->
let v = fn e in
- set_key h k v;
+ set h e v;
v
- let memoize_option fn =
+ let memoize_option n fn =
let v = lazy (fn None) in
let fn e = fn (Some e) in
- let fn = memoize fn in
+ let fn = memoize n fn in
function
| Some e -> fn e
| None -> Lazy.force v
diff --git a/src/util/hashweak.mli b/src/util/hashweak.mli
index 9455b26f819143c3db6d620e5e6f00376bc05c06..4d5a2f3a0947233f9e5c9508c96961c4594d91de 100644
--- a/src/util/hashweak.mli
+++ b/src/util/hashweak.mli
@@ -19,24 +19,17 @@
(** Hashtable with weak key used for memoization *)
-type key
+type tag
-type 'a t
+val dummy_tag : tag
-val create_key : unit -> key
+val create_tag : int -> tag
-val create : unit -> 'a t
- (* create a hashtbl with weak keys *)
+val tag_hash : tag -> int
-val find : 'a t -> key -> 'a
- (* find the value bound to a key.
- Raises Not_found if there is no binding *)
+val tag_equal : tag -> tag -> bool
-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 *)
+val tag_compare : tag -> tag -> int
module type S = sig
@@ -44,9 +37,13 @@ module type S = sig
type 'a t
- val create : unit -> 'a t
+ val create : int -> 'a t
(* create a hashtbl with weak keys *)
+ val clear : 'a t -> unit
+
+ val copy : 'a t -> 'a t
+
val find : 'a t -> key -> 'a
(* find the value bound to a key.
Raises Not_found if there is no binding *)
@@ -57,10 +54,23 @@ module type S = sig
val set : 'a t -> key -> 'a -> unit
(* bind the key _once_ with the given value *)
- val memoize : (key -> 'a) -> (key -> 'a)
+ val remove : 'a t -> key -> unit
+ (* remove the value *)
+
+ val iter : (key -> 'a -> unit) -> 'a t -> unit
+
+ val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+
+ val iterk : (key -> unit) -> 'a t -> unit
+
+ val foldk : (key -> 'b -> 'b) -> 'a t -> 'b -> 'b
+
+ val length : 'a t -> int
+
+ val memoize : int -> (key -> 'a) -> (key -> 'a)
(* create a memoizing function *)
- val memoize_option : (key option -> 'a) -> (key option -> 'a)
+ val memoize_option : int -> (key option -> 'a) -> (key option -> 'a)
(* memoizing functions on option types *)
end
@@ -68,7 +78,7 @@ end
module type Weakey =
sig
type t
- val key : t -> key
+ val tag : t -> tag
end
module Make (S : Weakey) : S with type key = S.t
diff --git a/src/util/util.ml b/src/util/util.ml
index 37d9e35ca768bfcf1176bb8216d55d70418960dc..f2e2043a2e442d123cc8da6933b7d778abf17075 100644
--- a/src/util/util.ml
+++ b/src/util/util.ml
@@ -148,6 +148,21 @@ struct
module H = Hashtbl.Make(T)
end
+module MakeTagged (X : Hashweak.Weakey) =
+struct
+ type t = X.t
+ let tag t = Hashweak.tag_hash (X.tag t)
+end
+
+module WeakStructMake (X : Hashweak.Weakey) =
+struct
+ module T = OrderedHash(MakeTagged(X))
+ module S = Set.Make(T)
+ module M = Map.Make(T)
+ module H = Hashtbl.Make(T)
+ module W = Hashweak.Make(X)
+end
+
(* memoization *)
let memo ?(size=17) f =
diff --git a/src/util/util.mli b/src/util/util.mli
index 8932cf02768dbe49deb4a583ec55818348036d07..812c155124a2780996fb6c71ea889f902c554ea4 100644
--- a/src/util/util.mli
+++ b/src/util/util.mli
@@ -110,6 +110,14 @@ sig
module H : Hashtbl.S with type key = X.t
end
+module WeakStructMake (X : Hashweak.Weakey) :
+sig
+ module S : Set.S with type elt = X.t
+ module M : Map.S with type key = X.t
+ module H : Hashtbl.S with type key = X.t
+ module W : Hashweak.S with type key = X.t
+end
+
(* memoization *)
val memo : ?size:int -> ('a -> 'b) -> 'a -> 'b