diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-10 19:50:19 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-11 16:20:04 +0100 |
commit | e8af74ad7913773c4dfb688167b15b6e15e4397a (patch) | |
tree | 4c4fe4a14682e652158a217b23f3f7e30087aa47 /kernel | |
parent | 2c449165e42f59fa6dfa8186bfca8c371de4c51a (diff) |
Clarifying the implementation of universe hashconsing.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/univ.ml | 33 |
1 files changed, 16 insertions, 17 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 492762df3..ea5727620 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -233,27 +233,26 @@ module Level = struct let hash x = x.hash - let hcons x = - let data' = RawLevel.hcons x.data in - if data' == x.data then x - else { x with data = data' } - let data x = x.data (** Hashcons on levels + their hash *) - let make = - let module Self = struct - type _t = t - type t = _t - let equal = equal - let hash = hash - end in - let module WH = Weak.Make(Self) in - let pool = WH.create 4910 in fun x -> - let x = { hash = RawLevel.hash x; data = x } in - try WH.find pool x - with Not_found -> WH.add pool x; x + module Self = struct + type _t = t + type t = _t + type u = raw_level -> raw_level + let equal x y = x.hash == y.hash && x.data == y.data + let hash x = x.hash + let hashcons hraw x = + let data' = hraw x.data in + if x.data == data' then x else { x with data = data' } + end + + let hcons = + let module H = Hashcons.Make(Self) in + Hashcons.simple_hcons H.generate H.hcons RawLevel.hcons + + let make l = hcons { hash = RawLevel.hash l; data = l } let set = make Set let prop = make Prop |