More in IArray

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

2 files changed, 323 insertions, 29 deletions

diff --git a/lib/iArray.ml b/lib/iArray.ml
index 59ce6fb9c..8dbe3f6c6 100644
--- a/lib/iArray.ml
+++ b/lib/iArray.ml
@@ -10,27 +10,32 @@ module type US =
 sig
   type +'a t
   (** We put it covariant even though it isn't, as we're going to use it purely
-      functionnaly. *)
+      functionally. *)
   val length : 'a t -> int
   val create : int -> 'a t
   val copy : 'a t -> 'a t
   val get : 'a t -> int -> 'a
   val set : 'a t -> int -> 'a -> unit
+  val safe_get : 'a t -> int -> 'a
+  val safe_set : 'a t -> int -> 'a -> unit
 end
 (** Minimal signature of unsafe arrays *)
 
-module ObjArray =
+module ObjArray : US =
 struct
   type +'a t = Obj.t
 
   type dummy = int option
   (** We choose this type such that:
       1. It is not a float, not to trigger the float unboxing mechanism
-      2. It is not a scalar, to ensure calling of the caml_copy function,
+      2. It is not a scalar, to ensure calling of the caml_modify function,
         otherwise that may result in strange GC behaviour.
   *)
 
-  let length = Obj.size
+  let length obj =
+    let obj : dummy array = Obj.magic obj in
+    Array.length obj
+
   let create len = Obj.new_block 0 len
   let copy obj = Obj.dup obj
 
@@ -43,20 +48,26 @@ struct
     let x : dummy = Obj.magic x in
     let obj : dummy array = Obj.magic obj in
     Array.unsafe_set obj i x
