diff options
| author | Pierre-Marie Pédrot | 2018-10-25 13:31:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-29 17:47:15 +0100 |
| commit | d5e762723bca7cb9297183e4332e0a9c7c0932f0 (patch) | |
| tree | 9eb7b8bf161c210a9c5b676e97fd09ff742daf0d /clib | |
| parent | 9ead21a38feae29fdde11344de326de86bfe8ad9 (diff) | |
Do not compare the type arguments in pattern-match branches.
We know that the two are living in a common type, so that it is useless
to perform the comparison check. Note that we only use this fast-path when
the branches are only made of lambda-abstractions, but this covers
all actual cases.
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/cArray.ml | 12 | ||||
| -rw-r--r-- | clib/cArray.mli | 2 |
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 : |