Adding closure-preventing functions in CArray. These functions are all

higher-order functions like map and iter, and they are modified so that
they take one additional argument, thus saving a cloure allocation.

Compare the following.

Array.iter: ('a -> unit) -> 'a array -> unit
Array.Fun1.iter: ('r -> 'a -> unit) -> 'r -> 'a array -> unit

Basically, Array.Fun1.iter f x v = Array.iter (f x) v, though it does not
allocate a closure.

For now only the most critical functions are recoded.

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

1 files changed, 17 insertions, 0 deletions

diff --git a/lib/cArray.mli b/lib/cArray.mli
index e0ec095f3e..fc26e19722 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -138,3 +138,20 @@ sig
 end
 
 include ExtS
+
+module Fun1 :
+sig
+  val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
+  (** [Fun1.map f x v = map (f x) v] *)
+
+  val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+  (** [Fun1.smartmap f x v = smartmap (f x) v] *)
+
+  val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
+  (** [Fun1.iter f x v = iter (f x) v] *)
+
+end
+(** The functions defined in this module are the same as the main ones, except
+    that they are all higher-order, and their function arguments have an
+    additional parameter. This allows to prevent closure creation in critical
+    cases. *)