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

25 files changed, 176 insertions, 56 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 2b66edcb1..31d2e005f 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,6 +1,7 @@
 Coq_config
 
 Hook
+CMap
 Int
 Option
 Store
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2c97f68df..090536cc3 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -1,6 +1,7 @@
 Coq_config
 
 Hook
+CMap
 Int
 Option
 Store
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index bde5c15f3..b1eb01f4f 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -1,6 +1,7 @@
 Coq_config
 
 Hook
+CMap
 Int
 Option
 Store
diff --git a/kernel/names.ml b/kernel/names.ml
index 9124b4689..2a04ff3c5 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -58,15 +58,7 @@ struct
   end
 
   module Set = Set.Make(Self)
-  module Map =
-  struct
-    include Map.Make(Self)
-    exception Finded
-    let exists f m =
-      try iter (fun a b -> if f a b then raise Finded) m ; false
-      with Finded -> true
-    let singleton k v = add k v empty
-  end
+  module Map = CMap.Make(Self)
 
   module Pred = Predicate.Make(Self)
 
@@ -218,7 +210,7 @@ struct
 
 end
 
-module MBImap = Map.Make(MBId)
+module MBImap = CMap.Make(MBId)
 module MBIset = Set.Make(MBId)
 
 (** {6 Names of structure elements } *)
@@ -298,7 +290,7 @@ module ModPath = struct
 end
 
 module MPset = Set.Make(ModPath)
-module MPmap = Map.Make(ModPath)
+module MPmap = CMap.Make(ModPath)
 
 (** {6 Kernel names } *)
 
@@ -357,7 +349,7 @@ module KerName = struct
 
 end
 
-module KNmap = Map.Make(KerName)
+module KNmap = CMap.Make(KerName)
 module KNpred = Predicate.Make(KerName)
 module KNset = Set.Make(KerName)
 
@@ -467,8 +459,8 @@ end
 
 module Constant = KerPair
 
-module Cmap = Map.Make(Constant.CanOrd)
-module Cmap_env = Map.Make(Constant.UserOrd)
+module Cmap = CMap.Make(Constant.CanOrd)
+module Cmap_env = CMap.Make(Constant.UserOrd)
 module Cpred = Predicate.Make(Constant.CanOrd)
 module Cset = Set.Make(Constant.CanOrd)
 module Cset_env = Set.Make(Constant.UserOrd)
@@ -477,7 +469,7 @@ module Cset_env = Set.Make(Constant.UserOrd)
 
 module MutInd = KerPair
 
-module Mindmap = Map.Make(MutInd.CanOrd)
+module Mindmap = CMap.Make(MutInd.CanOrd)
 module Mindset = Set.Make(MutInd.CanOrd)
 module Mindmap_env = Map.Make(MutInd.UserOrd)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index c05e30b9b..82df07562 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+
 (** {6 Identifiers } *)
 
 module Id :
@@ -35,7 +37,7 @@ sig
   module Set : Set.S with type elt = t
   (** Finite sets of identifiers. *)
 
-  module Map : Map.S with type key = t
+  module Map : Map.ExtS with type key = t and module Set := Set
   (** Finite maps of identifiers. *)
 
   module Pred : Predicate.S with type elt = t
@@ -133,7 +135,7 @@ sig
   (** Pretty-printer. *)
 
   module Set : Set.S with type elt = t
-  module Map : Map.S with type key = t
+  module Map : Map.ExtS with type key = t and module Set := Set
 
 end
 
@@ -170,7 +172,7 @@ sig
 end
 
 module MBIset : Set.S with type elt = MBId.t
-module MBImap : Map.S with type key = MBId.t
+module MBImap : Map.ExtS with type key = MBId.t and module Set := MBIset
 
 (** {6 The module part of the kernel name } *)
 
@@ -194,7 +196,7 @@ sig
 end
 
 module MPset : Set.S with type elt = ModPath.t
