aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/util.ml11
-rw-r--r--lib/util.mli1
2 files changed, 12 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml
index ed39934103..599e17adf4 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -475,6 +475,17 @@ let array_last v =
let array_cons e v = Array.append [|e|] v
+let array_rev t =
+ let n=Array.length t in
+ if n <=0 then ()
+ else
+ let tmp=ref t.(0) in
+ for i=0 to pred (n/2) do
+ tmp:=t.((pred n)-i);
+ t.((pred n)-i)<- t.(i);
+ t.(i)<- !tmp
+ done
+
let array_fold_right_i f v a =
let rec fold a n =
if n=0 then a
diff --git a/lib/util.mli b/lib/util.mli
index 7e6c3316f2..a5089a2de0 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -149,6 +149,7 @@ val array_hd : 'a array -> 'a
val array_tl : 'a array -> 'a array
val array_last : 'a array -> 'a
val array_cons : 'a -> 'a array -> 'a array
+val array_rev : 'a array -> unit
val array_fold_right_i :
(int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
val array_fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a