module Refiner

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

2 files changed, 22 insertions, 0 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 440acd6ba..0f900ff92 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -127,6 +127,25 @@ let list_except x l = List.filter (fun y -> not (x = y)) l
 
 let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
 
+let list_map_i f = 
+  let rec map_i_rec i = function
+    | [] -> [] 
+    | x::l -> let v = f i x in v::map_i_rec (i+1) l
+  in 
+  map_i_rec
+
+let rec list_sep_last = function
+  | [] -> failwith "sep_last"
+  | hd::[] -> (hd,[])
+  | hd::tl -> let (l,tl) = list_sep_last tl in (l,hd::tl)
+
+let list_try_find_i f = 
+  let rec try_find_f n = function
+    | [] -> failwith "try_find_i"
+    | h::t -> try f n h with Failure _ -> try_find_f (n+1) t
+  in 
+  try_find_f
+
 (* Arrays *)
 
 let array_exists f v = 
diff --git a/lib/util.mli b/lib/util.mli
index ef56afeb2..7998dde2a 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -41,6 +41,9 @@ 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
 val list_except : 'a -> 'a list -> 'a list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_sep_last : 'a list -> 'a * 'a list
+val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
 
 (*s Arrays. *)