module Closure

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

2 files changed, 34 insertions, 3 deletions

diff --git a/lib/util.ml b/lib/util.ml
index adf3c757a..625ceed87 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -69,6 +69,14 @@ let intersect l1 l2 =
 let subtract l1 l2 =
   if l2 = [] then l1 else List.filter (fun x -> not (List.mem x l2)) l1
 
+let list_chop n l = 
+  let rec chop_aux acc = function
+    | (0, l2) -> (List.rev acc, l2)
+    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+    | (_, []) -> failwith "chop_list"
+  in 
+  chop_aux [] (n,l)
+ 
 (* Arrays *)
 
 let array_exists f v = 
@@ -78,6 +86,13 @@ let array_exists f v =
   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
@@ -86,15 +101,20 @@ let array_for_all2 f v1 v2 =
   let lv1 = Array.length v1 in
   lv1 = Array.length v2 && allrec (pred lv1) 
 
+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_hd v = 
+let array_last v =
   match Array.length v with
-    | 0 -> failwith "array_hd"
-    | _ -> v.(0)
+    | 0 -> failwith "aray_last"
+    | n -> v.(pred n)
 
 let array_cons e v = Array.append [|e|] v
 
@@ -125,6 +145,13 @@ let array_list_of_tl 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 "chop_vect"
+  else 
+    (Array.sub v 0 n, Array.sub v n (vlen-n))
+
 (* Functions *)
 
 let compose f g x = f (g x)
diff --git a/lib/util.mli b/lib/util.mli
index 4e92b46b8..92aabea5d 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -24,19 +24,23 @@ val parse_section_path : string -> string list * string * string
 
 val intersect : 'a list -> 'a list -> 'a list
 val subtract : 'a list -> 'a list -> 'a list
+val list_chop  : int -> 'a list -> 'a list * 'a list
 
 (* Arrays *)
 
 val array_exists : ('a -> bool) -> 'a array -> bool
+val array_for_all : ('a -> bool) -> 'a array -> bool
 val array_for_all2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
 val array_hd : 'a array -> 'a
 val array_tl : 'a array -> 'a array
+val array_last : 'a array -> 'a
 val array_cons : 'a -> 'a array -> 'a array
 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
 
 (* Functions *)