+
+  let safe_get (obj : 'a t) i : 'a =
+    let obj : dummy array = Obj.magic obj in
+    let ans = Array.get obj i in
+    Obj.magic ans
+
+  let safe_set (obj : 'a t) i (x : 'a) =
+    let x : dummy = Obj.magic x in
+    let obj : dummy array = Obj.magic obj in
+    Array.set obj i x
+
 end
 
-module Make(M : US) =
-struct
+module M = ObjArray
 
 type +'a t = 'a M.t
 
 let length = M.length
 
-let get t i =
-  if i < 0 || M.length t <= i then
-    invalid_arg "Array.get"
-  else
-    M.get t i
+let get = M.safe_get
 
 (* let set t i x =
   if i < 0 || M.length t <= i then
@@ -73,7 +84,9 @@ let make len x =
   in
   ans
 
-let copy = M.copy
+let is_empty t = M.length t = 0
+
+(* let copy = M.copy *)
 
 let init len f =
   let ans = M.create len in
@@ -124,7 +137,7 @@ let concat l =
 let sub t off len =
   let tlen = M.length t in
   let () = if off < 0 || off + len > tlen then
-    invalid_arg "Array.sub"
+    invalid_arg "IArray.sub"
   in
   let ans = M.create len in
   let () =
@@ -153,6 +166,8 @@ let to_list t =
   in
   iter (M.length t - 1) []
 
+(** ITERS *)
+
 let iter f t =
   for i = 0 to M.length t - 1 do
     f (M.get t i)
@@ -163,6 +178,8 @@ let iteri f t =
     f i (M.get t i)
   done
 
+(** MAPS *)
+
 let map f t =
   let len = M.length t in
   let ans = M.create len in
@@ -183,13 +200,79 @@ let mapi f t =
   in
   ans
 
-let fold_right f accu t =
+let map2 f t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.map2" in
+  let ans = M.create len1 in
+  for i = 0 to len1 do
+    M.set ans i (f (M.get t1 i) (M.get t2 i));
+  done;
+  ans
+
+let map2i f t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.map2i" in
+  let ans = M.create len1 in
+  for i = 0 to len1 do
+    M.set ans i (f i (M.get t1 i) (M.get t2 i));
+  done;
+  ans
+
+let map3 f t1 t2 t3 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let len3 = M.length t3 in
+  let () = if len1 <> len2 || len1 <> len3 then invalid_arg "IArray.map3" in
+  let ans = M.create len1 in
+  for i = 0 to len1 do
+    M.set ans i (f (M.get t1 i) (M.get t2 i) (M.get t3 i));
+  done;
+  ans
+
+let smartmap f t =
+  let len = M.length t in
+  let rec loop i =
+    if i = len then t
+    else
+      let x = M.get t i in
+      let y = f x in
+      if x == y then loop (succ i)
+      (* We have to do it by hand *)
+      else begin
+        let ans = M.create len in
+        for j = 0 to pred i do
+          M.set ans j (M.get t j)
+        done;
+        M.set ans i y;
+        for j = succ i to pred len do
+          M.set ans i (f (M.get t i))
+        done;
+        ans
+      end
+  in
+  loop 0
+
+(** FOLDS *)
+
+let fold_right f t accu =
   let rec fold i accu =
     if i < 0 then accu
     else fold (pred i) (f (M.get t i) accu)
   in
   fold (M.length t - 1) accu
 
+let fold_right2 f t1 t2 accu =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.fold_right2" in
+  let rec fold i accu =
+    if i < 0 then accu
+    else fold (pred i) (f (M.get t1 i) (M.get t2 i) accu)
+  in
+  fold (len1 - 1) accu
+
 let fold_left f accu t =
   let len = M.length t in
   let rec fold i accu =
@@ -198,32 +281,192 @@ let fold_left f accu t =
   in
   fold 0 accu
 
-end
+let fold_lefti f accu t =
+  let len = M.length t in
+  let rec fold i accu =
+    if len <= i then accu
+    else fold (succ i) (f i accu (M.get t i))
+  in
+  fold 0 accu
+
+let fold_left2 f accu t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.fold_left2" in
+  let rec fold i accu =
+    if len1 <= i then accu
+    else fold (succ i) (f accu (M.get t1 i) (M.get t2 i))
+  in
+  fold 0 accu
+
+let fold_left2i f accu t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.fold_left2" in
+  let rec fold i accu =
+    if len1 <= i then accu
+    else fold (succ i) (f i accu (M.get t1 i) (M.get t2 i))
+  in
+  fold 0 accu
+
+(** FORALL *)
+
+let for_all f t =
+  let len = M.length t in
+  let rec loop i =
+    if i = len then true
+    else f (M.get t i) && loop (succ i)
+  in
+  loop 0
+
+let for_all2 f t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let () = if len1 <> len2 then invalid_arg "IArray.fold_left2" in
+  let rec loop i =
+    if i = len1 then true
+    else f (M.get t1 i) (M.get t2 i) && loop (succ i)
+  in
+  loop 0
+
+(** EXISTS *)
+
+let exists f t =
+  let len = M.length t in
+  let rec loop i =
+    if i = len then false
+    else f (M.get t i) || loop (succ i)
+  in
+  loop 0
+
+(** OTHERS *)
+
+let compare f t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let c = Pervasives.compare len1 len2 in
+  let rec loop i =
+    if i = len1 then 0
+    else
+      let x1 = M.get t1 i in
+      let x2 = M.get t2 i in
+      let c = f x1 x2 in
+      if c = 0 then loop (succ i)
+      else c
+  in
+  if c = 0 then loop 0
+  else c
+
+let equal f t1 t2 =
+  let len1 = M.length t1 in
+  let len2 = M.length t2 in
+  let rec loop i =
+    if i = len1 then true
+    else
+      let x1 = M.get t1 i in
+      let x2 = M.get t2 i in
+      f x1 x2 && loop (succ i)
+  in
+  if len1 = len2 then loop 0
+  else false
+
+let of_array t =
+  let len = Array.length t in
+  let ans = M.create len in
+  for i = 0 to pred len do
+    M.set ans i (Array.unsafe_get t i)
+  done;
+  ans
+
+let to_array t =
+  let init i = M.get t i in
+  Array.init (M.length t) init
+
+(** Purely functional equivalents *)
+
+let set t i x =
+  let ans = M.copy t in
+  let () = M.safe_set t i x in
+  ans
+
+let fill t off len x =
+  let tlen = M.length t in
+  let () =
+    if off < 0 || len < 0 || off > tlen - len
+    then invalid_arg "IArray.fill"
+  in
+  let ans = M.create tlen in
+  for i = 0 to pred off do
+    M.set ans i (M.get t i)
+  done;
+  for i = off to off + len - 1 do
+    M.set t i x
+  done;
+  for i = off + len to pred tlen do
+    M.set ans i (M.get t i)
+  done;
+  ans
+
+let blit src soff dst doff len =
+  let slen = M.length src in
+  let dlen = M.length dst in
+  let () =
+    if len < 0 || soff < 0 || soff > slen - len ||
+      doff < 0 || doff > dlen - len
+    then invalid_arg "IArray.blit"
+  in
+  let ans = M.create dlen in
+  for i = 0 to pred doff do
+    M.set ans i (M.get dst i)
+  done;
+  for i = 0 to pred len do
+    M.set ans (doff + i) (M.get src (soff + i))
+  done;
+  for i = doff + len to pred dlen do
+    M.set ans i (M.get dst i)
+  done;
+  ans
+
+(** Specific *)
+
+let empty = M.create 0
+
+let singleton x = make 1 x
+
+let diff t = function
+| [] -> t
+| l ->
+  let ans = M.copy t in
+  let iter (i, x) = M.safe_set ans i x in
+  let () = List.iter iter l in
+  ans
+
+(* end *)
 
-module M = Make(ObjArray)
+(* module M = Make(ObjArray) *)
 
-include M
+(* include M *)
 
 module Unsafe =
 struct
 
-let get = ObjArray.get
+let get = M.get
 
-let set = ObjArray.set
+let set = M.set
 
-let of_array (t : 'a array) : 'a ObjArray.t =
+let of_array (t : 'a array) : 'a M.t =
   let tag = Obj.tag (Obj.repr t) in
   let () = if tag = Obj.double_array_tag then
-    invalid_arg "Array.of_array"
+    invalid_arg "IArray.of_array"
   in
   Obj.magic t
 
-let to_array (t : 'a ObjArray.t) : 'a array =
-  if Obj.size t = 0 then [||]
+let to_array (t : 'a M.t) : 'a array =
+  if Obj.size (Obj.repr t) = 0 then [||]
   else
-    let dummy = Obj.field t 0 in
+    let dummy = Obj.field (Obj.repr t) 0 in
     let () = if Obj.tag dummy = Obj.double_tag then
-      invalid_arg "Array.to_array"
+      invalid_arg "IArray.to_array"
     in
     Obj.magic t
 
diff --git a/lib/iArray.mli b/lib/iArray.mli
index 911de4062..9c28eb82b 100644
--- a/lib/iArray.mli
+++ b/lib/iArray.mli
@@ -6,17 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+(** This module defines immutable arrays. Compared to usual arrays, they ensure
+    that they cannot be modified dynamically. We also use some optimization
+    tricks taking advantage of this fact. *)
+
 type +'a t
 (** Immutable arrays containing elements of type ['a]. *)
 
 (** {5 Operations inherited from [Array]}
 
-  Refer to the documentation of [CArray] for greater detail.
-
-*)
+  Refer to the documentation of [CArray] for greater detail. *)
 
+val get : 'a t -> int -> 'a
 val length : 'a t -> int
 val make : int -> 'a -> 'a t
+val is_empty : 'a t -> bool
 val init : int -> (int -> 'a) -> 'a t
 val append : 'a t -> 'a t -> 'a t
 val concat : 'a t list -> 'a t
@@ -25,10 +29,57 @@ val of_list : 'a list -> 'a t
 val to_list : 'a t -> 'a list
 val iter : ('a -> unit) -> 'a t -> unit
 val iteri : (int -> 'a -> unit) -> 'a t -> unit
+
 val map : ('a -> 'b) -> 'a t -> 'b t
 val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t
-val fold_right : ('a -> 'b -> 'b) -> 'b -> 'a t -> 'b
+val map2 : ('a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
+val map2i : (int -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t
+val map3 : ('a -> 'b -> 'c -> 'd) -> 'a t -> 'b t -> 'c t -> 'd t
+val smartmap : ('a -> 'a) -> 'a t -> 'a t
+
+val fold_right : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
+
 val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+val fold_lefti : (int -> 'a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
+val fold_left2i : (int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b t -> 'c t -> 'a
+
+val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
+val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
+
+val exists : ('a -> bool) -> 'a t -> bool
+
+val for_all : ('a -> bool) -> 'a t -> bool
+val for_all2 : ('a -> 'b -> bool) -> 'a t -> 'b t -> bool
+
+(** {5 Purely functional version of [Array] operations} *)
+
+(** These functions are equivalent to the eponymous versions in [Array], but
+    they do not work in place. Instead, they generate a fresh copy. *)
+
+val set : 'a t -> int -> 'a -> 'a t
+val fill : 'a t -> int -> int -> 'a -> 'a t
+val blit : 'a t -> int -> 'a t -> int -> int -> 'a t
+
+(** {5 Immutable array specific operations}*)
+
+val empty : 'a t
+(** The empty array. *)
+
+val singleton : 'a -> 'a t
+(** The singleton array. *)
+
+val diff : 'a t -> (int * 'a) list -> 'a t
+(** [diff t [(i1, x1); ...; (in, xn)] create an array identical to [t] except on
+    indices [ik] that will contain [xk]. If the same index is present several
+    times on the diff, which value is chosen is undefined. *)
+
+val of_array : 'a array -> 'a t
+(** Create a new immutable array with the same elements as the argument. *)
+
+val to_array : 'a t -> 'a array
+(** Create a new mutable array with the same elements as the argument. *)
 
 (** {5 Unsafe operations} *)