[Kernel] Documentations for Linear, Finite and Nat.

src/kernel_services/analysis/filter/finite.mli

@@ -22,6 +22,11 @@
 
 open Nat
 
+
+
+(* The type [n finite] encodes all finite sets of cardinal [n]. It is used by
+   the module Linear to represent accesses to vectors and matrices coefficients,
+   statically ensuring that no out of bounds access can be performed. *)
 type 'n finite
 
 val first : 'n succ finite

src/kernel_services/analysis/filter/linear.mli

@@ -25,35 +25,98 @@ open Finite
 
 
 
+(* Definition of a linear space over a field. Used by Linear_filter to represent
+   and compute linear filters invariants. *)
+
 module Space (Field : Field.S) : sig
 
+  (* The type of scalars in the field 𝕂. *)
   type scalar = Field.scalar
+
+  (* The type of matrices in 𝕂ⁿˣᵐ *)
   type ('n, 'm) matrix
+
+  (* Type representing a column vector of 𝕂ⁿ. One can use [transpose] if one
+     needs a row vector, for example when printing it. *)
   type 'n vector = ('n, zero succ) matrix
 
+
+
   module Vector : sig
+
     val pretty : Format.formatter -> 'n vector -> unit
+
+    (* The call [zero n] returns the 0 vector in 𝕂ⁿ. *)
     val zero   : 'n succ nat -> 'n succ vector
-    val base   : 'n succ finite -> 'n succ nat -> 'n succ vector
+
+    (* The call [repeat x n] returns a vector in 𝕂ⁿ which each dimension
+       containing the scalar x. *)
     val repeat : scalar -> 'n succ nat -> 'n succ vector
+
+    (* The call [base i n] returns the i-th base vector in the orthonormal space
+       of 𝕂ⁿ. In other words, the returned vector contains zero except for the
+       i-th coordinate, which contains one. *)
+    val base   : 'n succ finite -> 'n succ nat -> 'n succ vector
+
+    (* The call [set i x v] returns a new vector of the same linear space as
+       [v], and with the same coordinates, except for the i-th one, which is
+       set to the scalar [x]. *)
     val set    : 'n finite -> scalar -> 'n vector -> 'n vector
+
+    (* The call [size v] for [v] a vector of 𝕂ⁿ returns n. *)
     val size   : 'n vector -> 'n nat
+
+    (* The call [norm v] computes the ∞-norm of [v], i.e the maximum of the
+       absolute values of its coordinates. *)
     val norm   : 'n vector -> scalar
+
   end
 
+
+
   module Matrix : sig
+
     val pretty : Format.formatter -> ('n, 'm) matrix -> unit
+
+    (* The call [id n] returns the identity matrix in 𝕂ⁿˣⁿ. *)
     val id : 'n succ nat -> ('n succ, 'n succ) matrix
+
+    (* The call [zero n m] returns the 0 matrix in 𝕂ⁿˣᵐ. *)
     val zero : 'n succ nat -> 'm succ nat -> ('n succ, 'm succ) matrix
+
+    (* The call [get i j m] returns the coefficient of the i-th row and
+       the j-th column. *)
     val get : 'n finite -> 'm finite -> ('n, 'm) matrix -> scalar
+
+    (* The call [set i j x m] returns a new matrix of the same linear space as
+       [m], and with the same coefficients, except for the one of the i-th row
+       and the j-th column, which is set to the scalar [x]. *)
     val set : 'n finite -> 'm finite -> scalar -> ('n, 'm) matrix -> ('n, 'm) matrix
+
+    (* The call [norm m] computes the ∞-norm of [m], i.e the maximum of the
+       absolute sums of the rows of [m]. *)
     val norm : ('n, 'm) matrix -> scalar
+
+    (* The call [transpose m] for m in 𝕂ⁿˣᵐ returns a new matrix in 𝕂ᵐˣⁿ with
+       all the coefficients transposed. *)
     val transpose : ('n, 'm) matrix -> ('m, 'n) matrix
+
+    (* The call [dimensions m] for m in 𝕂ⁿˣᵐ returns the pair (n, m). *)
     val dimensions : ('m, 'n) matrix -> 'm nat * 'n nat
+
+    (* Matrices addition. The dimensions compatibility is statically ensured. *)
     val ( + ) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix
+
+    (* Matrices multiplication. The dimensions compatibility is statically
+       ensured. *)
     val ( * ) : ('n, 'm) matrix -> ('m, 'p) matrix -> ('n, 'p) matrix
-    (* Memoized, instantiate first on a matrix and then use it *)
+
+    (* Matrix exponentiation. The call [power m] returns a memoized function.
+       When one needs to compute several exponentiations of the same matrix, one
+       should perform the call [power m] once and used the returned function
+       each times one needs it. *)
     val power : ('n, 'n) matrix -> (int -> ('n, 'n) matrix)
+
   end
 
 end

src/kernel_services/analysis/filter/nat.mli

@@ -20,6 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* Encoding of the Peano arithmetic in OCaml type system. A value of type
+   [n nat] contains [n] at the value and the type level, allowing to express
+   properties on objects sizes and accesses for example. It is used by the
+   module Linear to represent vectors and matrices dimensions. *)
 type zero = |
 type 'n succ = |
 type 'n nat