micromega : bug fixes and optimisations

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

1 files changed, 40 insertions, 0 deletions

diff --git a/contrib/micromega/mutils.ml b/contrib/micromega/mutils.ml
index 2473608f2..03e3999fd 100644
--- a/contrib/micromega/mutils.ml
+++ b/contrib/micromega/mutils.ml
@@ -17,6 +17,15 @@ let debug = false
 let fst' (Micromega.Pair(x,y)) = x
 let snd' (Micromega.Pair(x,y)) = y
 
+let map_option f x = 
+  match x with
+    | None -> None
+    | Some v -> Some (f v)
+
+let from_option = function
+  | None -> failwith "from_option"
+  | Some v -> v  
+
 let rec try_any l x = 
  match l with
   | [] -> None
@@ -24,6 +33,37 @@ let rec try_any l x =
      | None -> try_any l x
      | x -> x
 
+let iteri f l =
+ let rec xiter i l = 
+  match l with
+   | [] -> ()
+   | e::l -> f i e ; xiter (i+1) l in
+  xiter 0 l
+
+let mapi f l =
+ let rec xmap i l = 
+  match l with
+   | [] -> []
+   | e::l -> (f i e)::xmap (i+1) l in
+  xmap 0 l
+
+let rec map3 f l1 l2 l3 = 
+  match l1 , l2 ,l3 with
+    | [] , [] , [] -> []
+    | e1::l1 , e2::l2 , e3::l3 -> (f e1 e2 e3)::(map3 f l1 l2 l3)
+    |      _   -> raise (Invalid_argument "map3")
+
+
+let rec is_sublist l1 l2 = 
+  match l1 ,l2 with
+    | [] ,_ -> true
+    | e::l1', [] -> false
+    | e::l1' , e'::l2' -> 
+	if e = e' then is_sublist l1' l2'
+	else is_sublist l1 l2'
+		
+
+
 let list_try_find f =
   let rec try_find_f = function
     | [] -> failwith "try_find"