Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

4 files changed, 29 insertions, 0 deletions

diff --git a/clib/cArray.ml b/clib/cArray.ml
index e0a1859184..145a32cf45 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -52,6 +52,8 @@ sig
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+  val map3_i :
+    (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   val iter2_i : (int -> 'a -> 'b -> unit) -> 'a array -> 'b array -> unit
   val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
@@ -358,6 +360,21 @@ let map3 f v1 v2 v3 =
     res
   end
 
+let map3_i f v1 v2 v3 =
+  let len1 = Array.length v1 in
+  let len2 = Array.length v2 in
+  let len3 = Array.length v3 in
+  let () = if not (Int.equal len1 len2 && Int.equal len1 len3) then invalid_arg "Array.map3_i" in
+  if Int.equal len1 0 then
+    [| |]
+  else begin
+    let res = Array.make len1 (f 0 (uget v1 0) (uget v2 0) (uget v3 0)) in
+    for i = 1 to pred len1 do
+      Array.unsafe_set res i (f i (uget v1 i) (uget v2 i) (uget v3 i))
+    done;
+    res
+  end
+
 let 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 Int.equal l 0 then [||] else begin
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 21479d2b45..8aca31ad33 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -83,6 +83,8 @@ sig
   val map2_i : (int -> 'a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
   val map3 :
     ('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
+  val map3_i :
+    (int -> 'a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
 
   val map_left : ('a -> 'b) -> 'a array -> 'b array
   (** As [map] but guaranteed to be left-to-right. *)
diff --git a/clib/cList.ml b/clib/cList.ml
index 524945ef23..aa01f6e5b5 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -98,6 +98,7 @@ sig
   val split : ('a * 'b) list -> 'a list * 'b list
   val combine : 'a list -> 'b list -> ('a * 'b) list
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
+  val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   val add_set : 'a eq -> 'a -> 'a list -> 'a list
   val eq_set : 'a eq -> 'a list -> 'a list -> bool
@@ -846,6 +847,12 @@ let split3 = function
     split3_loop cp cq cr l;
     (cast cp, cast cq, cast cr)
 
+(** XXX TODO tailrec *)
+let rec split4 = function
+  | [] -> ([], [], [], [])
+  | (a,b,c,d)::l ->
+      let (ra, rb, rc, rd) = split4 l in (a::ra, b::rb, c::rc, d::rd)
+
 let rec combine3_loop p l1 l2 l3 = match l1, l2, l3 with
   | [], [], [] -> ()
   | x :: l1, y :: l2, z :: l3 ->
diff --git a/clib/cList.mli b/clib/cList.mli
index 8582e6cd65..a2fe0b759a 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -308,6 +308,9 @@ sig
   val split3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list
   (** Like [split] but for triples *)
 
+  val split4 : ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
+  (** Like [split] but for quads *)
+
   val combine3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list
   (** Like [combine] but for triples *)