diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /lib/cSet.ml | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'lib/cSet.ml')
-rw-r--r-- | lib/cSet.ml | 67 |
1 files changed, 67 insertions, 0 deletions
diff --git a/lib/cSet.ml b/lib/cSet.ml new file mode 100644 index 00000000..d7d5c70b --- /dev/null +++ b/lib/cSet.ml @@ -0,0 +1,67 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +module type OrderedType = +sig + type t + val compare : t -> t -> int +end + +module type S = Set.S + +module Make(M : OrderedType)= Set.Make(M) + +module type HashedType = +sig + type t + val hash : t -> int +end + +module Hashcons(M : OrderedType)(H : HashedType with type t = M.t) = +struct + module Set = Make(M) + + type set = Set.t + type _set = + | SEmpty + | SNode of set * M.t * set * int + + let set_prj : set -> _set = Obj.magic + let set_inj : _set -> set = Obj.magic + + let rec spine s accu = match set_prj s with + | SEmpty -> accu + | SNode (l, v, r, _) -> spine l ((v, r) :: accu) + + let rec umap f s = match set_prj s with + | SEmpty -> set_inj SEmpty + | SNode (l, v, r, h) -> + let l' = umap f l in + let r' = umap f r in + let v' = f v in + set_inj (SNode (l', v', r', h)) + + let rec eqeq s1 s2 = match s1, s2 with + | [], [] -> true + | (v1, r1) :: s1, (v2, r2) :: s2 -> + v1 == v2 && eqeq (spine r1 s1) (spine r2 s2) + | _ -> false + + module Hashed = + struct + open Hashset.Combine + type t = set + type u = M.t -> M.t + let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) + let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0 + let hashcons = umap + end + + include Hashcons.Make(Hashed) + +end |