Ajout array_map_left and co

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

2 files changed, 25 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 56d6717e3..89e8a7b84 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -551,6 +551,28 @@ let array_map3 f v1 v2 v3 =
     res
   end
 
+let array_map_left f a = (* Ocaml does not guarantee Array.map is LR *)
+  let l = Array.length a in (* (even if so), then we rewrite it *)
+  if l = 0 then [||] else begin
+    let r = Array.create l (f a.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i)
+    done;
+    r
+  end
+
+let array_map_left_pair f a g b =
+  let l = Array.length a in
+  if l = 0 then [||],[||] else begin
+    let r = Array.create l (f a.(0)) in
+    let s = Array.create l (g b.(0)) in
+    for i = 1 to l - 1 do
+      r.(i) <- f a.(i);
+      s.(i) <- g b.(i)
+    done;
+    r, s
+  end
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index e4a2ef707..e2e46f528 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -160,6 +160,9 @@ val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 val array_map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 val array_map3 : 
   ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+val array_map_left : ('a -> 'b) -> 'a array -> 'b array
+val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
+  'b array * 'd array
 
 (*s Matrices *)