[Kernel] Linear filter: removes modules Types.

src/kernel_services/analysis/filter/field.ml

@@ -22,9 +22,8 @@
 
 module type S = sig
 
-  module Types : sig type scalar end
-  include Datatype.S_with_collections with type t = Types.scalar
-  open Types
+  type scalar
+  include Datatype.S_with_collections with type t = scalar
 
   val zero     : scalar
   val one      : scalar

src/kernel_services/analysis/filter/linear.ml

@@ -27,15 +27,11 @@ open Finite.Types
 
 module Space (Field : Field.S) = struct
 
-  open Field.Types
+  type scalar = Field.scalar
 
-  module Types = struct
-    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
-
-  open Types
+  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
 
 
 

src/kernel_services/analysis/filter/linear.mli

@@ -27,14 +27,9 @@ open Finite.Types
 
 module Space (Field : Field.S) : sig
 
-  open Field.Types
-
-  module Types : sig
-    type ('n, 'm) matrix
-    type 'n vector = ('n, zero succ) matrix
-  end
-
-  open Types
+  type scalar = Field.scalar
+  type ('n, 'm) matrix
+  type 'n vector = ('n, zero succ) matrix
 
   module Vector : sig
     val pretty : Format.formatter -> 'n vector -> unit

src/kernel_services/analysis/filter/linear_filter.ml

@@ -27,8 +27,6 @@ open Nat.Types
 module Make (Field : Field.S) = struct
 
   module Linear = Linear.Space (Field)
-  open Linear.Types
-  open Field.Types
   open Linear
 
 
@@ -58,20 +56,14 @@ module Make (Field : Field.S) = struct
 
 
 
-  module Types = struct
+  type ('n, 'm) filter =
+    | Filter : ('n succ, 'm succ) data -> ('n succ, 'm succ) filter
 
-    type ('n, 'm) filter =
-      | Filter : ('n succ, 'm succ) data -> ('n succ, 'm succ) filter
-
-    and ('n, 'm) data =
-      { state : ('n, 'n) matrix
-      ; input : ('n, 'm) matrix
-      ; measure : 'm vector
-      }
-
-  end
-
-  open Types
+  and ('n, 'm) data =
+    { state : ('n, 'n) matrix
+    ; input : ('n, 'm) matrix
+    ; measure : 'm vector
+    }
 
 
 
@@ -88,7 +80,7 @@ module Make (Field : Field.S) = struct
     let rec aux (m, r) i = if i >= 0 then aux (p m, r + m) (i - 1) else r in
     aux (Matrix.id order, Field.zero) (stop - 1)
 
-  type ('n, 'm) invariant = ('n, 'm) filter -> int -> scalar option
+  type ('n, 'm) invariant = ('n, 'm) filter -> int -> Field.scalar option
   let invariant : type n m. (n, m) invariant = fun (Filter f) max ->
     let open Option.Operators in
     let order, _ = Matrix.dimensions f.input in

src/kernel_services/analysis/filter/linear_filter.mli

@@ -25,18 +25,15 @@ open Nat.Types
 module Make (Field : Field.S) : sig
 
   module Linear : module type of Linear.Space (Field)
-  open Linear.Types
-  open Field.Types
 
   (* A value of type [(n, m) filter] describes a linear filter of order n (i.e
      with n state variables) and with m inputs. *)
-  module Types : sig type ('n, 'm) filter end
-  open Types
+  type ('n, 'm) filter
 
   val create :
-    ('n succ, 'n succ) matrix ->
-    ('n succ, 'm succ) matrix ->
-    'm succ vector -> ('n succ, 'm succ) filter
+    ('n succ, 'n succ) Linear.matrix ->
+    ('n succ, 'm succ) Linear.matrix ->
+    'm succ Linear.vector -> ('n succ, 'm succ) filter
 
   val pretty : Format.formatter -> ('n, 'm) filter -> unit
 
@@ -52,6 +49,6 @@ module Make (Field : Field.S) : sig
      filters, a depth of 200 will gives an exact upper bound up to at least ten
      digits, which is more than enough. Moreover, for those simple filters, the
      computation is immediate, even when using rational numbers. *)
-  val invariant : ('n, 'm) filter -> int -> scalar option
+  val invariant : ('n, 'm) filter -> int -> Field.scalar option
 
 end