Ajout array_fold_map', list_fold_map' et list_remove_first

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

3 files changed, 35 insertions, 12 deletions

diff --git a/lib/util.ml b/lib/util.ml
index 953c8187e2..33f91b04ee 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -250,6 +250,13 @@ let list_for_all_i p =
 
 let list_except x l = List.filter (fun y -> not (x = y)) l
 
+let list_remove = list_except (* Alias *)
+
+let rec list_remove_first a = function
+  | b::l when a = b -> l
+  | b::l -> b::list_remove_first a l
+  | [] -> raise Not_found
+
 let list_for_all2eq f l1 l2 = try List.for_all2 f l1 l2 with Failure _ -> false
 
 let list_map_i f = 
@@ -361,12 +368,12 @@ let list_share_tails l1 l2 =
 
 let list_join_map f l = List.flatten (List.map f l)
 
-let rec list_fold_map f e = function 
+let rec list_fold_map f e = function
   |  []  -> (e,[])
-  |  h::t -> 
+  |  h::t ->
        let e',h' = f e h in
        let e'',t' = list_fold_map f e' t in
-	 e'',h'::t'
+         e'',h'::t'
 
 (* (* tail-recursive version of the above function *)
 let list_fold_map f e l = 
@@ -378,6 +385,10 @@ let list_fold_map f e l =
     (e',List.rev lrev)
 *)
 
+(* The same, based on fold_right, with the effect accumulated on the right *)
+let list_fold_map' f l e =
+  List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
 (* Arrays *)
@@ -595,6 +606,20 @@ let array_map_left_pair f a g b =
     r, s
   end
 
+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')
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index 9497f9a4d2..f330ef8e00 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -106,6 +106,8 @@ val list_fold_right_and_left :
     ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
+val list_remove : 'a -> 'a list -> 'a list
+val list_remove_first : 'a -> 'a list -> 'a list
 val list_for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val list_sep_last : 'a list -> 'a * 'a list
 val list_try_find_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b
@@ -127,8 +129,8 @@ val list_share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
 val list_join_map : ('a -> 'b list) -> 'a list -> 'b list
 (* [list_fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
    where [(e_i,k_i)=f e_{i-1} l_i] *)
-val list_fold_map : 
-  ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list 
+val list_fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+val list_fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
 val list_map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
 
 (*s Arrays. *)
@@ -167,6 +169,7 @@ val array_map3 :
 val array_map_left : ('a -> 'b) -> 'a array -> 'b array
 val array_map_left_pair : ('a -> 'b) -> 'a array -> ('c -> 'd) -> 'c array ->
   'b array * 'd array
+val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
 
 (*s Matrices *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index fe0e2cca47..404e06f991 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -385,11 +385,6 @@ let implicits_of_global r =
 
 (* Declare manual implicits *)
 
-let rec list_remove a = function
-  | b::l when a = b -> l
-  | b::l -> b::list_remove a l
-  | [] -> raise Not_found
-
 let set_implicit id imp =
   Some (id,match imp with None -> Manual | Some imp -> imp)
 
@@ -403,9 +398,9 @@ let declare_manual_implicits r l =
   let rec merge k l = function
     | (Name id,imp)::imps ->
 	let l',imp =
-	  try list_remove (ExplByPos k) l, set_implicit id imp
+	  try list_remove_first (ExplByPos k) l, set_implicit id imp
 	  with Not_found ->
-	  try list_remove (ExplByName id) l, set_implicit id imp
+	  try list_remove_first (ExplByName id) l, set_implicit id imp
 	  with Not_found ->
 	  l, None in
 	imp :: merge (k+1) l' imps