[Kernel] Persistent array: exports type 'a t instead of 'a array.

Avoids overloading stdlib types.

src/kernel_services/analysis/filter/linear.ml

@@ -22,7 +22,6 @@
 
 open Nat.Types
 open Finite.Types
-open Parray.Types
 
 
 
@@ -31,7 +30,7 @@ module Space (Field : Field.S) = struct
   open Field.Types
 
   module Types = struct
-    type ('n, 'm) m = { data : scalar array ; rows : 'n nat ; cols : 'm nat }
+    type ('n, 'm) m = { data : scalar Parray.t ; rows : 'n nat ; cols : 'm nat }
     type ('n, 'm) matrix = M : ('n succ, 'm succ) m -> ('n succ, 'm succ) matrix
     type 'n vector = ('n, zero succ) matrix
   end

src/libraries/utils/parray.ml

@@ -20,13 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Types = struct
-  type 'a memory = 'a Array.t
-  type 'a array = 'a data ref
-  and 'a data = Memory of 'a memory | Diff of int * 'a * 'a array
-end
-
-open Types
+type 'a t = 'a data ref
+and 'a data = Memory of 'a array | Diff of int * 'a * 'a t
 
 let init n f = ref (Memory (Array.init n f))
 

src/libraries/utils/parray.mli

@@ -24,19 +24,15 @@
    Sylvain Conchon and Jean-Chistophe Filliâtre. For further details, see
    https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf *)
 
-module Types : sig
-  type 'a array
-end
+type 'a t
 
-open Types
-
-val init : int -> (int -> 'a) -> 'a array
-val get  : 'a array -> int -> 'a
-val set  : 'a array -> int -> 'a -> 'a array
-val fold : (int -> 'a -> 'b -> 'b) -> 'a array -> 'b -> 'b
-val map  : ('a -> 'a) -> 'a array -> 'a array
+val init : int -> (int -> 'a) -> 'a t
+val get  : 'a t -> int -> 'a
+val set  : 'a t -> int -> 'a -> 'a t
+val fold : (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+val map  : ('a -> 'a) -> 'a t -> 'a t
 
 val pretty :
   ?pp_sep : (Format.formatter -> unit -> unit) ->
   (Format.formatter -> 'a -> unit) ->
-  Format.formatter -> 'a array -> unit
+  Format.formatter -> 'a t -> unit