diff options
| author | Enrico Tassi | 2015-01-06 18:38:20 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-01-06 18:38:20 +0100 |
| commit | a4001165f27a6ac0f4f76917037f154aa217f0d1 (patch) | |
| tree | b84b148cbe7d24760feda36fa6a690d005ed1a01 /lib/iArray.ml | |
| parent | 341909bbc5c1c59e81dfad2f2532602e2561ec36 (diff) | |
remove unused iArray
Diffstat (limited to 'lib/iArray.ml')
| -rw-r--r-- | lib/iArray.ml | 471 |
1 files changed, 0 insertions, 471 deletions
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 |
