Added a more efficient way to recover the domain of a map.

The extended signature is defined in CMap, and should be compatible
with the old one, except that module arguments have to be explicitely
named. The implementation itself is quite unsafe, as it relies on the
current implementation of OCaml maps, even though that should not be
a problem (it has not changed in ages).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7

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