diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 17:28:00 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-24 17:28:00 +0000 |
commit | 9e37e3b9695a214040c52082b1e7288df9362b33 (patch) | |
tree | bc2bc853f3a01999ac4b07b847e43e747e6f104d | |
parent | 748d4e285c9352b5678e07963a295341cc6acc5b (diff) |
Specializing hash functions for widely used types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/closure.ml | 6 | ||||
-rw-r--r-- | kernel/constr.ml | 67 | ||||
-rw-r--r-- | kernel/evar.ml | 1 | ||||
-rw-r--r-- | kernel/evar.mli | 3 | ||||
-rw-r--r-- | kernel/names.ml | 58 | ||||
-rw-r--r-- | kernel/names.mli | 21 | ||||
-rw-r--r-- | kernel/nativecode.ml | 8 | ||||
-rw-r--r-- | kernel/sorts.ml | 15 | ||||
-rw-r--r-- | kernel/sorts.mli | 1 | ||||
-rw-r--r-- | kernel/univ.ml | 34 | ||||
-rw-r--r-- | kernel/univ.mli | 6 | ||||
-rw-r--r-- | lib/cString.ml | 11 | ||||
-rw-r--r-- | lib/cString.mli | 3 | ||||
-rw-r--r-- | lib/hashcons.ml | 23 | ||||
-rw-r--r-- | lib/hashcons.mli | 6 | ||||
-rw-r--r-- | lib/int.ml | 2 |
16 files changed, 211 insertions, 54 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index a32be4f69..98fb467c8 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -213,7 +213,11 @@ module IdKeyHash = struct type t = id_key let equal = Names.eq_id_key - let hash = Hashtbl.hash + open Hashset.Combine + let hash = function + | ConstKey c -> combinesmall 1 (Constant.hash c) + | VarKey id -> combinesmall 2 (Id.hash id) + | RelKey i -> combinesmall 3 (Int.hash i) end module KeyTable = Hashtbl.Make(IdKeyHash) diff --git a/kernel/constr.ml b/kernel/constr.ml index bd6326cf4..6a71b0cfc 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -542,6 +542,12 @@ let term_array_table = HashsetTermArray.create 4999 open Hashset.Combine +let hash_cast_kind = function +| VMcast -> 0 +| NATIVEcast -> 1 +| DEFAULTcast -> 2 +| REVERTcast -> 3 + (* [hashcons hash_consing_functions constr] computes an hash-consed representation for [constr] using [hash_consing_functions] on leaves. *) @@ -549,39 +555,39 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let rec hash_term t = match t with | Var i -> - (Var (sh_id i), combinesmall 1 (Hashtbl.hash i)) + (Var (sh_id i), combinesmall 1 (Id.hash i)) | Sort s -> - (Sort (sh_sort s), combinesmall 2 (Hashtbl.hash s)) + (Sort (sh_sort s), combinesmall 2 (Sorts.hash s)) | Cast (c, k, t) -> let c, hc = sh_rec c in let t, ht = sh_rec t in - (Cast (c, k, t), combinesmall 3 (combine3 hc (Hashtbl.hash k) ht)) + (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht)) | Prod (na,t,c) -> let t, ht = sh_rec t and c, hc = sh_rec c in - (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Hashtbl.hash na) ht hc)) + (Prod (sh_na na, t, c), combinesmall 4 (combine3 (Name.hash na) ht hc)) | Lambda (na,t,c) -> let t, ht = sh_rec t and c, hc = sh_rec c in - (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Hashtbl.hash na) ht hc)) + (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (Name.hash na) ht hc)) | LetIn (na,b,t,c) -> let b, hb = sh_rec b in let t, ht = sh_rec t in let c, hc = sh_rec c in - (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc)) + (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Name.hash na) hb ht hc)) | App (c,l) -> let c, hc = sh_rec c in let l, hl = hash_term_array l in (App (c,l), combinesmall 7 (combine hl hc)) | Evar (e,l) -> let l, hl = hash_term_array l in - (Evar (e,l), combinesmall 8 (combine (Hashtbl.hash e) hl)) + (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl)) | Const c -> - (Const (sh_con c), combinesmall 9 (Hashtbl.hash c)) - | Ind ((kn,i) as ind) -> - (Ind (sh_ind ind), combinesmall 10 (combine (Hashtbl.hash kn) i)) - | Construct (((kn,i),j) as c)-> - (Construct (sh_construct c), combinesmall 11 (combine3 (Hashtbl.hash kn) i j)) + (Const (sh_con c), combinesmall 9 (Constant.hash c)) + | Ind ind -> + (Ind (sh_ind ind), combinesmall 10 (ind_hash ind)) + | Construct c -> + (Construct (sh_construct c), combinesmall 11 (constructor_hash c)) | Case (ci,p,c,bl) -> let p, hp = sh_rec p and c, hc = sh_rec c in @@ -591,14 +597,18 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = | Fix (ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in - Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; - let h = combine3 (Hashtbl.hash lna) hbl htl in + let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in + let fold accu na = combine (Name.hash na) accu in + let hna = Array.fold_left fold 0 lna in + let h = combine3 hna hbl htl in (Fix (ln,(lna,tl,bl)), combinesmall 13 h) | CoFix(ln,(lna,tl,bl)) -> let bl,hbl = hash_term_array bl in let tl,htl = hash_term_array tl in - Array.iteri (fun i x -> lna.(i) <- sh_na x) lna; - let h = combine3 (Hashtbl.hash lna) hbl htl in + let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in + let fold accu na = combine (Name.hash na) accu in + let hna = Array.fold_left fold 0 lna in + let h = combine3 hna hbl htl in (CoFix (ln,(lna,tl,bl)), combinesmall 14 h) | Meta n -> (t, combinesmall 15 n) @@ -616,9 +626,9 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = and hash_term_array t = let accu = ref 0 in for i = 0 to Array.length t - 1 do - let x, h = sh_rec t.(i) in + let x, h = sh_rec (Array.unsafe_get t i) in accu := combine !accu h; - t.(i) <- x + Array.unsafe_set t i x done; (* [h] must be positive. *) let h = !accu land 0x3FFFFFFF in @@ -636,9 +646,12 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = let rec hash t = match kind t with - | Var i -> combinesmall 1 (Hashtbl.hash i) - | Sort s -> combinesmall 2 (Hashtbl.hash s) - | Cast (c, _, _) -> hash c + | Var i -> combinesmall 1 (Id.hash i) + | Sort s -> combinesmall 2 (Sorts.hash s) + | Cast (c, k, t) -> + let hc = hash c in + let ht = hash t in + combinesmall 3 (combine3 hc (hash_cast_kind k) ht) | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c)) | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c)) | LetIn (_, b, t, c) -> @@ -647,13 +660,13 @@ let rec hash t = | App (c,l) -> combinesmall 7 (combine (hash_term_array l) (hash c)) | Evar (e,l) -> - combinesmall 8 (combine (Hashtbl.hash e) (hash_term_array l)) + combinesmall 8 (combine (Evar.hash e) (hash_term_array l)) | Const c -> - combinesmall 9 (Hashtbl.hash c) (* TODO: proper hash function for constants *) - | Ind (kn,i) -> - combinesmall 10 (combine (Hashtbl.hash kn) i) - | Construct ((kn,i),j) -> - combinesmall 11 (combine3 (Hashtbl.hash kn) i j) + combinesmall 9 (Constant.hash c) + | Ind ind -> + combinesmall 10 (ind_hash ind) + | Construct c -> + combinesmall 11 (constructor_hash c) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) | Fix (ln ,(_, tl, bl)) -> diff --git a/kernel/evar.ml b/kernel/evar.ml index d7e32626f..62d54027c 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -12,6 +12,7 @@ let repr x = x let unsafe_of_int x = x let compare = Int.compare let equal = Int.equal +let hash = Int.hash module Self = struct diff --git a/kernel/evar.mli b/kernel/evar.mli index 8e8b88d94..9f1017351 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -27,5 +27,8 @@ val equal : t -> t -> bool val compare : t -> t -> int (** Comparison over existential variables. *) +val hash : t -> int +(** Hash over existential variables. *) + module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/kernel/names.ml b/kernel/names.ml index 00b8df486..c505017f6 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -32,6 +32,8 @@ struct let compare = String.compare + let hash = String.hash + let check_soft x = let iter (fatal, x) = if fatal then Errors.error x else Pp.msg_warning (str x) @@ -82,6 +84,10 @@ struct | Name id1, Name id2 -> String.equal id1 id2 | _ -> false + let hash = function + | Anonymous -> 0 + | Name id -> Id.hash id + module Self_Hashcons = struct type _t = t @@ -96,7 +102,7 @@ struct | (Name id1, Name id2) -> id1 == id2 | (Anonymous,Anonymous) -> true | _ -> false - let hash = Hashtbl.hash + let hash = hash end module Hname = Hashcons.Make(Self_Hashcons) @@ -141,6 +147,14 @@ struct let equal p1 p2 = Int.equal (compare p1 p2) 0 + let rec hash accu = function + | [] -> accu + | id :: dp -> + let accu = Hashset.Combine.combine (Id.hash id) accu in + hash accu dp + + let hash dp = hash 0 dp + let make x = x let repr x = x @@ -198,6 +212,11 @@ struct let to_id (_, s, _) = s + open Hashset.Combine + + let hash (i, id, dp) = + combine3 (Int.hash i) (Id.hash id) (DirPath.hash dp) + module Self_Hashcons = struct type _t = t @@ -207,7 +226,7 @@ struct let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) = (x == y) || (Int.equal n1 n2 && s1 == s2 && dir1 == dir2) - let hash = Hashtbl.hash + let hash = hash end module HashMBId = Hashcons.Make(Self_Hashcons) @@ -267,6 +286,14 @@ module ModPath = struct let equal mp1 mp2 = Int.equal (compare mp1 mp2) 0 + open Hashset.Combine + + let rec hash = function + | MPfile dp -> combinesmall 1 (DirPath.hash dp) + | MPbound id -> combinesmall 2 (MBId.hash id) + | MPdot (mp, lbl) -> + combinesmall 3 (combine (hash mp) (Label.hash lbl)) + let initial = MPfile DirPath.initial module Self_Hashcons = struct @@ -284,7 +311,7 @@ module ModPath = struct | MPbound m1, MPbound m2 -> m1 == m2 | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2 | _ -> false - let hash = Hashtbl.hash + let hash = hash end module HashMP = Hashcons.Make(Self_Hashcons) @@ -336,6 +363,11 @@ module KerName = struct let equal kn1 kn2 = Int.equal (compare kn1 kn2) 0 + open Hashset.Combine + + let hash (mp, dp, lbl) = + combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) + module Self_Hashcons = struct type t = kernel_name type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t) @@ -344,7 +376,7 @@ module KerName = struct (hmod mp,hdir dir,hstr l) let equal (mp1,dir1,l1) (mp2,dir2,l2) = mp1 == mp2 && dir1 == dir2 && l1 == l2 - let hash = Hashtbl.hash + let hash = hash end module HashKN = Hashcons.Make(Self_Hashcons) @@ -446,6 +478,14 @@ module KerPair = struct the same user part implies having the same canonical part (invariant of the system). *) + open Hashset.Combine + + let hash = function + | Same kn -> combinesmall 1 (KerName.hash kn) + | Dual (kn1, kn2) -> + let hk = combine (KerName.hash kn1) (KerName.hash kn2) in + combinesmall 2 hk + module Self_Hashcons = struct type t = kernel_pair @@ -454,7 +494,7 @@ module KerPair = struct | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) let equal x y = (user x) == (user y) - let hash = Hashtbl.hash + let hash = hash end module HashKP = Hashcons.Make(Self_Hashcons) @@ -500,6 +540,8 @@ let ind_ord (m1, i1) (m2, i2) = let ind_user_ord (m1, i1) (m2, i2) = let c = Int.compare i1 i2 in if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c +let ind_hash (m, i) = + Hashset.Combine.combine (MutInd.hash m) (Int.hash i) let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2 let constructor_ord (ind1, j1) (ind2, j2) = @@ -508,6 +550,8 @@ let constructor_ord (ind1, j1) (ind2, j2) = let constructor_user_ord (ind1, j1) (ind2, j2) = let c = Int.compare j1 j2 in if Int.equal c 0 then ind_user_ord ind1 ind2 else c +let constructor_hash (ind, i) = + Hashset.Combine.combine (ind_hash ind) (Int.hash i) module InductiveOrdered = struct type t = inductive @@ -553,7 +597,7 @@ module Hind = Hashcons.Make( type u = MutInd.t -> MutInd.t let hashcons hmind (mind, i) = (hmind mind, i) let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && Int.equal i1 i2 - let hash = Hashtbl.hash + let hash = ind_hash end) module Hconstruct = Hashcons.Make( @@ -562,7 +606,7 @@ module Hconstruct = Hashcons.Make( type u = inductive -> inductive let hashcons hind (ind, j) = (hind ind, j) let equal (ind1, j1) (ind2, j2) = ind1 == ind2 && Int.equal j1 j2 - let hash = Hashtbl.hash + let hash = constructor_hash end) let hcons_con = Hashcons.simple_hcons Constant.HashKP.generate KerName.hcons diff --git a/kernel/names.mli b/kernel/names.mli index 6f4ac9a53..417e35aaa 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -21,6 +21,9 @@ sig val compare : t -> t -> int (** Comparison over identifiers *) + val hash : t -> int + (** Hash over identifiers *) + val is_valid : string -> bool (** Check that a string may be converted to an identifier. *) @@ -59,6 +62,9 @@ sig val equal : t -> t -> bool (** Equality over names. *) + val hash : t -> int + (** Hash over names. *) + val hcons : t -> t (** Hashconsing over names. *) @@ -86,6 +92,9 @@ sig val compare : t -> t -> int (** Comparison over directory paths. *) + val hash : t -> int + (** Hash over directory paths. *) + val make : module_ident list -> t (** Create a directory path. (The list must be reversed). *) @@ -122,6 +131,9 @@ sig val compare : t -> t -> int (** Comparison over labels. *) + val hash : t -> int + (** Hash over labels. *) + val make : string -> t (** Create a label out of a string. *) @@ -156,6 +168,9 @@ sig val compare : t -> t -> int (** Comparison over unique bound names. *) + val hash : t -> int + (** Hash over unique bound names. *) + val make : DirPath.t -> Id.t -> t (** The first argument is a file name, to prevent conflict between different files. *) @@ -188,6 +203,7 @@ sig val compare : t -> t -> int val equal : t -> t -> bool + val hash : t -> int val is_bound : t -> bool @@ -279,6 +295,9 @@ sig val equal : t -> t -> bool (** Default comparison, alias for [CanOrd.equal] *) + val hash : t -> int + (** Hashing function *) + val change_label : t -> Label.t -> t (** Builds a new constant name with a different label *) @@ -381,10 +400,12 @@ val inductive_of_constructor : constructor -> inductive val index_of_constructor : constructor -> int val eq_ind : inductive -> inductive -> bool val ind_ord : inductive -> inductive -> int +val ind_hash : inductive -> int val ind_user_ord : inductive -> inductive -> int val eq_constructor : constructor -> constructor -> bool val constructor_ord : constructor -> constructor -> int val constructor_user_ord : constructor -> constructor -> int +val constructor_hash : constructor -> int (** Better to have it here that in Closure, since required in grammar.cma *) type evaluable_global_reference = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 874e4a573..d656eceb6 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -148,11 +148,11 @@ open Hashset.Combine let hash_symbol symb = match symb with | SymbValue v -> combinesmall 1 (Hashtbl.hash v) - | SymbSort s -> combinesmall 2 (Hashtbl.hash s) - | SymbName name -> combinesmall 3 (Hashtbl.hash name) - | SymbConst c -> combinesmall 4 (Hashtbl.hash c) + | SymbSort s -> combinesmall 2 (Sorts.hash s) + | SymbName name -> combinesmall 3 (Name.hash name) + | SymbConst c -> combinesmall 4 (Constant.hash c) | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw) - | SymbInd ind -> combinesmall 6 (Hashtbl.hash ind) + | SymbInd ind -> combinesmall 6 (ind_hash ind) module HashedTypeSymbol = struct type t = symbol diff --git a/kernel/sorts.ml b/kernel/sorts.ml index d2469c4fd..04deade92 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -46,6 +46,19 @@ let family = function let family_equal = (==) +open Hashset.Combine + +let hash = function +| Prop p -> + let h = match p with + | Pos -> 0 + | Null -> 1 + in + combinesmall 1 h +| Type u -> + let h = Universe.hash u in + combinesmall 2 h + module Hsorts = Hashcons.Make( struct @@ -59,7 +72,7 @@ module Hsorts = | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false - let hash = Hashtbl.hash + let hash = hash end) let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 51e8a6f6c..b64e92fba 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -22,6 +22,7 @@ val type1 : t val equal : t -> t -> bool val compare : t -> t -> int +val hash : t -> int val is_prop : t -> bool val family : t -> family diff --git a/kernel/univ.ml b/kernel/univ.ml index aa6c9c4c8..9b5c42f56 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -31,9 +31,11 @@ open Util module UniverseLevel = struct + open Names + type t = | Set - | Level of int * Names.DirPath.t + | Level of int * DirPath.t (* A specialized comparison function: we compare the [int] part first. This way, most of the time, the [DirPath.t] part is not considered. @@ -53,19 +55,24 @@ module UniverseLevel = struct | Level (i1, dp1), Level (i2, dp2) -> if i1 < i2 then -1 else if i1 > i2 then 1 - else Names.DirPath.compare dp1 dp2) + else DirPath.compare dp1 dp2) let equal u v = match u,v with | Set, Set -> true | Level (i1, dp1), Level (i2, dp2) -> - Int.equal i1 i2 && Names.DirPath.equal dp1 dp2 + Int.equal i1 i2 && DirPath.equal dp1 dp2 | _ -> false + let hash = function + | Set -> 0 + | Level (i, dp) -> + Hashset.Combine.combine (Int.hash i) (DirPath.hash dp) + let make m n = Level (n, m) let to_string = function | Set -> "Set" - | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (n,d) -> DirPath.to_string d^"."^string_of_int n end module UniverseLMap = Map.Make (UniverseLevel) @@ -109,6 +116,21 @@ struct let make l = Atom l + open Hashset.Combine + + let rec hash_list accu = function + | [] -> 0 + | u :: us -> + let accu = combine (UniverseLevel.hash u) accu in + hash_list accu us + + let hash = function + | Atom u -> combinesmall 1 (UniverseLevel.hash u) + | Max (lt, le) -> + let hlt = hash_list 0 lt in + let hle = hash_list 0 le in + combinesmall 2 (combine hlt hle) + end open Universe @@ -996,7 +1018,7 @@ module Hunivlevel = | UniverseLevel.Level (n,d), UniverseLevel.Level (n',d') -> n == n' && d == d' | _ -> false - let hash = Hashtbl.hash + let hash = UniverseLevel.hash end) module Huniv = @@ -1015,7 +1037,7 @@ module Huniv = (List.for_all2eq (==) gel gel') && (List.for_all2eq (==) gtl gtl') | _ -> false - let hash = Hashtbl.hash + let hash = Universe.hash end) let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons diff --git a/kernel/univ.mli b/kernel/univ.mli index 7511769c4..64555fbb0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -20,6 +20,9 @@ sig val equal : t -> t -> bool (** Equality function *) + val hash : t -> int + (** Hash function *) + val make : Names.DirPath.t -> int -> t (** Create a new universe level from a unique identifier and an associated module path. *) @@ -41,6 +44,9 @@ sig val equal : t -> t -> bool (** Equality function *) + val hash : t -> int + (** Hash function *) + val make : UniverseLevel.t -> t (** Create a constraint-free universe out of a given level. *) diff --git a/lib/cString.ml b/lib/cString.ml index 823a35679..551b62834 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -46,6 +46,7 @@ module type ExtS = sig include S external equal : string -> string -> bool = "caml_string_equal" "noalloc" + val hash : string -> int val is_empty : string -> bool val explode : string -> string list val implode : string list -> string @@ -67,6 +68,16 @@ include String external equal : string -> string -> bool = "caml_string_equal" "noalloc" +let rec hash len s i accu = + if i = len then accu + else + let c = Char.code (String.unsafe_get s i) in + hash len s (succ i) (accu * 19 + c) + +let hash s = + let len = String.length s in + hash len s 0 0 + let explode s = let rec explode_rec n = if n >= String.length s then diff --git a/lib/cString.mli b/lib/cString.mli index 6ecbe888a..d8a19c8e4 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -52,6 +52,9 @@ sig external equal : string -> string -> bool = "caml_string_equal" "noalloc" (** Equality on strings *) + val hash : string -> int + (** Hashing on strings. Should be compatible with generic one. *) + val is_empty : string -> bool (** Test whether a string is empty. *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 33f2c578f..3a8a86e3e 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -117,9 +117,10 @@ let register_hcons h u = (* Basic hashcons modules for string and obj. Integers do not need be hashconsed. *) +module type HashedType = sig type t val hash : t -> int end + (* list *) -module type SomeData = sig type t end -module Hlist (D:SomeData) = +module Hlist (D:HashedType) = Make( struct type t = D.t list @@ -133,7 +134,12 @@ module Hlist (D:SomeData) = | [], [] -> true | x1::l1, x2::l2 -> x1==x2 && l1==l2 | _ -> false - let hash = Hashtbl.hash + let rec hash accu = function + | [] -> accu + | x :: l -> + let accu = Hashset.Combine.combine (D.hash x) accu in + hash accu l + let hash l = hash 0 l end) (* string *) @@ -143,7 +149,16 @@ module Hstring = Make( type u = unit let hashcons () s =(* incr accesstr;*) s external equal : string -> string -> bool = "caml_string_equal" "noalloc" - let hash = Hashtbl.hash + (** Copy from CString *) + let rec hash len s i accu = + if i = len then accu + else + let c = Char.code (String.unsafe_get s i) in + hash len s (succ i) (accu * 19 + c) + + let hash s = + let len = String.length s in + hash len s 0 0 end) (* Obj.t *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 255cb0430..cf3a09af4 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -83,12 +83,12 @@ val recursive2_hcons : (** {6 Hashconsing of usual structures} *) +module type HashedType = sig type t val hash : t -> int end + module Hstring : (S with type t = string and type u = unit) (** Hashconsing of strings. *) -module type SomeData = sig type t end - -module Hlist (D:SomeData) : +module Hlist (D:HashedType) : (S with type t = D.t list and type u = (D.t list -> D.t list)*(D.t->D.t)) (** Hashconsing of lists. *) diff --git a/lib/int.ml b/lib/int.ml index a85cf400d..6eb426065 100644 --- a/lib/int.ml +++ b/lib/int.ml @@ -12,7 +12,7 @@ external equal : int -> int -> bool = "%eq" external compare : int -> int -> int = "caml_int_compare" -let hash i = i land max_int +let hash i = i land 0x3FFFFFFF module Self = struct |