aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib2
-rw-r--r--kernel/names.ml38
-rw-r--r--kernel/term.ml12
-rw-r--r--kernel/univ.ml16
-rw-r--r--lib/hashcons.ml34
-rw-r--r--lib/hashcons.mli67
-rw-r--r--lib/hashset.ml (renamed from lib/hashtbl_alt.ml)14
-rw-r--r--lib/hashset.mli (renamed from lib/hashtbl_alt.mli)6
-rw-r--r--lib/lib.mllib2
-rw-r--r--plugins/cc/ccalgo.ml2
10 files changed, 116 insertions, 77 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index c2a77f215..703aa9616 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -14,6 +14,7 @@ CList
CArray
Util
Bigint
+Hashset
Hashcons
Dyn
CUnix
@@ -31,7 +32,6 @@ Rtree
Heap
Option
Dnet
-Hashtbl_alt
Names
Univ
diff --git a/kernel/names.ml b/kernel/names.ml
index 6146e1083..d2c06104b 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -353,7 +353,7 @@ module Hname = Hashcons.Make(
struct
type t = name
type u = identifier -> identifier
- let hash_sub hident = function
+ let hashcons hident = function
| Name id -> Name (hident id)
| n -> n
let equal n1 n2 =
@@ -369,7 +369,7 @@ module Hdir = Hashcons.Make(
struct
type t = dir_path
type u = identifier -> identifier
- let hash_sub hident d = List.smartmap hident d
+ let hashcons hident d = List.smartmap hident d
let rec equal d1 d2 =
(d1==d2) ||
match (d1,d2) with
@@ -383,7 +383,7 @@ module Huniqid = Hashcons.Make(
struct
type t = uniq_ident
type u = (identifier -> identifier) * (dir_path -> dir_path)
- let hash_sub (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
+ let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
(x == y) ||
(n1 = n2 && s1 == s2 && dir1 == dir2)
@@ -395,10 +395,10 @@ module Hmod = Hashcons.Make(
type t = module_path
type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
(string -> string)
- let rec hash_sub (hdir,huniqid,hstr as hfuns) = function
+ let rec hashcons (hdir,huniqid,hstr as hfuns) = function
| MPfile dir -> MPfile (hdir dir)
| MPbound m -> MPbound (huniqid m)
- | MPdot (md,l) -> MPdot (hash_sub hfuns md, hstr l)
+ | MPdot (md,l) -> MPdot (hashcons hfuns md, hstr l)
let rec equal d1 d2 =
d1 == d2 ||
match (d1,d2) with
@@ -414,7 +414,7 @@ module Hkn = Hashcons.Make(
type t = kernel_name
type u = (module_path -> module_path)
* (dir_path -> dir_path) * (string -> string)
- let hash_sub (hmod,hdir,hstr) (md,dir,l) =
+ let hashcons (hmod,hdir,hstr) (md,dir,l) =
(hmod md, hdir dir, hstr l)
let equal (mod1,dir1,l1) (mod2,dir2,l2) =
mod1 == mod2 && dir1 == dir2 && l1 == l2
@@ -429,7 +429,7 @@ module Hcn = Hashcons.Make(
struct
type t = kernel_name*kernel_name
type u = kernel_name -> kernel_name
- let hash_sub hkn (user,can) = (hkn user, hkn can)
+ let hashcons hkn (user,can) = (hkn user, hkn can)
let equal (user1,_) (user2,_) = user1 == user2
let hash (user,_) = Hashtbl.hash user
end)
@@ -438,7 +438,7 @@ module Hind = Hashcons.Make(
struct
type t = inductive
type u = mutual_inductive -> mutual_inductive
- let hash_sub hmind (mind, i) = (hmind mind, i)
+ let hashcons hmind (mind, i) = (hmind mind, i)
let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
let hash = Hashtbl.hash
end)
@@ -447,23 +447,23 @@ module Hconstruct = Hashcons.Make(
struct
type t = constructor
type u = inductive -> inductive
- let hash_sub hind (ind, j) = (hind ind, j)
+ let hashcons hind (ind, j) = (hind ind, j)
let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
let hash = Hashtbl.hash
end)
-let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f ()
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate ()
let hcons_ident = hcons_string
-let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident
-let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident
-let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath)
+let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident
+let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident
+let hcons_uid = Hashcons.simple_hcons Huniqid.generate (hcons_ident,hcons_dirpath)
let hcons_mp =
- Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string)
-let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string)
-let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn
-let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn
-let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind
-let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind
+ Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,hcons_string)
+let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,hcons_string)
+let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
+let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
+let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.generate hcons_ind
(*******)
diff --git a/kernel/term.ml b/kernel/term.ml
index e54e56f12..8ab04af24 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1236,9 +1236,9 @@ let equals_constr t1 t2 =
(** Note that the following Make has the side effect of creating
once and for all the table we'll use for hash-consing all constr *)
-module H = Hashtbl_alt.Make(struct type t = constr let equals = equals_constr end)
+module H = Hashset.Make(struct type t = constr let equal = equals_constr end)
-open Hashtbl_alt.Combine
+open Hashset.Combine
(* [hcons_term hash_consing_functions constr] computes an hash-consed
representation for [constr] using [hash_consing_functions] on
@@ -1369,7 +1369,7 @@ module Hsorts =
struct
type t = sorts
type u = universe -> universe
- let hash_sub huniv = function
+ let hashcons huniv = function
Prop c -> Prop c
| Type u -> Type (huniv u)
let equal s1 s2 =
@@ -1385,7 +1385,7 @@ module Hcaseinfo =
struct
type t = case_info
type u = inductive -> inductive
- let hash_sub hind ci = { ci with ci_ind = hind ci.ci_ind }
+ let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
let equal ci ci' =
ci.ci_ind == ci'.ci_ind &&
ci.ci_npar = ci'.ci_npar &&
@@ -1394,8 +1394,8 @@ module Hcaseinfo =
let hash = Hashtbl.hash
end)
-let hcons_sorts = Hashcons.simple_hcons Hsorts.f hcons_univ
-let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.f hcons_ind
+let hcons_sorts = Hashcons.simple_hcons Hsorts.generate hcons_univ
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
let hcons_constr =
hcons_term
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9334a06d1..faadb1081 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -874,7 +874,7 @@ module Hunivlevel =
struct
type t = universe_level
type u = Names.dir_path -> Names.dir_path
- let hash_sub hdir = function
+ let hashcons hdir = function
| UniverseLevel.Set -> UniverseLevel.Set
| UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d)
let equal l1 l2 =
@@ -892,7 +892,7 @@ module Huniv =
struct
type t = universe
type u = universe_level -> universe_level
- let hash_sub hdir = function
+ let hashcons hdir = function
| Atom u -> Atom (hdir u)
| Max (gel,gtl) -> Max (List.map hdir gel, List.map hdir gtl)
let equal u v =
@@ -906,15 +906,15 @@ module Huniv =
let hash = Hashtbl.hash
end)
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath
-let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel
+let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.hcons_dirpath
+let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel
module Hconstraint =
Hashcons.Make(
struct
type t = univ_constraint
type u = universe_level -> universe_level
- let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2)
+ let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
let equal (l1,k,l2) (l1',k',l2') =
l1 == l1' && k = k' && l2 == l2'
let hash = Hashtbl.hash
@@ -925,7 +925,7 @@ module Hconstraints =
struct
type t = constraints
type u = univ_constraint -> univ_constraint
- let hash_sub huc s =
+ let hashcons huc s =
Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
let equal s s' =
List.for_all2eq (==)
@@ -934,5 +934,5 @@ module Hconstraints =
let hash = Hashtbl.hash
end)
-let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel
-let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate hcons_univlevel
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 7c2897be0..f71af15c7 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -13,29 +13,29 @@
(* [t] is the type of object to hash-cons
* [u] is the type of hash-cons functions for the sub-structures
* of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...).
- * [hash_sub u x] is a function that hash-cons the sub-structures of x using
+ * [hashcons u x] is a function that hash-cons the sub-structures of x using
* the hash-consing functions u provides.
* [equal] is a comparison function. It is allowed to use physical equality
- * on the sub-terms hash-consed by the hash_sub function.
+ * on the sub-terms hash-consed by the hashcons function.
* [hash] is the hash function given to the Hashtbl.Make function
*
* Note that this module type coerces to the argument of Hashtbl.Make.
*)
-module type Comp =
+module type HashconsedType =
sig
type t
type u
- val hash_sub : u -> t -> t
+ val hashcons : u -> t -> t
val equal : t -> t -> bool
val hash : t -> int
end
-(* The output is a function f such that
- * [f ()] has the side-effect of creating (internally) a hash-table of the
+(* The output is a function [generate] such that
+ * [generate ()] has the side-effect of creating (internally) a hash-table of the
* hash-consed objects. The result is a function taking the sub-hashcons
* functions and an object, and hashcons it. It does not really make sense
- * to call f() with different sub-hcons functions. That's why we use the
+ * to call generate() with different sub-hcons functions. That's why we use the
* wrappers simple_hcons, recursive_hcons, ... The latter just take as
* argument the sub-hcons functions (the tables are created at that moment),
* and returns the hcons function for t.
@@ -45,10 +45,10 @@ module type S =
sig
type t
type u
- val f : unit -> (u -> t -> t)
+ val generate : unit -> (u -> t -> t)
end
-module Make(X:Comp) =
+module Make (X : HashconsedType) =
struct
type t = X.t
type u = X.u
@@ -66,20 +66,20 @@ module Make(X:Comp) =
(* The table is created when () is applied.
* Hashconsing is then very simple:
- * 1- hashcons the subterms using hash_sub and u
+ * 1- hashcons the subterms using hashcons and u
* 2- look up in the table, if we do not get a hit, we add it
*)
- let f () =
+ let generate () =
let tab = Htbl.create 97 in
(fun u x ->
- let y = X.hash_sub u x in
+ let y = X.hashcons u x in
(* incr acces;*)
try let r = Htbl.find tab y in(* incr succes;*) r
with Not_found -> Htbl.add tab y y; y)
end
(* A few usefull wrappers:
- * takes as argument the function f above and build a function of type
+ * takes as argument the function [generate] above and build a function of type
* u -> t -> t that creates a fresh table each time it is applied to the
* sub-hcons functions. *)
@@ -136,7 +136,7 @@ module Hstring = Make(
struct
type t = string
type u = unit
- let hash_sub () s =(* incr accesstr;*) s
+ let hashcons () s =(* incr accesstr;*) s
let equal s1 s2 =(* incr comparaisonstr;
if*) s1=s2(* then (incr successtr; true) else false*)
let hash = Hashtbl.hash
@@ -175,7 +175,7 @@ module Hobj = Make(
struct
type t = Obj.t
type u = (Obj.t -> Obj.t) * unit
- let hash_sub (hrec,_) = hash_obj hrec
+ let hashcons (hrec,_) = hash_obj hrec
let equal = comp_obj
let hash = Hashtbl.hash
end)
@@ -185,8 +185,8 @@ module Hobj = Make(
*)
(* string : string -> string *)
(* obj : Obj.t -> Obj.t *)
-let string = register_hcons (simple_hcons Hstring.f) ()
-let obj = register_hcons (recursive_hcons Hobj.f) ()
+let string = register_hcons (simple_hcons Hstring.generate) ()
+let obj = register_hcons (recursive_hcons Hobj.generate) ()
(* The unsafe polymorphic hashconsing function *)
let magic_hash (c : 'a) =
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index b4a9da2f8..bafec6f91 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -8,43 +8,82 @@
(** Generic hash-consing. *)
-module type Comp =
+module type HashconsedType =
sig
+ (** {6 Generic hashconsing signature}
+
+ Given an equivalence relation [equal], a hashconsing function is a
+ function that associates the same canonical element to two elements
+ related by [equal]. Usually, the element chosen is canonical w.r.t.
+ physical equality [(==)], so as to reduce memory consumption and
+ enhance efficiency of equality tests.
+
+ In order to ensure canonicality, we need a way to remember the element
+ associated to a class of equivalence; this is done using a hidden state
+ generated by the [Make] functor.
+ *)
+
type t
+ (** Type of objects to hashcons. *)
type u
- val hash_sub : u -> t -> t
+ (** Type of hashcons functions for the sub-structures contained in [t].
+ Usually a tuple of functions. *)
+ val hashcons : u -> t -> t
+ (** The actual hashconsing function, using its fist argument to recursively
+ hashcons substructures. *)
val equal : t -> t -> bool
+ (** A comparison function. It is allowed to use physical equality
+ on the sub-terms hashconsed by the [hashcons] function. *)
val hash : t -> int
+ (** A hash function passed to the underlying hashtable structure. *)
end
module type S =
sig
type t
+ (** Type of objects to hashcons. *)
type u
- val f : unit -> (u -> t -> t)
+ (** Type of hashcons functions for the sub-structures contained in [t]. *)
+ val generate : unit -> (u -> t -> t)
+ (** This has the side-effect of creating (internally) a hashtable of the
+ hashconsed objects. The result is a function taking the sub-hashcons
+ functions and an object, and hashconsing it. It does not really make sense
+ to call [generate] with different sub-hcons functions. That's why we use the
+ wrappers [simple_hcons], [recursive_hcons], ... The latter just take as
+ argument the sub-hcons functions (the tables are created at that moment),
+ and returns the hcons function for [t]. *)
end
-module Make(X:Comp) : (S with type t = X.t and type u = X.u)
+module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u)
+(** Create a new hashconsing, given canonicalization functions. *)
+
+(** {6 Wrappers} *)
+
+(** * These are intended to be used together with instances of the [Make]
+ functor. *)
val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't)
+(** [simple_hcons f sub obj] creates a new table each time it is applied to any
+ sub-hash function [sub]. *)
+
val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+(** As [simple_hcons] but intended to be used with well-founded data structures. *)
+
val recursive_loop_hcons :
(unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't)
+(** As [simple_hcons] but intended to be used with any recursive data structure,
+ in particular if they contain loops. *)
+
val recursive2_hcons :
(unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u1 -> 't1 -> 't1) ->
(unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) ->
'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2)
+(** As [recursive_hcons] but with two mutually recursive structures. *)
-(** Declaring and reinitializing global hash-consing functions *)
-
-val init : unit -> unit
-val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't)
+(** {6 Hashconsing of usual structures} *)
module Hstring : (S with type t = string and type u = unit)
-module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
-
-val string : string -> string
-val obj : Obj.t -> Obj.t
-
-val magic_hash : 'a -> 'a
+(** Hashconsing of strings. *)
+module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
+(** Hashconsing of OCaml values. *)
diff --git a/lib/hashtbl_alt.ml b/lib/hashset.ml
index 2780afe8f..28767df8f 100644
--- a/lib/hashtbl_alt.ml
+++ b/lib/hashset.ml
@@ -16,9 +16,9 @@
given to the caller, which makes possible the interleaving of the
hash key computation and the hash-consing. *)
-module type Hashtype = sig
+module type EqType = sig
type t
- val equals : t -> t -> bool
+ val equal : t -> t -> bool
end
module type S = sig
@@ -31,7 +31,7 @@ module type S = sig
val may_add_and_get : int -> elt -> elt
end
-module Make (E : Hashtype) =
+module Make (E : EqType) =
struct
type elt = E.t
@@ -72,7 +72,7 @@ module Make (E : Hashtype) =
| Empty ->
add hash key; key
| Cons (k, h, rest) ->
- if hash == h && E.equals key k then k else aux rest
+ if hash == h && E.equal key k then k else aux rest
in
aux bucket
@@ -81,15 +81,15 @@ module Make (E : Hashtype) =
match odata.(hash mod (Array.length odata)) with
| Empty -> add hash key; key
| Cons (k1, h1, rest1) ->
- if hash == h1 && E.equals key k1 then k1 else
+ if hash == h1 && E.equal key k1 then k1 else
match rest1 with
| Empty -> add hash key; key
| Cons (k2, h2, rest2) ->
- if hash == h2 && E.equals key k2 then k2 else
+ if hash == h2 && E.equal key k2 then k2 else
match rest2 with
| Empty -> add hash key; key
| Cons (k3, h3, rest3) ->
- if hash == h2 && E.equals key k3 then k3
+ if hash == h2 && E.equal key k3 then k3
else find_rec hash key rest3
end
diff --git a/lib/hashtbl_alt.mli b/lib/hashset.mli
index 7a1dcd57f..4b260791b 100644
--- a/lib/hashtbl_alt.mli
+++ b/lib/hashset.mli
@@ -16,9 +16,9 @@
given to the caller, which makes possible the interleaving of the
hash key computation and the hash-consing. *)
-module type Hashtype = sig
+module type EqType = sig
type t
- val equals : t -> t -> bool
+ val equal : t -> t -> bool
end
module type S = sig
@@ -31,7 +31,7 @@ module type S = sig
val may_add_and_get : int -> elt -> elt
end
-module Make (E : Hashtype) : S with type elt = E.t
+module Make (E : EqType) : S with type elt = E.t
module Combine : sig
val combine : int -> int -> int
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 21eb7a4a5..a7d56c666 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -4,6 +4,7 @@ Compat
Loc
Errors
Bigint
+Hashset
Hashcons
Dyn
Segmenttree
@@ -23,4 +24,3 @@ Heap
Dnet
Store
Unionfind
-Hashtbl_alt
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 04038b1a7..40599b827 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -115,7 +115,7 @@ let rec term_equal t1 t2 =
i1 = i2 && j1 = j2 && eq_constructor c1 c2
| _ -> t1 = t2
-open Hashtbl_alt.Combine
+open Hashset.Combine
let rec hash_term = function
| Symb c -> combine 1 (hash_constr c)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 19:37:58 +0000