mach et himsg; typage sans extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@21 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 34 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 4370b4cb91..3bac54cf94 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -116,6 +116,13 @@ let list_fold_left_i f =
  in 
  it_list_f 
 
+let list_for_all_i p = 
+  let rec for_all_p i = function
+    | [] -> true 
+    | a::l -> p i a && for_all_p (i+1) l
+  in 
+  for_all_p
+
 (* Arrays *)
 
 let array_exists f v = 
@@ -167,6 +174,16 @@ let array_fold_left2 f a v1 v2 =
   else
     fold a 0
 
+let array_fold_left2_i f a v1 v2 =
+  let lv1 = Array.length v1 in
+  let rec fold a n = 
+    if n >= lv1 then a else fold (f n a v1.(n) v2.(n)) (succ n)
+  in
+  if Array.length v2 <> lv1 then
+    invalid_arg "array_fold_left2"
+  else
+    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)
@@ -201,6 +218,19 @@ let array_chop n v =
   else 
     (Array.sub v 0 n, Array.sub v n (vlen-n))
 
+let array_map2 f v1 v2 =
+  if Array.length v1 <> Array.length v2 then
+    invalid_arg "map2_vect"
+  else if Array.length v1 == 0 then 
+    [| |] 
+  else begin
+    let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
+    for i = 1 to pred (Array.length v1) do
+      res.(i) <- f v1.(i) v2.(i)
+    done;
+    res
+  end
+
 (* Functions *)
 
 let compose f g x = f (g x)
diff --git a/lib/util.mli b/lib/util.mli
index f02a205296..c5e21f350a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -33,6 +33,7 @@ val list_distinct : 'a list -> bool
 val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
 val list_index : 'a -> 'a list -> int
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
+val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 
 (* Arrays *)
 
@@ -45,12 +46,15 @@ val array_last : 'a array -> 'a
 val array_cons : 'a -> 'a array -> 'a array
 val array_fold_left2 : 
   ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c 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
 val array_fold_right_from : int -> ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 val array_app_tl : 'a array -> 'a list -> 'a list
 val array_list_of_tl : 'a array -> 'a list
 val array_map_to_list : ('a -> 'b) -> 'a array ->'b list
 val array_chop : int -> 'a array -> 'a array * 'a array
+val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
 
 (* Functions *)