-module MPmap : Map.S with type key = ModPath.t
+module MPmap : Map.ExtS with type key = ModPath.t and module Set := MPset
 
 (** {6 The absolute names of objects seen by kernel } *)
 
@@ -222,7 +224,7 @@ end
 
 module KNset  : Set.S with type elt = KerName.t
 module KNpred : Predicate.S with type elt = KerName.t
-module KNmap  : Map.S with type key = KerName.t
+module KNmap  : Map.ExtS with type key = KerName.t and module Set := KNset
 
 
 (** {6 Constant Names } *)
@@ -288,11 +290,11 @@ end
 
 (** The [*_env] modules consider an order on user part of names
    the others consider an order on canonical part of names*)
-module Cmap  : Map.S with type key = Constant.t
-module Cmap_env  : Map.S with type key = Constant.t
-module Cpred  : Predicate.S with type elt = Constant.t
-module Cset  : Set.S with type elt = Constant.t
+module Cpred : Predicate.S with type elt = Constant.t
+module Cset : Set.S with type elt = Constant.t
 module Cset_env  : Set.S with type elt = Constant.t
+module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset
+module Cmap_env : Map.ExtS with type key = Constant.t  and module Set := Cset_env
 
 (** {6 Inductive names} *)
 
@@ -352,9 +354,9 @@ sig
 
 end
 
-module Mindmap : Map.S with type key = MutInd.t
-module Mindmap_env : Map.S with type key = MutInd.t
 module Mindset : Set.S with type elt = MutInd.t
+module Mindmap : Map.ExtS with type key = MutInd.t and module Set := Mindset
+module Mindmap_env : Map.S with type key = MutInd.t
 
 (** Beware: first inductive has index 0 *)
 type inductive = MutInd.t * int
@@ -448,11 +450,7 @@ module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
 module Idpred : Predicate.S with type elt = identifier and type t = Id.Pred.t
 (** @deprecated Same as [Id.Pred]. *)
 
-module Idmap  : sig
-  include Map.S with type key = identifier
-  val exists : (identifier -> 'a -> bool) -> 'a t -> bool
-  val singleton : key -> 'a -> 'a t
-end
+module Idmap : module type of Id.Map
 (** @deprecated Same as [Id.Map]. *)
 
 (** {5 Directory paths} *)
diff --git a/lib/cMap.ml b/lib/cMap.ml
new file mode 100644
index 000000000..bf0a33768
--- /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 000000000..9b7043d9e
--- /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 59a6d17c6..1cb153b66 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 c9ff60f76..6ecbe888a 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 f8e92f4af..30821492e 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 86d79fd31..a85cf400d 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 cde422a84..956432a52 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 fb968cc64..35220261c 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 209f64c2f..34aa0e1ab 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
diff --git a/library/assumptions.mli b/library/assumptions.mli
index f91412013..cd08caf73 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Names
 open Term
 open Environ
@@ -19,8 +20,9 @@ type context_object =
   | Transparent of constant (** A transparent constant *)
 
 (** AssumptionSet.t is a set of [assumption] *)
-module OrderedContextObject :  Set.OrderedType with type t = context_object
-module ContextObjectMap : Map.S with type key = context_object
+module ContextObjectSet : Set.S with type elt = context_object
+module ContextObjectMap : Map.ExtS
+  with type key = context_object and module Set := ContextObjectSet
 
 (** collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type) *)
diff --git a/library/globnames.ml b/library/globnames.ml
index a04cdea8c..e80197030 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Errors
 open Names
 open Term
diff --git a/library/globnames.mli b/library/globnames.mli
index 74da2cca8..4bf21cf0a 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Names
 open Term
@@ -57,10 +58,12 @@ module RefOrdered_env : sig
 end
 
 module Refset : Set.S with type elt = global_reference
-module Refmap : Map.S with type key = global_reference
+module Refmap : Map.ExtS
+  with type key = global_reference and module Set := Refset
 
 module Refset_env : Set.S with type elt = global_reference
