diff options
| -rw-r--r-- | checker/check.mllib | 5 | ||||
| -rw-r--r-- | dev/printers.mllib | 5 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 5 | ||||
| -rw-r--r-- | lib/cSet.ml | 67 | ||||
| -rw-r--r-- | lib/cSet.mli | 31 | ||||
| -rw-r--r-- | lib/clib.mllib | 5 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 4 |
8 files changed, 118 insertions, 8 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 08196d27f..1999317cd 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,6 +1,9 @@ Coq_config Hook +Hashset +Hashcons +CSet CMap Int Option @@ -15,8 +18,6 @@ Segmenttree Unicodetable Unicode Errors -Hashset -Hashcons CObj CList CString diff --git a/dev/printers.mllib b/dev/printers.mllib index 30ac772d0..d9610fd25 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,6 +1,9 @@ Coq_config Hook +Hashset +Hashcons +CSet CMap Int Option @@ -17,8 +20,6 @@ Segmenttree Unicodetable Unicode Errors -Hashset -Hashcons CObj CList CString diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 3f5fc5e86..fd1d0e47e 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,9 @@ Coq_config Hook +Hashset +Hashcons +CSet CMap Int Option @@ -12,8 +15,6 @@ Flags Pp Loc Errors -Hashset -Hashcons CList CString CArray diff --git a/lib/cSet.ml b/lib/cSet.ml new file mode 100644 index 000000000..2a22ab6d3 --- /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-2012 *) +(* \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 diff --git a/lib/cSet.mli b/lib/cSet.mli new file mode 100644 index 000000000..77381d0a8 --- /dev/null +++ b/lib/cSet.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \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) : S + with type elt = M.t + and type t = Set.Make(M).t + +module type HashedType = +sig + type t + val hash : t -> int +end + +module Hashcons (M : OrderedType) (H : HashedType with type t = M.t) : Hashcons.S with + type t = Set.Make(M).t + and type u = M.t -> M.t +(** Create hash-consing for sets. The hashing function provided must be + compatible with the comparison function. *) diff --git a/lib/clib.mllib b/lib/clib.mllib index d6d017c72..6164212e1 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,6 +1,9 @@ Coq_config Hook +Hashset +Hashcons +CSet CMap Int Option @@ -13,8 +16,6 @@ Pp_control Flags Pp Deque -Hashset -Hashcons CObj CList CString diff --git a/lib/util.ml b/lib/util.ml index a5ed584cd..c293e4dfd 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -65,6 +65,10 @@ let (@) = CList.append module Array : CArray.ExtS = CArray +(* Sets *) + +module Set = CSet + (* Maps *) module Map = CMap diff --git a/lib/util.mli b/lib/util.mli index 62db3225e..c9456802d 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -59,6 +59,10 @@ val (@) : 'a list -> 'a list -> 'a list module Array : CArray.ExtS +(** {6 Sets. } *) + +module Set : module type of CSet + (** {6 Maps. } *) module Map : module type of CMap |