remove unused iArray

3 files changed, 0 insertions, 569 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index 04c4f77572..2da81c959f 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -13,7 +13,6 @@ Option
 Store
 Exninfo
 Backtrace
-IArray
 IStream
 Pp_control
 Flags
diff --git a/lib/iArray.ml b/lib/iArray.ml
deleted file mode 100644
index 3cbee45b63..0000000000
--- a/lib/iArray.ml
+++ /dev/null
@@ -1,471 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-module type US =
-sig
-  type +'a t
-  (** We put it covariant even though it isn't, as we're going to use it purely
-      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 : 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_modify function,
-        otherwise that may result in strange GC behaviour.
-  *)
-
-  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
-
-  let get (obj : 'a t) i : 'a =
-    let obj : dummy array = Obj.magic obj in
-    let ans = Array.unsafe_get obj i in
-    Obj.magic ans
-
-  let set (obj : 'a t) i (x : 'a) =
-    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 M = ObjArray
-
-type +'a t = 'a M.t
-
-let length = M.length
-
-let get = M.safe_get
-
-(* let set t i x =
-  if i < 0 || M.length t <= i then
-    invalid_arg "Array.set"
-  else
-    M.set t i x *)
-
-let make len x =
-  let ans = M.create len in
-  let () =
-    for i = 0 to pred len do
-      M.set ans i x
-    done
-  in
-  ans
-
-let is_empty t = M.length t = 0
-
-(* let copy = M.copy *)
-
-let init len f =
-  let ans = M.create len in
-  let () =
-    for i = 0 to pred len do
-      M.set ans i (f i)
-    done
-  in
-  ans
-
-let append t1 t2 =
-  let len1 = M.length t1 in
-  let len2 = M.length t2 in
-  let ans = M.create (len1 + len2) in
-  let () =
-    for i = 0 to pred len1 do
-      M.set ans i (M.get t1 i)
-    done
-  in
-  let () =
-    for i = 0 to pred len2 do
-      M.set ans (len1 + i) (M.get t2 i)
-    done
-  in
-  ans
-
-let concat l =
-  let rec len accu = function
-  | [] -> accu
-  | t :: l -> len (M.length t + accu) l
-  in
-  let len = len 0 l in
-  let ans = M.create len in
-  let rec iter off = function
-  | [] -> ()
-  | t :: l ->
-    let len = M.length t in
-    let () =
-      for i = 0 to pred len do
-        M.set ans (off + i) (M.get t i)
-      done
-    in
-    iter (off + len) l
-  in
-  let () = iter 0 l in
-  ans
-
-let sub t off len =
-  let tlen = M.length t in
-  let () = if off < 0 || off + len > tlen then
-    invalid_arg "IArray.sub"
-  in
-  let ans = M.create len in
-  let () =
-    for i = 0 to len - 1 do
-      M.set ans i (M.get t (off + i))
-    done
-  in
-  ans
-
-let of_list l =
-  let len = List.length l in
-  let ans = M.create len in
-  let rec iter off = function
-  | [] -> ()
-  | x :: l ->
-    let () = M.set ans off x in
-    iter (succ off) l
-  in
-  let () = iter 0 l in
-  ans
-
-let to_list t =
-  let rec iter off accu =
-    if off < 0 then accu
-    else iter (pred off) (M.get t off :: accu)
-  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)
-  done
-
-let iteri f t =
-  for i = 0 to M.length t - 1 do
-    f i (M.get t i)
-  done
-
-(** MAPS *)
-
-let map f t =
-  let len = M.length t in
-  let ans = M.create len in
-  let () =
-    for i = 0 to pred len do
-      M.set ans i (f (M.get t i))
-    done
-  in
-  ans
-
-let mapi f t =
-  let len = M.length t in
-  let ans = M.create len in
-  let () =
-    for i = 0 to pred len do
-      M.set ans i (f i (M.get t i))
-    done
-  in
-  ans
-
-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 =
-    if len <= i then accu
-    else fold (succ i) (f accu (M.get t i))
-  in
-  fold 0 accu
-
-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) *)
-
-(* include M *)
-
-module Unsafe =
-struct
-
-let get = M.get
-
-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 "IArray.of_array"
-  in
-  Obj.magic t
-
-let to_array (t : 'a M.t) : 'a array =
-  if Obj.size (Obj.repr t) = 0 then [||]
-  else
-    let dummy = Obj.field (Obj.repr t) 0 in
-    let () = if Obj.tag dummy = Obj.double_tag then
-      invalid_arg "IArray.to_array"
-    in
-    Obj.magic t
-
-end
diff --git a/lib/iArray.mli b/lib/iArray.mli
deleted file mode 100644
index a3789845e3..0000000000
--- a/lib/iArray.mli
+++ /dev/null
@@ -1,97 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       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. *)
-
-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
-val sub : 'a t -> int -> int -> 'a t
-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 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} *)
-
-module Unsafe :
-sig
-  val get : 'a t -> int -> 'a
-  (** Get a value, does not do bound checking. *)
-
-  val of_array : 'a array -> 'a t
-  (** Cast a mutable array into an immutable one. Essentially identity. *)
-
-  val to_array : 'a t -> 'a array
-  (** Cast an immutable array into a mutable one. Essentially identity. *)
-end
-(** Unsafe operations. Use with caution! *)