diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-25 22:34:08 +0000 |
commit | f4a6a6aaa928e7a6c8d360c45268cb82c020c2dc (patch) | |
tree | 95bf369c1f34a6a4c055357b68e60de58849bd11 /kernel | |
parent | 646c6765e5e3307f8898c4f63c405d91c2e6f47b (diff) |
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
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/names.ml | 22 | ||||
-rw-r--r-- | kernel/names.mli | 30 |
2 files changed, 21 insertions, 31 deletions
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} *) |