aboutsummaryrefslogtreecommitdiff
path: root/clib
diff options
context:
space:
mode:
authorMaxime Dénès2018-11-05 13:02:38 +0100
committerMaxime Dénès2018-11-05 13:02:38 +0100
commit538a54e8855d477e9ca350a76f852a147809a06b (patch)
tree05b825e775c1e4a50d844cde8fd88176e0a1bf48 /clib
parent62c75af6595fc31ec076b1bedfae62f652eda05e (diff)
parentd5e762723bca7cb9297183e4332e0a9c7c0932f0 (diff)
Merge PR #8824: Do not check convertibility of pattern types in the kernel
Diffstat (limited to 'clib')
-rw-r--r--clib/cArray.ml12
-rw-r--r--clib/cArray.mli2
2 files changed, 14 insertions, 0 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml
index 9644834381..c3a693ff16 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -35,6 +35,8 @@ sig
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+ val fold_right3 :
+ ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd
val fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :
@@ -252,6 +254,16 @@ let fold_left2_i f a v1 v2 =
if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i";
fold a 0
+let fold_right3 f v1 v2 v3 a =
+ let lv1 = Array.length v1 in
+ let rec fold a n =
+ if n=0 then a
+ else
+ let k = n-1 in
+ fold (f (uget v1 k) (uget v2 k) (uget v3 k) a) k in
+ if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_right3";
+ fold a lv1
+
let fold_left3 f a v1 v2 v3 =
let lv1 = Array.length v1 in
let rec fold a n =
diff --git a/clib/cArray.mli b/clib/cArray.mli
index e65a56d15e..21479d2b45 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -58,6 +58,8 @@ sig
val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a
val fold_right2 :
('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c
+ val fold_right3 :
+ ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd
val fold_left2 :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :