aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.mllib1
-rw-r--r--dev/printers.mllib1
-rw-r--r--grammar/grammar.mllib1
-rw-r--r--kernel/names.ml22
-rw-r--r--kernel/names.mli30
-rw-r--r--lib/cMap.ml60
-rw-r--r--lib/cMap.mli35
-rw-r--r--lib/cString.ml4
-rw-r--r--lib/cString.mli2
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/int.ml2
-rw-r--r--lib/int.mli2
-rw-r--r--lib/util.ml4
-rw-r--r--lib/util.mli4
-rw-r--r--library/assumptions.mli6
-rw-r--r--library/globnames.ml1
-rw-r--r--library/globnames.mli7
-rw-r--r--library/goptions.ml9
-rw-r--r--library/libnames.mli3
-rw-r--r--parsing/lexer.ml43
-rw-r--r--plugins/cc/ccalgo.ml19
-rw-r--r--plugins/rtauto/proof_search.ml3
-rw-r--r--plugins/setoid_ring/newring.ml42
-rw-r--r--pretyping/evd.mli8
-rw-r--r--toplevel/obligations.ml2
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)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:14:13 +0000