diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 9 | ||||
| -rw-r--r-- | lib/util.mli | 2 |
2 files changed, 11 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index a8e716e0f3..242c203211 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1000,6 +1000,15 @@ let array_fold_left2_i f a v1 v2 = if Array.length v2 <> lv1 then invalid_arg "array_fold_left2"; fold a 0 +let array_fold_left3 f a v1 v2 v3 = + let lv1 = Array.length v1 in + let rec fold a n = + if n >= lv1 then a else fold (f a v1.(n) v2.(n) v3.(n)) (succ n) + in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 then + invalid_arg "array_fold_left2"; + fold a 0 + let array_fold_left_from n f a v = let rec fold a n = if n >= Array.length v then a else fold (f a v.(n)) (succ n) diff --git a/lib/util.mli b/lib/util.mli index 5248d0e6b1..2216ba9813 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -259,6 +259,8 @@ val array_fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c val array_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a +val array_fold_left3 : + ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a val array_fold_left2_i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val array_fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a |