Module Slap_size

Slap.Size contains operations on sizes (the dimensions of vectors and matrices).

type +'n t = private int

A singleton type on sizes (i.e., dimensions of vectors and matrices).

Evaluation of a term with singleton type 'n size always results in the natural number corresponding to phantom type parameter 'n. 'n is instantiated to a generative phantom type or a (phantom) type that represents an arithmetic operation defined in this module. In either case, only the equality of sizes is verified statically.

Constants

type z

zero

type 'n s

successor, i.e., 'n s corresponds to 'n + 1.

val zero : z t
type one = z s
val one : one t
type two = z s s
val two : two t
type three = z s s s
val three : three t
type four = z s s s s
val four : four t
type five = z s s s s s
val five : five t
type six = z s s s s s s
val six : six t
type seven = z s s s s s s s
val seven : seven t
type eight = z s s s s s s s s
val eight : eight t
type nine = z s s s s s s s s s
val nine : nine t
type ten = z s s s s s s s s s s
val ten : ten t

Arithmetic operations

val succ : 'n t -> 'n s t

succ n

  • returns

    n + 1

type 'n p
val pred_dyn : 'n t -> 'n p t

pred_dyn n

  • returns

    n - 1

  • raises Invalid_arg

    if n <= 0.

  • since 0.2.0
type ('m, 'n) add
val add : 'm t -> 'n t -> ('m, 'n) add t

add m n

  • returns

    m + n

type ('m, 'n) sub
val sub_dyn : 'm t -> 'n t -> ('m, 'n) sub t

sub_dyn m n

  • returns

    m - n

type ('m, 'n) mul
val mul : 'm t -> 'n t -> ('m, 'n) mul t

mul m n

  • returns

    the product of m and n

type ('m, 'n) div
val div_dyn : 'm t -> 'n t -> ('m, 'n) div t

div_dyn m n

  • returns

    m / n

type ('m, 'n) min
val min : 'm t -> 'n t -> ('m, 'n) min t

min m n

  • returns

    the minimum of m and n

type ('m, 'n) max
val max : 'm t -> 'n t -> ('m, 'n) max t

max m n

  • returns

    the maximum of m and n

Storage sizes for BLAS and LAPACK

type 'n packed

Type 'n packed corresponds to the packed storage size of a n-by-n matrix.

  • since 0.2.0
val packed : 'n t -> 'n packed t

packed n computes the packed storage size of a n-by-n matrix.

  • since 0.2.0
val unpacked : 'n packed t -> 'n t

unpacked n computes the inverse of the packed storage size, i.e., unpacked (packed n) = n for all n.

  • since 0.2.0
type ('m, 'n, 'kl, 'ku) geband

('m, 'n, 'kl, 'ku) geband represents band storage size: A 'm-by-'n band matrix with 'kl subdiagonals and 'ku superdiagonals is stored in a ('kl+'ku+1)-by-'n matrix where 'kl, 'ku << min('m, 'n). ('m, 'n, 'kl, 'ku) geband corresponds to the number of columns of a band-storage-format matrix for such a band matrix.

  • since 0.2.0
val geband_dyn : 'm t -> 'n t -> 'kl t -> 'ku t -> ('m, 'n, 'kl, 'ku) geband t

geband_dyn m n kl ku computs the band storage size of m-by-n band matrices with kl subdiagonals and ku superdiagonals.

  • parameter m

    the number of rows

  • parameter n

    the number of columns

  • parameter kl

    the number of subdiagonals

  • parameter ku

    the number of superdiagonals

  • since 0.2.0
type ('n, 'kd) syband

('n, 'kd) syband represents symmetric or Hermitian band storage size: A n-by-n symmetric or Hermitian band matrix with kd superdiagonals or subdiagonals is stored in a (kd+1)-by-n matrix where kd << n. ('n, 'kd) syband corresponds to the number of columns of a band-storage-format matrix for such a symmetric band matrix.

  • since 0.2.0
val syband_dyn : 'n t -> 'kd t -> ('n, 'kd) syband t

syband_dyn n kd computs the band storage size of symmetric or Hermitian band matrices with kd superdiagonals or subdiagonals.

  • parameter n

    the number of rows or columns

  • parameter kd

    the number of superdiagonals or subdiagonals

  • since 0.2.0
type ('m, 'n, 'kl, 'ku) luband = ('m, 'n, 'kl, ('kl, 'ku) add) geband

('m, 'n, 'kl, 'ku) luband represents band storage size for LU factorization: A 'm-by-'n band matrix with 'kl subdiagonals and 'ku superdiagonals for LU factorization is stored in band storage format with 'kl+'ku superdiagonals.

  • since 0.2.0
val luband_dyn : 'm t -> 'n t -> 'kl t -> 'ku t -> ('m, 'n, 'kl, 'ku) luband t

luband_dyn m n kl ku computs the band storage size for LU factorization of m-by-n band matrices with kl subdiagonals and ku superdiagonals.

  • parameter m

    the number of rows

  • parameter n

    the number of columns

  • parameter kl

    the number of subdiagonals

  • parameter ku

    the number of superdiagonals

  • since 0.2.0

Conversion between a size and an integer

module type SIZE = sig ... end

The signature of modules as packages of types like exists n. n Size.t.

val to_int : 'n t -> int

Return the integer correponding to the given size.

val of_int_dyn : int -> (module SIZE)

module N = (val of_int_dyn n : SIZE)

  • returns

    module N containing the size N.value (= n) that has the type N.n Size.t with a generative phantom type N.n as a package of an existential quantified sized type like exists n. n Size.t.

val unsafe_of_int : int -> (module SIZE)

Like of_int_dyn, but dynamic size checking is not performed.

module Of_int_dyn (N : sig ... end) : SIZE

A functor version of of_int_dyn.

Iterators on sizes

The following functions are iterators over [1; 2; ...; n] where n is a size.

val fold_left : ('accum -> (module SIZE) -> 'accum) -> 'accum -> 'n t -> 'accum

fold_left f init n is f (... (f (f init 1) 2) ...) n.

val fold_right : ((module SIZE) -> 'accum -> 'accum) -> 'n t -> 'accum -> 'accum

fold_right f n init is f 1 (f 2 (... (f n init) ...)).

val iter : ((module SIZE) -> unit) -> 'n t -> unit

iter f n is f 1; f 2; ...; f n.

val riter : ((module SIZE) -> unit) -> 'n t -> unit

riter f n is f n; ...; f 2; f 1.

Iterators on integers

The following functions are iterators over [1; 2; ...; to_int n] where n is a size.

val fold_lefti : ('accum -> int -> 'accum) -> 'accum -> 'n t -> 'accum

fold_lefti f init n is f (... (f (f init 1) 2) ...) (to_int n).

val fold_righti : (int -> 'accum -> 'accum) -> 'n t -> 'accum -> 'accum

fold_righti f n init is f 1 (f 2 (... (f (to_int n) init) ...)).

val iteri : (int -> unit) -> 'n t -> unit

iteri f n is f 1; f 2; ...; f (to_int n).

val riteri : (int -> unit) -> 'n t -> unit

riteri f n is f (to_int n); ...; f 2; f 1.

Checking

val iszero : 'n t -> bool

iszero n returns true if size n is zero.

  • since 1.0.0
val nonzero : 'n t -> bool

nonzero n returns true if size n is not zero.

  • since 1.0.0