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

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

pred n returns

returns
n - 1

since 4.0.0

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

raises Invalid_argument
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

raises Invalid_argument
n is zero

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.

see http://www.netlib.org/lapack/lug/node123.html
Packed Storage (BLAS & LAPACK)

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.

see http://www.netlib.org/lapack/lug/node124.html
Band Storage (BLAS & LAPACK)

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

raises Invalid_argument
if m >= kl and n >= ku.

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.

see http://www.netlib.org/lapack/lug/node124.html
Band Storage (BLAS & LAPACK)

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

raises Invalid_argument
if kd >= n.

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.

see http://www.netlib.org/lapack/lug/node124.html
Band Storage (BLAS & LAPACK)

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

raises Invalid_argument
if m >= kl and n >= ku.

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.

raises Invalid_argument
the given size is negative.

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.

type dyn =

| SIZE : 'n t -> dyn

The type of packages of existential quantified sized type: dyn = exists n. n Size.t.

since 4.0.0

val of_int_c_dyn : int -> dyn

let SIZE n = of_int_c_dyn i

returns
a constructor SIZE that has the size n (= i) that has the existential quantified sized type exists n. n Size.t. "c" of of_int_c_dyn means a "c"onstructor of GADT. This function is available in OCaml 4.00 or above.

raises Invalid_argument
the given size is negative.

since 4.0.0

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

package slap

Module Slap_size