From b8b74087046dfff57c8fdb83a6feded3041f8b70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 30 Jan 2024 15:33:13 +0100
Subject: [PATCH] [Kernel] Linear filter: removes modules Types.
---
src/kernel_services/analysis/filter/field.ml | 5 ++--
src/kernel_services/analysis/filter/linear.ml | 12 ++++------
.../analysis/filter/linear.mli | 11 +++------
.../analysis/filter/linear_filter.ml | 24 +++++++------------
.../analysis/filter/linear_filter.mli | 13 ++++------
5 files changed, 22 insertions(+), 43 deletions(-)
diff --git a/src/kernel_services/analysis/filter/field.ml b/src/kernel_services/analysis/filter/field.ml
index fd00c817945..df737174179 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 96010938400..b3c1d6537cf 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 e2d69ed4ff9..8437815b75a 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 977c7043350..da1722d5d25 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 c7e2b8f25b9..3170b118f2e 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
--
GitLab