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

2 files changed, 63 insertions, 0 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index 5bbc813d5..7b008b8db 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -454,3 +454,49 @@ let rev_to_list a =
 let filter_with filter v =
   Array.of_list (CList.filter_with filter (Array.to_list v))
 
+module Fun1 =
+struct
+
+  let map f arg v = match v with
+  | [| |] -> [| |]
+  | _ ->
+    let len = Array.length v in
+    let x0 = Array.unsafe_get v 0 in
+    let ans = Array.make len (f arg x0) in
+    for i = 1 to pred len do
+      let x = Array.unsafe_get v i in
+      Array.unsafe_set ans i (f arg x)
+    done;
+    ans
+
+  exception Local of int * Obj.t
+
+  let smartmap f arg v =
+    let len = Array.length v in
+    try
+      for i = 0 to len - 1 do
+        let x = uget v i in
+        let y = f arg x in
+        if x != y then (* pointer (in)equality *)
+          raise (Local (i, Obj.repr y))
+      done;
+      v
+    with Local (i, x) ->
+      (** FIXME: use Array.unsafe_blit from OCAML 4.00 *)
+      let ans : 'a array = Array.make len (uget v 0) in
+      let () = Array.blit v 0 ans 0 i in
+      let () = Array.unsafe_set ans i (Obj.obj x) in
+      for j = succ i to pred len do
+        let y = f arg (uget v j) in
+        Array.unsafe_set ans j y
+      done;
+      ans
+
+  let iter f arg v =
+    let len = Array.length v in
+    for i = 0 to pred len do
+      let x = uget v i in
+      f arg x
+    done
+
+end
diff --git a/lib/cArray.mli b/lib/cArray.mli
index e0ec095f3..fc26e1972 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. *)