As r15801: putting everything from Util.array_* to CArray.*.

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

1 files changed, 3 insertions, 320 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 523579d1f5..42ad11ee1f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -363,332 +363,15 @@ let ascii_of_ident s =
     done with End_of_input -> () end;
     !out
 
+(* Lists *)
+
 module List : CList.ExtS = CList
 
 let (@) = CList.append
 
 (* Arrays *)
 
-let array_compare item_cmp v1 v2 =
-  let c = compare (Array.length v1) (Array.length v2) in
-  if c<>0 then c else
-    let rec cmp = function
-	-1 -> 0
-      | i ->
-	  let c' = item_cmp v1.(i) v2.(i) in
-	  if c'<>0 then c'
-	  else cmp (i-1) in
-    cmp (Array.length v1 - 1)
-
-let array_equal cmp t1 t2 =
-  Array.length t1 = Array.length t2 &&
-  let rec aux i =
-    (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
-  in aux 0
-
-let array_exists f v =
-  let rec exrec = function
-    | -1 -> false
-    | n -> (f v.(n)) || (exrec (n-1))
-  in
-  exrec ((Array.length v)-1)
-
-let array_for_all f v =
-  let rec allrec = function
-    | -1 -> true
-    | n -> (f v.(n)) && (allrec (n-1))
-  in
-  allrec ((Array.length v)-1)
-
-let array_for_all2 f v1 v2 =
-  let rec allrec = function
-    | -1 -> true
-    | n -> (f v1.(n) v2.(n)) && (allrec (n-1))
-  in
-  let lv1 = Array.length v1 in
-  lv1 = Array.length v2 && allrec (pred lv1)
-
-let array_for_all3 f v1 v2 v3 =
-  let rec allrec = function
-    | -1 -> true
-    | n -> (f v1.(n) v2.(n) v3.(n)) && (allrec (n-1))
-  in
-  let lv1 = Array.length v1 in
-  lv1 = Array.length v2 && lv1 = Array.length v3 && allrec (pred lv1)
-
-let array_for_all4 f v1 v2 v3 v4 =
-  let rec allrec = function
-    | -1 -> true
-    | n -> (f v1.(n) v2.(n) v3.(n) v4.(n)) && (allrec (n-1))
-  in
-  let lv1 = Array.length v1 in
-  lv1 = Array.length v2 &&
-  lv1 = Array.length v3 &&
-  lv1 = Array.length v4 &&
-    allrec (pred lv1)
-
-let array_for_all_i f i v =
-  let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in
-  allrec i 0
-
-exception Found of int
-
-let array_find_i (pred: int -> 'a -> bool) (arr: 'a array) : int option =
-  try
-    for i=0 to Array.length arr - 1 do if pred i (arr.(i)) then raise (Found i) done;
-    None
-  with Found i -> Some i
-
-let array_hd v =
-  match Array.length v with
-    | 0 -> failwith "array_hd"
-    | _ -> v.(0)
-
-let array_tl v =
-  match Array.length v with
-    | 0 -> failwith "array_tl"
-    | n -> Array.sub v 1 (pred n)
-
-let array_last v =
-  match Array.length v with
-    | 0 -> failwith "array_last"
-    | n -> v.(pred n)
-
-let array_cons e v = Array.append [|e|] v
-
-let array_rev t =
-  let n=Array.length t in
-    if n <=0 then ()
-    else
-      let tmp=ref t.(0) in
-      for i=0 to pred (n/2) do
-	tmp:=t.((pred n)-i);
-	t.((pred n)-i)<- t.(i);
-	t.(i)<- !tmp
-      done
-
-let array_fold_right_i f v a =
-  let rec fold a n =
-    if n=0 then a
-    else
-      let k = n-1 in
-      fold (f k v.(k) a) k in
-  fold a (Array.length v)
-
-let array_fold_left_i f v a =
-  let n = Array.length a in
-  let rec fold i v = if i = n then v else fold (succ i) (f i v a.(i)) in
-  fold 0 v
-
-let array_fold_right2 f v1 v2 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 v1.(k) v2.(k) a) k in
-  if Array.length v2 <> lv1 then invalid_arg "array_fold_right2";
-  fold a lv1
-
-let array_fold_left2 f a v1 v2 =
-  let lv1 = Array.length v1 in
-  let rec fold a n =
-    if n >= lv1 then a else fold (f a v1.(n) v2.(n)) (succ n)
-  in
-  if Array.length v2 <> lv1 then invalid_arg "array_fold_left2";
-  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";
-  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)
-  in
-  fold a n
-
-let array_fold_right_from n f v a =
-  let rec fold n =
-    if n >= Array.length v then a else f v.(n) (fold (succ n))
-  in
-  fold n
-
-let array_app_tl v l =
-  if Array.length v = 0 then invalid_arg "array_app_tl";
-  array_fold_right_from 1 (fun e l -> e::l) v l
-
-let array_list_of_tl v =
-  if Array.length v = 0 then invalid_arg "array_list_of_tl";
-  array_fold_right_from 1 (fun e l -> e::l) v []
-
-let array_map_to_list f v =
-  List.map f (Array.to_list v)
-
-let array_chop n v =
-  let vlen = Array.length v in
-  if n > vlen then failwith "array_chop";
-  (Array.sub v 0 n, Array.sub v n (vlen-n))
-
-exception Local of int
-
-(* If none of the elements is changed by f we return ar itself.
-   The for loop looks for the first such an element.
-   If found it is temporarily stored in a ref and the new array is produced,
-   but f is not re-applied to elements that are already checked *)
-let array_smartmap f ar =
-  let ar_size = Array.length ar in
-  let aux = ref None in
-  try
-    for i = 0 to ar_size-1 do
-      let a = ar.(i) in
-      let a' = f a in
-	if a != a' then (* pointer (in)equality *) begin
-	  aux := Some a';
-	  raise (Local i)
-	end
-    done;
-    ar
-  with
-      Local i ->
-	let copy j =
-	  if j<i then ar.(j)
-	  else if j=i then
-	    match !aux with Some a' -> a' | None -> failwith "Error"
-	  else f (ar.(j))
-	in
-	  Array.init ar_size copy
-
-let array_map2 f v1 v2 =
-  if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
-  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
-
-let array_map2_i f v1 v2 =
-  if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
-  if Array.length v1 == 0 then
-    [| |]
-  else begin
-    let res = Array.create (Array.length v1) (f 0 v1.(0) v2.(0)) in
-    for i = 1 to pred (Array.length v1) do
-      res.(i) <- f i v1.(i) v2.(i)
-    done;
-    res
-  end
-
-let array_map3 f v1 v2 v3 =
-  if Array.length v1 <> Array.length v2 ||
-     Array.length v1 <> Array.length v3 then invalid_arg "array_map3";
-  if Array.length v1 == 0 then
-    [| |]
-  else begin
-    let res = Array.create (Array.length v1) (f v1.(0) v2.(0) v3.(0)) in
-    for i = 1 to pred (Array.length v1) do
-      res.(i) <- f v1.(i) v2.(i) v3.(i)
-    done;
-    res
-  end
-
-let array_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 l = 0 then [||] else begin
-    let r = Array.create l (f a.(0)) in
-    for i = 1 to l - 1 do
-      r.(i) <- f a.(i)
-    done;
-    r
-  end
-
-let array_map_left_pair f a g b =
-  let l = Array.length a in
-  if l = 0 then [||],[||] else begin
-    let r = Array.create l (f a.(0)) in
-    let s = Array.create l (g b.(0)) in
-    for i = 1 to l - 1 do
-      r.(i) <- f a.(i);
-      s.(i) <- g b.(i)
-    done;
-    r, s
-  end
-
-let array_iter2 f v1 v2 =
-  let n = Array.length v1 in
-  if Array.length v2 <> n then invalid_arg "array_iter2"
-  else for i = 0 to n - 1 do f v1.(i) v2.(i) done
-
-let pure_functional = false
-
-let array_fold_map' f v e =
-if pure_functional then
-  let (l,e) =
-    Array.fold_right
-      (fun x (l,e) -> let (y,e) = f x e in (y::l,e))
-      v ([],e) in
-  (Array.of_list l,e)
-else
-  let e' = ref e in
-  let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
-  (v',!e')
-
-let array_fold_map f e v =
-  let e' = ref e in
-  let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
-  (!e',v')
-
-let array_fold_map2' f v1 v2 e =
-  let e' = ref e in
-  let v' =
-    array_map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2
-  in
-  (v',!e')
-
-let array_distinct v =
-  let visited = Hashtbl.create 23 in
-  try
-    Array.iter
-      (fun x ->
-        if Hashtbl.mem visited x then raise Exit
-        else Hashtbl.add visited x x)
-      v;
-    true
-  with Exit -> false
-
-let array_union_map f a acc =
-  Array.fold_left
-    (fun x y -> f y x)
-    acc
-    a
-
-let array_rev_to_list a =
-  let rec tolist i res =
-    if i >= Array.length a then res else tolist (i+1) (a.(i) :: res) in
-  tolist 0 []
-
-let array_filter_along f filter v =
-  Array.of_list (CList.filter_along f filter (Array.to_list v))
-
-let array_filter_with filter v =
-  Array.of_list (CList.filter_with filter (Array.to_list v))
+module Array : CArray.ExtS = CArray
 
 (* Matrices *)