aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/constr.ml63
-rw-r--r--kernel/names.ml19
-rw-r--r--kernel/sorts.ml11
-rw-r--r--lib/hashcons.ml19
-rw-r--r--lib/hashcons.mli6
5 files changed, 67 insertions, 51 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index d09222ead..eba490dbd 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -492,30 +492,25 @@ let hasheq 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 HashsetTerm = Hashset.Make(struct type t = constr let equal = hasheq end)
+module HashsetTerm =
+ Hashset.Make(struct type t = constr let equal = hasheq end)
+
+module HashsetTermArray =
+ Hashset.Make(struct type t = constr array let equal = array_eqeq end)
let term_table = HashsetTerm.create 19991
(* The associative table to hashcons terms. *)
+let term_array_table = HashsetTermArray.create 4999
+(* The associative table to hashcons term arrays. *)
+
open Hashset.Combine
(* [hashcons hash_consing_functions constr] computes an hash-consed
representation for [constr] using [hash_consing_functions] on
leaves. *)
let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
-
- (* Note : we hash-cons constr arrays *in place* *)
-
- let rec 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
- accu := combine !accu h;
- t.(i) <- x
- done;
- !accu
-
- and hash_term t =
+ let rec hash_term t =
match t with
| Var i ->
(Var (sh_id i), combinesmall 1 (Hashtbl.hash i))
@@ -540,12 +535,11 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
(LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (Hashtbl.hash na) hb ht hc))
| App (c,l) ->
let c, hc = sh_rec c in
- let hl = hash_term_array l in
- (App (c, l), combinesmall 7 (combine hl hc))
+ let l, hl = hash_term_array l in
+ (App (c,l), combinesmall 7 (combine hl hc))
| Evar (e,l) ->
- let hl = hash_term_array l in
- (* since the array have been hashed in place : *)
- (t, combinesmall 8 (combine (Hashtbl.hash e) hl))
+ let l, hl = hash_term_array l in
+ (Evar (e,l), combinesmall 8 (combine (Hashtbl.hash e) hl))
| Const c ->
(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
| Ind ((kn,i) as ind) ->
@@ -555,21 +549,21 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
| Case (ci,p,c,bl) ->
let p, hp = sh_rec p
and c, hc = sh_rec c in
- let hbl = hash_term_array bl in
+ let bl,hbl = hash_term_array bl in
let hbl = combine (combine hc hp) hbl in
(Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
| Fix (ln,(lna,tl,bl)) ->
- let hbl = hash_term_array bl in
- let htl = hash_term_array tl in
+ 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;
- (* since the three arrays have been hashed in place : *)
- (t, combinesmall 13 (combine (Hashtbl.hash lna) (combine hbl htl)))
+ let h = combine3 (Hashtbl.hash lna) hbl htl in
+ (Fix (ln,(lna,tl,bl)), combinesmall 13 h)
| CoFix(ln,(lna,tl,bl)) ->
- let hbl = hash_term_array bl in
- let htl = hash_term_array tl in
+ 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;
- (* since the three arrays have been hashed in place : *)
- (t, combinesmall 14 (combine (Hashtbl.hash lna) (combine hbl htl)))
+ let h = combine3 (Hashtbl.hash lna) hbl htl in
+ (CoFix (ln,(lna,tl,bl)), combinesmall 14 h)
| Meta n ->
(t, combinesmall 15 n)
| Rel n ->
@@ -581,6 +575,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
let h = h land 0x3FFFFFFF in
(HashsetTerm.repr h y term_table, h)
+ (* Note : During hash-cons of arrays, we modify them *in place* *)
+
+ 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
+ accu := combine !accu h;
+ t.(i) <- x
+ done;
+ (* [h] must be positive. *)
+ let h = !accu land 0x3FFFFFFF in
+ (HashsetTermArray.repr h t term_array_table, h)
+
in
(* Make sure our statically allocated Rels (1 to 16) are considered
as canonical, and hence hash-consed to themselves *)
diff --git a/kernel/names.ml b/kernel/names.ml
index 0da8fc5d4..9124b4689 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -156,24 +156,9 @@ struct
let initial = [default_module_name]
- module Self_Hashcons =
- struct
- type t_ = t
- type t = t_
- type u = Id.t -> Id.t
- let hashcons hident d = List.smartmap hident d
- let rec equal d1 d2 =
- d1 == d2 ||
- match (d1, d2) with
- | [], [] -> true
- | id1 :: d1, id2 :: d2 -> id1 == id2 && equal d1 d2
- | _ -> false
- let hash = Hashtbl.hash
- end
-
- module Hdir = Hashcons.Make(Self_Hashcons)
+ module Hdir = Hashcons.Hlist(Id)
- let hcons = Hashcons.simple_hcons Hdir.generate Id.hcons
+ let hcons = Hashcons.recursive_hcons Hdir.generate Id.hcons
end
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index 7ab6b553a..88c99683e 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -51,13 +51,12 @@ module Hsorts =
type t = _t
type u = universe -> universe
let hashcons huniv = function
- Prop c -> Prop c
| Type u -> Type (huniv u)
- let equal s1 s2 =
- match (s1,s2) with
- (Prop c1, Prop c2) -> c1 == c2
- | (Type u1, Type u2) -> u1 == u2
- |_ -> false
+ | s -> s
+ let equal s1 s2 = match (s1,s2) with
+ | (Prop c1, Prop c2) -> c1 == c2
+ | (Type u1, Type u2) -> u1 == u2
+ |_ -> false
let hash = Hashtbl.hash
end)
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index db502c90c..b33a20058 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -126,6 +126,25 @@ let register_hcons h u =
(* Basic hashcons modules for string and obj. Integers do not need be
hashconsed. *)
+(* list *)
+module type SomeData = sig type t end
+module Hlist (D:SomeData) =
+ Make(
+ struct
+ type t = D.t list
+ type u = (t -> t) * (D.t -> D.t)
+ let hashcons (hrec,hdata) = function
+ | x :: l -> hdata x :: hrec l
+ | l -> l
+ let equal l1 l2 =
+ l1 == l2 ||
+ match l1, l2 with
+ | [], [] -> true
+ | x1::l1, x2::l2 -> x1==x2 && l1==l2
+ | _ -> false
+ let hash = Hashtbl.hash
+ end)
+
(* string *)
module Hstring = Make(
struct
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 2f86174b2..ae7d6b9d9 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -91,5 +91,11 @@ val recursive2_hcons :
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) :
+ (S with type t = D.t list and type u = (D.t list -> D.t list)*(D.t->D.t))
+(** Hashconsing of lists. *)
+
module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit)
(** Hashconsing of OCaml values. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 17:58:29 +0000