aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-12-17 18:36:24 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-12-17 18:37:45 +0100
commite4ac6f91e8d95a168cdaeaec72cf761b7b6da4b7 (patch)
tree62c804059699ff38055c4e93b9d53dfafebe8273
parent00f82e4411ebbab16fcab99e6c563852a87507a3 (diff)
Fix (actually, properly implement :) hashconsing of projections,
resulting in huge speedup at Qed/section closing in presence of primitive projections.
-rw-r--r--kernel/constr.ml2
-rw-r--r--kernel/names.ml19
-rw-r--r--kernel/names.mli3
3 files changed, 19 insertions, 5 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 0fd4c9d57..e757c5b56 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -821,7 +821,7 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
| Proj (p,c) ->
let c, hc = sh_rec c in
- let p' = Projection.hashcons p in
+ let p' = Projection.hcons p in
(Proj (p', c), combinesmall 17 (combine (Projection.hash p') hc))
| Const (c,u) ->
let c' = sh_con c in
diff --git a/kernel/names.ml b/kernel/names.ml
index 5d73bd520..13ea9e1d8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -794,10 +794,23 @@ struct
let unfolded = snd
let unfold (c, b as p) = if b then p else (c, true)
let equal (c, b) (c', b') = Constant.equal c c' && b == b'
+
let hash (c, b) = (if b then 0 else 1) + Constant.hash c
- let hashcons (c, b as x) =
- let c' = hcons_con c in
- if c' == c then x else (c', b)
+
+ module Self_Hashcons =
+ struct
+ type _t = t
+ type t = _t
+ type u = Constant.t -> Constant.t
+ let hashcons hc (c,b) = (hc c,b)
+ let equal ((c,b) as x) ((c',b') as y) =
+ x == y || (c == c' && b == b')
+ let hash = hash
+ end
+
+ module HashProjection = Hashcons.Make(Self_Hashcons)
+
+ let hcons = Hashcons.simple_hcons HashProjection.generate hcons_con
let compare (c, b) (c', b') =
if b == b' then Constant.CanOrd.compare c c'
diff --git a/kernel/names.mli b/kernel/names.mli
index 893cad09d..c71b76aab 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -645,7 +645,8 @@ module Projection : sig
val equal : t -> t -> bool
val hash : t -> int
- val hashcons : t -> t
+ val hcons : t -> t
+ (** Hashconsing of projections. *)
val compare : t -> t -> int