From f2ab2825077bf8344d2e55be433efb1891212589 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:34:22 +0200
Subject: Collecting Array.smart_* functions into a module Array.Smart.

---
 lib/rtree.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/rtree.ml b/lib/rtree.ml
index 0e371025e..d2ba6af7b 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -103,11 +103,11 @@ let rec map f t = match t with
 let smartmap f t = match t with
     Param _ -> t
   | Node (a,sons) ->
-      let a'=f a and sons' = Array.smartmap (map f) sons in
+      let a'=f a and sons' = Array.Smart.map (map f) sons in
       if a'==a && sons'==sons then t
       else Node (a',sons')
   | Rec(j,defs) ->
-      let defs' = Array.smartmap (map f) defs in
+      let defs' = Array.Smart.map (map f) defs in
       if defs'==defs then t
       else Rec(j,defs')
 
-- 
cgit v1.2.3


From d8851bbd50df1f77af0aabfe98bebd44fcb4aa02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 23 May 2018 13:35:29 +0200
Subject: Moving Rtree.smart_map into Rtree.Smart.map.

---
 checker/declarations.ml |  2 +-
 kernel/declareops.ml    |  2 +-
 lib/rtree.ml            | 28 +++++++++++++++++-----------
 lib/rtree.mli           | 11 ++++++++++-
 4 files changed, 29 insertions(+), 14 deletions(-)

(limited to 'lib')

diff --git a/checker/declarations.ml b/checker/declarations.ml
index ddd505a9a..e1d2cf6d1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -480,7 +480,7 @@ let dest_subterms p =
   let (_,cstrs) = Rtree.dest_node p in
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 let eq_recarg r1 r2 = match r1, r2 with
   | Norec, Norec -> true
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index cc0b381c9..832d478b3 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -178,7 +178,7 @@ let recarg_length p j =
   let (_,cstrs) = Rtree.dest_node p in
   Array.length (snd (Rtree.dest_node cstrs.(j-1)))
 
-let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
+let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 (** {7 Substitution of inductive declarations } *)
 
diff --git a/lib/rtree.ml b/lib/rtree.ml
index d2ba6af7b..e1c6a4c4d 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -94,22 +94,28 @@ let is_node t =
       Node _ -> true
     | _ -> false
 
-
 let rec map f t = match t with
     Param(i,j) -> Param(i,j)
   | Node (a,sons) -> Node (f a, Array.map (map f) sons)
   | Rec(j,defs) -> Rec (j, Array.map (map f) defs)
 
-let smartmap f t = match t with
-    Param _ -> t
-  | Node (a,sons) ->
-      let a'=f a and sons' = Array.Smart.map (map f) sons in
-      if a'==a && sons'==sons then t
-      else Node (a',sons')
-  | Rec(j,defs) ->
-      let defs' = Array.Smart.map (map f) defs in
-      if defs'==defs then t
-      else Rec(j,defs')
+module Smart =
+struct
+
+  let map f t = match t with
+      Param _ -> t
+    | Node (a,sons) ->
+        let a'=f a and sons' = Array.Smart.map (map f) sons in
+        if a'==a && sons'==sons then t
+        else Node (a',sons')
+    | Rec(j,defs) ->
+        let defs' = Array.Smart.map (map f) defs in
+        if defs'==defs then t
+        else Rec(j,defs')
+
+end
+
+let smartmap = Smart.map
 
 (** Structural equality test, parametrized by an equality on elements *)
 
diff --git a/lib/rtree.mli b/lib/rtree.mli
index 8edfc3d37..5ab14f603 100644
--- a/lib/rtree.mli
+++ b/lib/rtree.mli
@@ -74,13 +74,22 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t -
 
 (** Iterators *)
 
+(** See also [Smart.map] *)
 val map : ('a -> 'b) -> 'a t -> 'b t
 
-(** [(smartmap f t) == t] if [(f a) ==a ] for all nodes *)
 val smartmap : ('a -> 'a) -> 'a t -> 'a t
+(** @deprecated Same as [Smart.map] *)
 
 (** A rather simple minded pretty-printer *)
 val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t
 
 val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
 (** @deprecated Same as [Rtree.equal] *)
+
+module Smart :
+sig
+
+  (** [(Smart.map f t) == t] if [(f a) ==a ] for all nodes *)
+  val map : ('a -> 'a) -> 'a t -> 'a t
+
+end
-- 
cgit v1.2.3