aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/rtree.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 13:35:29 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-23 18:50:10 +0200
commitd8851bbd50df1f77af0aabfe98bebd44fcb4aa02 (patch)
tree8c2385ac275d1ef50cc6b8c4c34ff8a58c115aca /lib/rtree.ml
parentbb2d7f94ba8688f57dc62ca72a857b82368aa784 (diff)
Moving Rtree.smart_map into Rtree.Smart.map.
Diffstat (limited to 'lib/rtree.ml')
-rw-r--r--lib/rtree.ml28
1 files changed, 17 insertions, 11 deletions
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 *)