Frama-C:
Plug-ins:
Libraries:

Frama-C API - Matrix

val pretty : Stdlib.Format.formatter -> ('n, 'm) matrix -> unit
val id : 'n Nat.succ Nat.nat -> ('n Nat.succ, 'n Nat.succ) matrix

The call id n returns the identity matrix in 𝕂ⁿˣⁿ.

val zero : 'n Nat.succ Nat.nat -> 'm Nat.succ Nat.nat -> ('n Nat.succ, 'm Nat.succ) matrix

The call zero n m returns the 0 matrix in 𝕂ⁿˣᵐ.

val shift : 'n Nat.succ Nat.nat -> ('n Nat.succ, 'n Nat.succ) matrix

The call shift n returns a square matrix in 𝕂ⁿˣⁿ such as the first row and the last column is all zero, and the remaining is the identity.

val get : 'n Finite.finite -> 'm Finite.finite -> ('n, 'm) matrix -> scalar

The call get i j m returns the coefficient of the i-th row and the j-th column.

val set : 'n Finite.finite -> 'm Finite.finite -> scalar -> ('n, 'm) matrix -> ('n, 'm) matrix

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 norm_inf : ('n, 'm) matrix -> scalar

The call norm_inf m computes the ∞-norm of m, i.e the maximum of the absolute sums of the rows of m.

val norm_one : ('n, 'm) matrix -> scalar

The call norm_one m computes the 1-norm of m, i.e the maximum of the absolute sums of the columns of m.

val transpose : ('n, 'm) matrix -> ('m, 'n) matrix

The call transpose m for m in 𝕂ⁿˣᵐ returns a new matrix in 𝕂ᵐˣⁿ with all the coefficients transposed.

val dimensions : ('m, 'n) matrix -> 'm Nat.nat * 'n Nat.nat

The call dimensions m for m in 𝕂ⁿˣᵐ returns the pair (n, m).

val (+) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix

Matrices addition. The dimensions compatibility is statically ensured.

val (-) : ('n, 'm) matrix -> ('n, 'm) matrix -> ('n, 'm) matrix

Matrices substraction. As for the addition, the dimensions compatibility is statically ensured.

val (*) : ('n, 'm) matrix -> ('m, 'p) matrix -> ('n, 'p) matrix

Matrices multiplication. The dimensions compatibility is statically ensured.

val (**) : scalar -> ('n, 'm) matrix -> ('n, 'm) matrix

Scalar multiplication.

val power : ('n, 'n) matrix -> int -> ('n, 'n) matrix

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 inverse : ('n, 'n) matrix -> ('n, 'n) matrix option

Matrix inverse. Returns None if the input matrix is singular.

val abs : ('n, 'm) matrix -> ('n, 'm) matrix

The call abs m returns a matrix for which each coordinate is the absolute value of the corresponding coordinate of m.