diff options
Diffstat (limited to 'src/lfsc/shashcons.ml')
-rw-r--r-- | src/lfsc/shashcons.ml | 84 |
1 files changed, 84 insertions, 0 deletions
diff --git a/src/lfsc/shashcons.ml b/src/lfsc/shashcons.ml new file mode 100644 index 0000000..a3d0f0c --- /dev/null +++ b/src/lfsc/shashcons.ml @@ -0,0 +1,84 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2019 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +(*s Hash tables for hash-consing. (Some code is borrowed from the ocaml + standard library, which is copyright 1996 INRIA.) *) + +module type HashedType = + sig + type t + val equal : t -> t -> bool + val hash : t -> int + val tag : int -> t -> t + end + +module type S = + sig + type t + val hashcons : t -> t + val iter : (t -> unit) -> unit + val stats : unit -> int * int * int * int * int * int + end + +module Make(H : HashedType) : (S with type t = H.t) = +struct + type t = H.t + + module WH = Weak.Make (H) + + let next_tag = ref 0 + + let htable = WH.create 5003 + + let hashcons d = + let d = H.tag !next_tag d in + let o = WH.merge htable d in + if o == d then incr next_tag; + o + + let iter f = WH.iter f htable + + let stats () = WH.stats htable +end + + +type 'a hash_consed = { + tag : int; + node : 'a } + +module type HashedType_consed = + sig + type t + val equal : t -> t -> bool + val hash : t -> int + end + +module type S_consed = + sig + type key + val hashcons : key -> key hash_consed + val iter : (key hash_consed -> unit) -> unit + val stats : unit -> int * int * int * int * int * int + end + +module Make_consed(H : HashedType_consed) : (S_consed with type key = H.t) = +struct + module M = Make(struct + type t = H.t hash_consed + let hash x = H.hash x.node + let equal x y = H.equal x.node y.node + let tag i x = {x with tag = i} + end) + include M + type key = H.t + let hashcons x = M.hashcons {tag = -1; node = x} +end |