diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cMap.ml | 60 | ||||
| -rw-r--r-- | lib/cMap.mli | 35 | ||||
| -rw-r--r-- | lib/cString.ml | 4 | ||||
| -rw-r--r-- | lib/cString.mli | 2 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 | ||||
| -rw-r--r-- | lib/int.ml | 2 | ||||
| -rw-r--r-- | lib/int.mli | 2 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 4 |
9 files changed, 109 insertions, 5 deletions
diff --git a/lib/cMap.ml b/lib/cMap.ml new file mode 100644 index 0000000000..bf0a337687 --- /dev/null +++ b/lib/cMap.ml @@ -0,0 +1,60 @@ +(************************************************************************) +(* 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 = Map.S + +module type ExtS = +sig + include Map.S + module Set : Set.S with type elt = key + val domain : 'a t -> Set.t +end + +module Domain (M : Map.OrderedType) : +sig + val domain : 'a Map.Make(M).t -> Set.Make(M).t +end = +struct + (** This unsafe module is a way to access to the actual implementations of + OCaml sets and maps without reimplementing them ourselves. It is quite + dubious that these implementations will ever be changed... Nonetheless, + if this happens, we can still implement a less clever version of [domain]. + *) + + type 'a map = 'a Map.Make(M).t + type set = Set.Make(M).t + + type 'a _map = + | MEmpty + | MNode of 'a map * M.t * 'a * 'a map * int + + type _set = + | SEmpty + | SNode of set * M.t * set * int + + let rec domain (s : 'a map) : set = match Obj.magic s with + | MEmpty -> Obj.magic SEmpty + | MNode (l, k, _, r, h) -> + Obj.magic (SNode (domain l, k, domain r, h)) + (** This function is essentially identity, but OCaml current stdlib does not + take advantage of the similarity of the two structures, so we introduce + this unsafe loophole. *) + +end + +module Make(M : Map.OrderedType) = +struct + include Map.Make(M) + include Domain(M) +end diff --git a/lib/cMap.mli b/lib/cMap.mli new file mode 100644 index 0000000000..9b7043d9ec --- /dev/null +++ b/lib/cMap.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** {5 Extended version of OCaml's maps} *) + +module type OrderedType = +sig + type t + val compare : t -> t -> int +end + +module type S = Map.S + +module type ExtS = +sig + include Map.S + (** The underlying Map library *) + + module Set : Set.S with type elt = key + (** Sets used by the domain function *) + + val domain : 'a t -> Set.t + (** Recover the set of keys defined in the map. *) + +end + +module Make(M : Map.OrderedType) : ExtS with + type key = M.t + and type 'a t = 'a Map.Make(M).t + and module Set := Set.Make(M) diff --git a/lib/cString.ml b/lib/cString.ml index 59a6d17c6e..1cb153b66b 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -59,7 +59,7 @@ sig val split : char -> string -> string list val is_sub : string -> string -> int -> bool module Set : Set.S with type elt = t - module Map : Map.S with type key = t + module Map : CMap.ExtS with type key = t and module Set := Set val hcons : string -> string end @@ -178,6 +178,6 @@ struct end module Set = Set.Make(Self) -module Map = Map.Make(Self) +module Map = CMap.Make(Self) let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate () diff --git a/lib/cString.mli b/lib/cString.mli index c9ff60f763..6ecbe888af 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -93,7 +93,7 @@ sig module Set : Set.S with type elt = t (** Finite sets on [string] *) - module Map : Map.S with type key = t + module Map : CMap.ExtS with type key = t and module Set := Set (** Finite maps on [string] *) val hcons : string -> string diff --git a/lib/clib.mllib b/lib/clib.mllib index f8e92f4afb..30821492ea 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,6 +1,7 @@ Coq_config Hook +CMap Int Option Store diff --git a/lib/int.ml b/lib/int.ml index 86d79fd311..a85cf400d6 100644 --- a/lib/int.ml +++ b/lib/int.ml @@ -21,4 +21,4 @@ struct end module Set = Set.Make(Self) -module Map = Map.Make(Self) +module Map = CMap.Make(Self) diff --git a/lib/int.mli b/lib/int.mli index cde422a849..956432a526 100644 --- a/lib/int.mli +++ b/lib/int.mli @@ -17,4 +17,4 @@ external compare : t -> t -> int = "caml_int_compare" val hash : t -> int module Set : Set.S with type elt = t -module Map : Map.S with type key = t +module Map : CMap.ExtS with type key = t and module Set := Set diff --git a/lib/util.ml b/lib/util.ml index fb968cc64f..35220261cc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -71,6 +71,10 @@ let (@) = CList.append module Array : CArray.ExtS = CArray +(* Maps *) + +module Map = CMap + (* Matrices *) let matrix_transpose mat = diff --git a/lib/util.mli b/lib/util.mli index 209f64c2f6..34aa0e1aba 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -60,6 +60,10 @@ val (@) : 'a list -> 'a list -> 'a list module Array : CArray.ExtS +(** {6 Maps. } *) + +module Map : module type of CMap + (** {6 Streams. } *) val stream_nth : int -> 'a Stream.t -> 'a |