diff --git a/src/kernel_services/analysis/filter/field.ml b/src/kernel_services/analysis/filter/field.ml index fd00c817945583bd242d9469739361e8bf396497..df7371741791a4f00d7aed11c33fa90fd0876740 100644 --- a/src/kernel_services/analysis/filter/field.ml +++ b/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 diff --git a/src/kernel_services/analysis/filter/linear.ml b/src/kernel_services/analysis/filter/linear.ml index 96010938400e0b31787bd8b24eae937feefae808..b3c1d6537cf4aa32a0c2c0d90eb0620d36199fee 100644 --- a/src/kernel_services/analysis/filter/linear.ml +++ b/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 diff --git a/src/kernel_services/analysis/filter/linear.mli b/src/kernel_services/analysis/filter/linear.mli index e2d69ed4ff90a1d11b4cd4df60d2f52700883638..8437815b75ab4ae223d14f01eae8334d18272356 100644 --- a/src/kernel_services/analysis/filter/linear.mli +++ b/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 diff --git a/src/kernel_services/analysis/filter/linear_filter.ml b/src/kernel_services/analysis/filter/linear_filter.ml index 977c7043350b166d31cf4dcb980284e341dadb10..da1722d5d25605e44be7396f81fadc2523a37308 100644 --- a/src/kernel_services/analysis/filter/linear_filter.ml +++ b/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 diff --git a/src/kernel_services/analysis/filter/linear_filter.mli b/src/kernel_services/analysis/filter/linear_filter.mli index c7e2b8f25b9f55725e52538e5544de2c3186d256..3170b118f2e22f94b6a6601725eeac3f3779a7f4 100644 --- a/src/kernel_services/analysis/filter/linear_filter.mli +++ b/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