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

1 files changed, 35 insertions, 0 deletions

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)