Removing association lists in Reductionops. Btw, defining the dual of the

domain operation on maps. The efficiency should just be improved.

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

2 files changed, 15 insertions, 3 deletions

diff --git a/lib/cMap.ml b/lib/cMap.ml
index bf0a337687..4c94f122ab 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -19,11 +19,13 @@ sig
   include Map.S
   module Set : Set.S with type elt = key
   val domain : 'a t -> Set.t
+  val bind : (key -> 'a) -> Set.t -> 'a t
 end
 
-module Domain (M : Map.OrderedType) :
+module MapExt (M : Map.OrderedType) :
 sig
   val domain : 'a Map.Make(M).t -> Set.Make(M).t
+  val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a Map.Make(M).t
 end =
 struct
   (** This unsafe module is a way to access to the actual implementations of
@@ -50,11 +52,17 @@ struct
   (** 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. *)
- 
+
+  let rec bind f (s : set) : 'a map = match Obj.magic s with
+  | SEmpty -> Obj.magic MEmpty
+  | SNode (l, k, r, h) ->
+    Obj.magic (MNode (bind f l, k, f k, bind f r, h))
+  (** Dual operation of [domain]. *)
+
 end
 
 module Make(M : Map.OrderedType) =
 struct
   include Map.Make(M)
-  include Domain(M)
+  include MapExt(M)
 end
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 9b7043d9ec..222138828e 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -27,6 +27,10 @@ sig
   val domain : 'a t -> Set.t
   (** Recover the set of keys defined in the map. *)
 
+  val bind : (key -> 'a) -> Set.t -> 'a t
+  (** [bind f s] transform the set [x1; ...; xn] into [x1 := f x1; ...;
+      xn := f xn]. *)
+
 end
 
 module Make(M : Map.OrderedType) : ExtS with