From a45a7f0411f19c10f7a50a02b84c1820c5907bb0 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 4 Nov 2013 12:17:57 +0000
Subject: 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
---
 lib/cArray.mli | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'lib/cArray.mli')

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. *)
-- 
cgit v1.2.3