From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 25 Jun 2009 10:17:13 +0000 (+0000)
Subject: new function list_mapi_acc
X-Git-Tag: make_still_working~3803
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0179e12340029c8316e3819c1f39171d878adc7;p=helm.git

new function list_mapi_acc
---

diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml
index 8451eb6b8..49d28bbb9 100644
--- a/helm/software/components/extlib/hExtlib.ml
+++ b/helm/software/components/extlib/hExtlib.ml
@@ -148,6 +148,14 @@ let list_mapi f l =
      aux 0 l
 ;;
 
+let list_mapi_acc f a l =
+  let rec aux k a res = function
+    | [] -> a, List.rev res
+    | h::tl -> let a,h = f h k a in aux (k+1) a (h::res) tl
+  in
+   aux 0 a [] l
+;;
+
 let list_index p =
  let rec aux n =
   function
diff --git a/helm/software/components/extlib/hExtlib.mli b/helm/software/components/extlib/hExtlib.mli
index a0b85ca4f..63bfc25f1 100644
--- a/helm/software/components/extlib/hExtlib.mli
+++ b/helm/software/components/extlib/hExtlib.mli
@@ -95,6 +95,8 @@ val list_findopt: ('a -> int -> 'b option) -> 'a list -> 'b option
 val flatten_map: ('a -> 'b list) -> 'a list -> 'b list
 val list_last: 'a list -> 'a
 val list_mapi: ('a -> int -> 'b) -> 'a list -> 'b list
+val list_mapi_acc: 
+      ('a -> int -> 'acc -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list 
 (* Finds the zero based index of the first element that satisfies a predicate*)
 val list_index: ('a -> bool) -> 'a list -> (int * 'a) option
 val sharing_map: ('a -> 'a) -> 'a list -> 'a list