Collecting Map.smart_* functions into a module Map.Smart.

5 files changed, 72 insertions, 33 deletions

diff --git a/clib/cMap.ml b/clib/cMap.ml
index 373e3f8fd..f6e52594b 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -35,8 +35,15 @@ sig
   val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
   val height : 'a t -> int
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a t -> 'a t
+    val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+  end
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -59,8 +66,15 @@ sig
   val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
   val smartmap : ('a -> 'a) -> 'a map -> 'a map
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
   val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
   val height : 'a map -> int
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a map -> 'a map
+    val mapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+  end
   module Unsafe :
   sig
     val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
@@ -154,28 +168,36 @@ struct
     let accu = f k v (fold_right f r accu) in
     fold_right f l accu
 
-  let rec smartmap f (s : 'a map) = match map_prj s with
-  | MEmpty -> map_inj MEmpty
-  | MNode (l, k, v, r, h) ->
-    let l' = smartmap f l in
-    let r' = smartmap f r in
-    let v' = f v in
-    if l == l' && r == r' && v == v' then s
-    else map_inj (MNode (l', k, v', r', h))
-
-  let rec smartmapi f (s : 'a map) = match map_prj s with
-  | MEmpty -> map_inj MEmpty
-  | MNode (l, k, v, r, h) ->
-    let l' = smartmapi f l in
-    let r' = smartmapi f r in
-    let v' = f k v in
-    if l == l' && r == r' && v == v' then s
-    else map_inj (MNode (l', k, v', r', h))
-
   let height s = match map_prj s with
   | MEmpty -> 0
   | MNode (_, _, _, _, h) -> h
 
+  module Smart =
+  struct
+
+    let rec map f (s : 'a map) = match map_prj s with
+    | MEmpty -> map_inj MEmpty
+    | MNode (l, k, v, r, h) ->
+      let l' = map f l in
+      let r' = map f r in
+      let v' = f v in
+      if l == l' && r == r' && v == v' then s
+      else map_inj (MNode (l', k, v', r', h))
+
+    let rec mapi f (s : 'a map) = match map_prj s with
+    | MEmpty -> map_inj MEmpty
+    | MNode (l, k, v, r, h) ->
+      let l' = mapi f l in
+      let r' = mapi f r in
+      let v' = f k v in
+      if l == l' && r == r' && v == v' then s
+      else map_inj (MNode (l', k, v', r', h))
+
+  end
+
+  let smartmap = Smart.map
+  let smartmapi = Smart.mapi
+
   module Unsafe =
   struct
 
diff --git a/clib/cMap.mli b/clib/cMap.mli
index bb0019bb8..b45effb95 100644
--- a/clib/cMap.mli
+++ b/clib/cMap.mli
@@ -58,14 +58,23 @@ sig
   (** Folding keys in decreasing order. *)
 
   val smartmap : ('a -> 'a) -> 'a t -> 'a t
-  (** As [map] but tries to preserve sharing. *)
+  (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
 
   val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
-  (** As [mapi] but tries to preserve sharing. *)
+  (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
 
   val height : 'a t -> int
   (** An indication of the logarithmic size of a map *)
 
+  module Smart :
+  sig
+    val map : ('a -> 'a) -> 'a t -> 'a t
+    (** As [map] but tries to preserve sharing. *)
+
+    val mapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+    (** As [mapi] but tries to preserve sharing. *)
+  end
+
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
diff --git a/clib/hMap.ml b/clib/hMap.ml
index 37f867c6b..b2cf47430 100644
--- a/clib/hMap.ml
+++ b/clib/hMap.ml
@@ -383,13 +383,21 @@ struct
     let m = Map.set k x m in
     Int.Map.set h m s
 
-  let smartmap f s =
-    let fs m = Map.smartmap f m in
-    Int.Map.smartmap fs s
+  module Smart =
+  struct
+
+    let map f s =
+      let fs m = Map.Smart.map f m in
+      Int.Map.Smart.map fs s
+
+    let mapi f s =
+      let fs m = Map.Smart.mapi f m in
+      Int.Map.Smart.map fs s
+
+  end
 
-  let smartmapi f s =
-    let fs m = Map.smartmapi f m in
-    Int.Map.smartmap fs s
+  let smartmap = Smart.map
+  let smartmapi = Smart.mapi
 
   let height s = Int.Map.height s
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index cb2d01bdf..38ceed569 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -214,7 +214,7 @@ let mk_new_meta () = EConstr.mkMeta(new_meta())
 
 let non_instantiated sigma =
   let listev = Evd.undefined_map sigma in
-  Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
+  Evar.Map.Smart.map (fun evi -> nf_evar_info sigma evi) listev
 
 (************************)
 (* Manipulating filters *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 03b843655..78d5d4c8f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -510,8 +510,8 @@ let raw_map f d =
     in
     ans
   in
-  let defn_evars = EvMap.smartmapi f d.defn_evars in
-  let undf_evars = EvMap.smartmapi f d.undf_evars in
+  let defn_evars = EvMap.Smart.mapi f d.defn_evars in
+  let undf_evars = EvMap.Smart.mapi f d.undf_evars in
   { d with defn_evars; undf_evars; }
 
 let raw_map_undefined f d =
@@ -524,7 +524,7 @@ let raw_map_undefined f d =
     in
     ans
   in
-  { d with undf_evars = EvMap.smartmapi f d.undf_evars; }
+  { d with undf_evars = EvMap.Smart.mapi f d.undf_evars; }
 
 let is_evar = mem
 
@@ -1040,11 +1040,11 @@ let map_metas_fvalue f evd =
   | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
   | x -> x
   in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let map_metas f evd =
   let map cl = map_clb f cl in
-  set_metas evd (Metamap.smartmap map evd.metas)
+  set_metas evd (Metamap.Smart.map map evd.metas)
 
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
@@ -1120,7 +1120,7 @@ let retract_coercible_metas evd =
     Cltyp (na, typ)
   | v -> v
   in
-  let metas = Metamap.smartmapi map evd.metas in
+  let metas = Metamap.Smart.mapi map evd.metas in
   !mc, set_metas evd metas
 
 let evar_source_of_meta mv evd =