Up  Next

Module Slap.Size

module Size: Slap_size
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
Since 4.0.0
Returns n - 1
type 'n p 
val pred_dyn : 'n t -> 'n p t
pred_dyn n
Since 0.2.0
Raises Invalid_arg if n <= 0.
Returns n - 1
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
Raises Invalid_argument 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
Raises Invalid_argument n is zero
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
See also Packed Storage (BLAS & LAPACK)
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
See also Band Storage (BLAS & LAPACK)
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.
Since 0.2.0
Raises Invalid_argument if m >= kl and n >= ku.
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
See also Band Storage (BLAS & LAPACK)
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.
Since 0.2.0
Raises Invalid_argument if kd >= n.
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
See also Band Storage (BLAS & LAPACK)
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.
Since 0.2.0
Raises Invalid_argument if m >= kl and n >= ku.

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 Slap_size.SIZE)
module N = (val of_int_dyn n : SIZE)
Raises Invalid_argument the given size is negative.
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 Slap_size.SIZE)
Like of_int_dyn, but dynamic size checking is not performed.
module Of_int_dyn: 
functor (N : sig


val value : int
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
Since 4.0.0
Raises Invalid_argument the given size is negative.
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.

Iterators on sizes

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

val fold_left : ('accum -> (module Slap_size.SIZE) -> 'accum) ->
       'accum -> 'n t -> 'accum
fold_left f init n is f (... (f (f init 1) 2) ...) n.
val fold_right : ((module Slap_size.SIZE) -> 'accum -> 'accum) ->
       'n t -> 'accum -> 'accum
fold_right f n init is f 1 (f 2 (... (f n init) ...)).
val iter : ((module Slap_size.SIZE) -> unit) -> 'n t -> unit
iter f n is f 1; f 2; ...; f n.
val riter : ((module Slap_size.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

Internal functions


val __expose : 'n t -> int
val __unexpose : int -> 'n t