-module Refmap_env : Map.S with type key = global_reference
+module Refmap_env : Map.ExtS
+  with type key = global_reference and module Set := Refset_env
 
 (** {6 Extended global references } *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 80539a156..4151e6774 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -192,8 +192,13 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-module OptionMap =
-  Map.Make (struct  type t = option_name let compare = compare end)
+module OptionOrd =
+struct
+  type t = option_name
+  let compare = compare
+end
+
+module OptionMap = Map.Make(OptionOrd)
 
 let value_tab = ref OptionMap.empty
 
diff --git a/library/libnames.mli b/library/libnames.mli
index 627b8f013..60ec7af79 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Pp
 open Loc
 open Names
@@ -37,7 +38,7 @@ val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t
 val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
 
 module Dirset : Set.S with type elt = DirPath.t
-module Dirmap : Map.S with type key = DirPath.t
+module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
 
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 81cfd3f1d..680139b12 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -14,7 +14,8 @@ open Tok
 (* Dictionaries: trees annotated with string options, each node being a map
    from chars to dictionaries (the subtrees). A trie, in other words. *)
 
-module CharMap = Map.Make (struct type t = char let compare = compare end)
+module CharOrd = struct type t = char let compare : char -> char -> int = compare end
+module CharMap = Map.Make (CharOrd)
 
 type ttree = {
   node : string option;
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index fbe31fe52..11786cbdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -83,13 +83,20 @@ type pa_mark=
     Fmark of pa_fun
   | Cmark of pa_constructor
 
-module PacMap=Map.Make(struct
-			 type t=pa_constructor
-			 let compare=Pervasives.compare end)
+module PacOrd =
+struct
+  type t = pa_constructor
+  let compare = Pervasives.compare (** FIXME *)
+end
+
+module PafOrd =
+struct
+  type t = pa_fun
+  let compare = Pervasives.compare (** FIXME *)
+end
 
-module PafMap=Map.Make(struct
-			 type t=pa_fun
-			 let compare=Pervasives.compare end)
+module PacMap=Map.Make(PacOrd)
+module PafMap=Map.Make(PafOrd)
 
 type cinfo=
     {ci_constr: constructor; (* inductive type *)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1b9afb7c7..75005f1c8 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -62,7 +62,8 @@ type form=
   | Conjunct of form * form
   | Disjunct of form * form
 
-module Fmap=Map.Make(struct type t=form let compare=compare end)
+module FOrd = struct type t = form let compare = Pervasives.compare (** FIXME *) end
+module Fmap = Map.Make(FOrd)
 
 type sequent =
     {rev_hyps: form Int.Map.t;
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index f618c54b0..9614d74e2 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -332,7 +332,7 @@ type ring_info =
       ring_pre_tac : glob_tactic_expr;
       ring_post_tac : glob_tactic_expr }
 
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
+module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
 let from_relation = Summary.ref Cmap.empty ~name:"ring-tac-rel-table"
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index e67b1f81b..59e176543 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open Loc
 open Pp
 open Names
@@ -19,9 +20,8 @@ open Termops
 (********************************************************************
    Meta map *)
 
-module Metamap : Map.S with type key = metavariable
-
 module Metaset : Set.S with type elt = metavariable
+module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset
 
 type 'a freelisted = {
   rebus : 'a;
@@ -187,8 +187,10 @@ type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * env * constr * constr
 val add_conv_pb :  evar_constraint -> evar_map -> evar_map
 
-module ExistentialMap : Map.S with type key = existential_key
 module ExistentialSet : Set.S with type elt = existential_key
+module ExistentialMap : Map.ExtS
+  with type key = existential_key and module Set := ExistentialSet
+
 val extract_changed_conv_pbs : evar_map ->
       (ExistentialSet.t -> evar_constraint -> bool) ->
       evar_map * evar_constraint list
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index ed315bcf5..d8f08cafd 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -440,7 +440,7 @@ let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
-module ProgMap = Map.Make(struct type t = Id.t let compare = Id.compare end)
+module ProgMap = Map.Make(Id)
 
 let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)