Added an update function in CMap. It has the same signature as Map.add, but

expects the given key to be present, and thus is faster.

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

2 files changed, 22 insertions, 4 deletions

diff --git a/lib/cMap.ml b/lib/cMap.ml
index d5aa8c46be..952ec21c69 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -18,6 +18,7 @@ module type ExtS =
 sig
   include Map.S
   module Set : Set.S with type elt = key
+  val update : key -> 'a -> 'a t -> 'a t
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   val domain : 'a t -> Set.t
   val bind : (key -> 'a) -> Set.t -> 'a t
@@ -25,9 +26,11 @@ end
 
 module MapExt (M : Map.OrderedType) :
 sig
-  val modify : M.t -> (M.t -> 'a -> 'a) -> 'a Map.Make(M).t -> 'a Map.Make(M).t
-  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
+  type 'a map = 'a Map.Make(M).t
+  val update : M.t -> 'a -> 'a map -> 'a map
+  val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  val domain : 'a map -> Set.Make(M).t
+  val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map
 end =
 struct
   (** This unsafe module is a way to access to the actual implementations of
@@ -52,6 +55,17 @@ struct
   let set_prj : set -> _set = Obj.magic
   let set_inj : _set -> set = Obj.magic
 
+  let rec update k v (s : 'a map) : 'a map = match map_prj s with
+  | MEmpty -> raise Not_found
+  | MNode (l, k', v', r, h) ->
+    let c = M.compare k k' in
+    if c < 0 then
+      map_inj (MNode (update k v l, k', v', r, h))
+    else if c = 0 then
+      map_inj (MNode (l, k', v, r, h))
+    else
+      map_inj (MNode (l, k', v', update k v r, h))
+
   let rec modify k f (s : 'a map) : 'a map = match map_prj s with
   | MEmpty -> raise Not_found
   | MNode (l, k', v, r, h) ->
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 8865c1eefd..6e5f3bcfdd 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -24,9 +24,13 @@ sig
   module Set : Set.S with type elt = key
   (** Sets used by the domain function *)
 
+  val update : key -> 'a -> 'a t -> 'a t
+  (** Same as [add], but expects the key to be present, and thus faster.
+      @raise Not_found when the key is unbound in the map. *)
+
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   (** Apply the given function to the binding of the given key.
-      @raise [Not_found] when the key is unbound in the map. *)
+      @raise Not_found when the key is unbound in the map. *)
 
   val domain : 'a t -> Set.t
   (** Recover the set of keys defined in the map. *)