aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/iArray.ml230
-rw-r--r--lib/iArray.mli46
3 files changed, 277 insertions, 0 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 83cad296d..9667df31c 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -3,6 +3,7 @@ Option
Store
Exninfo
Backtrace
+IArray
Pp_control
Pp
Coq_config
diff --git a/lib/iArray.ml b/lib/iArray.ml
new file mode 100644
index 000000000..59ce6fb9c
--- /dev/null
+++ b/lib/iArray.ml
@@ -0,0 +1,230 @@
+(***********************************************************************)
+(* 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
+ functionnaly. *)
+ 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
+end
+(** Minimal signature of unsafe arrays *)
+
+module ObjArray =
+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,
+ otherwise that may result in strange GC behaviour.
+ *)
+
+ let length = Obj.size
+ 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
+end
+
+module Make(M : US) =
+struct
+
+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 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 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 "Array.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) []
+
+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
+
+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 fold_right f accu t =
+ 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_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
+
+end
+
+module M = Make(ObjArray)
+
+include M
+
+module Unsafe =
+struct
+
+let get = ObjArray.get
+
+let set = ObjArray.set
+
+let of_array (t : 'a array) : 'a ObjArray.t =
+ let tag = Obj.tag (Obj.repr t) in
+ let () = if tag = Obj.double_array_tag then
+ invalid_arg "Array.of_array"
+ in
+ Obj.magic t
+
+let to_array (t : 'a ObjArray.t) : 'a array =
+ if Obj.size t = 0 then [||]
+ else
+ let dummy = Obj.field t 0 in
+ let () = if Obj.tag dummy = Obj.double_tag then
+ invalid_arg "Array.to_array"
+ in
+ Obj.magic t
+
+end
diff --git a/lib/iArray.mli b/lib/iArray.mli
new file mode 100644
index 000000000..911de4062
--- /dev/null
+++ b/lib/iArray.mli
@@ -0,0 +1,46 @@
+(***********************************************************************)
+(* 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 *)
+(***********************************************************************)
+
+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 length : 'a t -> int
+val make : int -> 'a -> 'a t
+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 fold_right : ('a -> 'b -> 'b) -> 'b -> 'a t -> 'b
+val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b t -> 'a
+
+(** {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! *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 04:03:39 +0000