ATSLIB/prelude/matrix

  • matrix
  • matrix_vt0ype_int_int_vt0ype
  • matrix_v
  • matrow_v
  • matcol_v
  • matrix2array_v
  • array2matrix_v
  • matrix_get_at
  • matrix_get_at_int
  • matrix_get_at_size
  • matrix_set_at
  • matrix_set_at_int
  • matrix_set_at_size
  • matrix_exch_at
  • matrix_exch_at_int
  • matrix_exch_at_size
  • matrix_ptr_takeout_elt
  • matrix_ptr_takeout_row
  • matrix_ptr_takeout_col
  • matrix_ptr_alloc
  • matrix_ptr_free
  • matrix_ptr_tabulate
  • matrix_tabulate$fopr
  • fprint_matrix
  • fprint_matrix_int
  • fprint_matrix_size
  • fprint_matrix$sep1
  • fprint_matrix$sep2
  • fprint_matrix_sep
  • matrix_foreach
  • matrix_foreach_env
  • matrix_foreach$fwork
  • matrix_foreachrow
  • matrix_foreachrow_env
  • matrix_foreachrow$fwork
  • matrix_initize
  • matrix_initize$init
  • matrix_mapto
  • matrix_mapto$fwork
  • matrix_map2to
  • matrix_map2to$fwork
  • Overloaded Symbols
  • []
  • fprint
    •

    matrix

    Synopsis

    stadef matrix = matrix_vt0ype_int_int_vt0ype

    matrix_vt0ype_int_int_vt0ype

    Synopsis

    absvt@ype
matrix_vt0ype_int_int_vt0ype
  (a:vt@ype+, row:int, col:int) = array(a, row*col)

    matrix_v

    Synopsis

    viewdef
matrix_v (
  a:viewt@ype+, l:addr, row:int, col:int
) = matrix (a, row, col) @ l

    matrow_v

    Synopsis

    stadef matrow_v = matrow_view

    matcol_v

    Synopsis

    stadef matcol_v = matcol_view

    matrix2array_v

    Synopsis

    praxi
matrix2array_v
  {a:vt0p}
  {l:addr}{m,n:int}
  (pf0: matrix_v(INV(a), l, m, n)): array_v (a, l, m*n)

    Description

    This proof function turns a proof of matrix-view into another proof of array-view.

    array2matrix_v

    Synopsis

    praxi
array2matrix_v
  {a:vt0p}
  {l:addr}{m,n:int}
(
  pf0:
  array_v(INV(a), l, m*n)
) : matrix_v (a, l, m(*nrow*), n(*ncol*))

    Description

    This proof function turns a proof of array-view into another proof of matrix-view.

    matrix_get_at

    Synopsis

    overload
matrix_get_at with matrix_get_at_int of 0
    overload
matrix_get_at with matrix_get_at_size of 0

    Description

    Note that the width (that is, number of columns) must be provided in order to access a matrix-cell.

    matrix_get_at_int

    Synopsis

    fun{a:t0p}
matrix_get_at_int
  {m,n:int}
(
  M: &RD(matrix(INV(a), m, n))
, i: natLt (m), n: int n, j: natLt (n)
) :<> (a) // end-of-function

    matrix_get_at_size

    Synopsis

    fun{a:t0p}
matrix_get_at_size
  {m,n:int}
(
  M: &RD(matrix(INV(a), m, n))
, i: sizeLt (m), n: size_t n, j: sizeLt(n)
) :<> (a) // endfun

    matrix_set_at

    Synopsis

    overload
matrix_set_at with matrix_set_at_int of 0
    overload
matrix_set_at with matrix_set_at_size of 0

    Description

    Note that the width (that is, number of columns) must be provided in order to access a matrix-cell.

    matrix_set_at_int

    Synopsis

    fun{a:t0p}
matrix_set_at_int
  {m,n:int}
(
  M: &matrix(INV(a), m, n)
, i: natLt (m), n: int n, j: natLt (n), x: a
) :<!wrt> void // end-of-function

    matrix_set_at_size

    Synopsis

    fun{a:t0p}
matrix_set_at_size
  {m,n:int}
(
  M: &matrix(INV(a), m, n)
, i: sizeLt (m), n: size_t n, j: sizeLt (n), x: a
) :<!wrt> void // end-of-function

    matrix_exch_at

    Synopsis

    overload matrix_exch_at with matrix_exch_at_int
    overload matrix_exch_at with matrix_exch_at_size

    Description

    Note that the width (that is, number of columns) must be provided in order to access a matrix-cell.

    matrix_exch_at_int

    Synopsis

    fun{a:vt0p}
matrix_exch_at_int
  {m,n:int}
(
  M: &matrix(INV(a), m, n)
, i: natLt (m), n: int n, j: natLt (n), x: &a>>a
) :<!wrt> void // endfun

    matrix_exch_at_size

    Synopsis

    fun{a:vt0p}
matrix_exch_at_size
  {m,n:int}
(
  M: &matrix(INV(a), m, n)
, i: sizeLt (m), n: size_t n, j: sizeLt (n), x: &a>>a
) :<!wrt> void // endfun

    matrix_ptr_takeout_elt

    Synopsis

    fun{a:vt0p}
matrix_ptr_takeout_elt
  {l0:addr}
  {m,n:int}
  {i,j:nat | i < m; j < n}
(
  pfm: matrix_v(INV(a), l0, m, n)
| base: ptr(l0)
, i: size_t(i), n: size_t(n), j: size_t(j)
) :<>
[l:addr]
(
  a @ l
, a @ l -<lin,prf> matrix_v (a, l0, m, n)
| ptr (l)
) (* end of [matrix_ptr_takeout_elt] *)

    matrix_ptr_takeout_row

    Synopsis

    fun{a:vt0p}
matrix_ptr_takeout_row
  {l0:addr}
  {m,n:int}
  {i:int | i < m}
(
  pfm: matrix_v(INV(a), l0, m, n)
| base: ptr(l0), i: size_t(i), n: size_t(n)
) :<>
[l:addr]
(
  matrow_v(a, l, m, n)
, matrow_v(a, l, m, n) -<lin,prf> matrix_v(a, l0, m, n)
| ptr (l)
) (* end of [matrix_ptr_takeout_row] *)

    matrix_ptr_takeout_col

    Synopsis

    fun{a:vt0p}
matrix_ptr_takeout_col
  {l0:addr}
  {m,n:int}
  {i:int | i < m}
(
  pfm: matrix_v(INV(a), l0, m, n)
| base: ptr l0, i: size_t(i), n: size_t(n)
) :<>
[l:addr]
(
  matcol_v(a, l, m, n)
, matcol_v(a, l, m, n) -<lin,prf> matrix_v(a, l0, m, n)
| ptr (l)
) (* end of [matrix_ptr_takeout_col] *)

    matrix_ptr_alloc

    Synopsis

    fun{a:vt0p}
matrix_ptr_alloc
  {m,n:int}
(
  row: size_t m, col: size_t n
) :<!wrt> [l:agz]
(
  matrix_v(a?, l, m, n), mfree_gc_v (l) | ptr l
) // end of [matrix_ptr_alloc]

    Description

    This function calls malloc_gc to allocate memory for storing a matrix of the given dimension. Note that the second returned proof needs to be present in order to free the allocated memory.

    matrix_ptr_free

    Synopsis

    fun{}
matrix_ptr_free
  {a:vt0p}{l:addr}{m,n:int}
(
  matrix_v(a?, l, m, n), mfree_gc_v l | ptr l
) :<!wrt> void // end of [matrix_ptr_free]

    Description

    This function frees the memory of a matrix. Note that both a proof of the view of the matrix and a proof of the free-view of the memory need to be present.

    matrix_ptr_tabulate

    Synopsis

    fun{a:vt0p}
matrix_ptr_tabulate
  {m,n:int}
(
  nrow: size_t m, ncol: size_t n
) : [l:addr]
(
  matrix_v (a, l, m, n), mfree_gc_v (l) | ptr(l)
) (* end of [matrixptr_tabulate] *)

    Description

    This function creates a matrix of a given dimension. For each valid index-pair (i, j), the content of matrix-cell (i, j) is initialized by the return value of a call to matrix_tabulate$fopr.

    matrix_tabulate$fopr

    Synopsis

    fun{a:vt0p}
matrix_tabulate$fopr
  (i: size_t, j: size_t): (a)

    fprint_matrix

    Synopsis

    overload fprint_matrix with fprint_matrix_int
    overload fprint_matrix with fprint_matrix_size

    fprint_matrix_int

    Synopsis

    fun{a:vt0p}
fprint_matrix_int
  {m,n:int}
(
  out: FILEref
, mat: &matrix(INV(a), m, n), m: int(m), n: int(n)
) : void // end of [fprint_matrix_int]

    fprint_matrix_size

    Synopsis

    fun{a:vt0p}
fprint_matrix_size
  {m,n:int}
(
  out: FILEref
, mat: &matrix(INV(a), m, n), m: size_t(m), n: size_t(n)
) : void // end of [fprint_matrix_size]

    fprint_matrix$sep1

    Synopsis

    fun{}
fprint_matrix$sep1(out: FILEref): void // col sep

    fprint_matrix$sep2

    Synopsis

    fun{}
fprint_matrix$sep2(out: FILEref): void // row sep

    fprint_matrix_sep

    Synopsis

    fun{a:vt0p}
fprint_matrix_sep
  {m,n:int}
(
  out: FILEref
, M: &matrix(INV(a), m, n)
, m: size_t(m), n: size_t(n)
, sep1: NSH(string), sep2: NSH(string)
) : void // end of [fprint_matrix_sep]

    matrix_foreach

    Synopsis

    fun{
a:vt0p
} matrix_foreach{m,n:int}
(
  M: &matrix(INV(a), m, n) >> _, size_t(m), size_t(n)
) : void // end of [matrix_foreach]

    matrix_foreach_env

    Synopsis

    fun{
a:vt0p}{env:vt0p
} matrix_foreach_env{m,n:int}
(
  M: &matrix(INV(a), m, n) >> _, size_t(m), size_t(n), env: &(env) >> _
) : void // end of [matrix_foreach_env]

    matrix_foreach$fwork

    Synopsis

    fun{
a:vt0p}{env:vt0p
} matrix_foreach$fwork
  (x: &a >> _, env: &(env) >> _): void

    matrix_foreachrow

    Synopsis

    fun{
a:vt0p
} matrix_foreachrow{m,n:int}
(
  M: &matrix(INV(a), m, n) >> _, m: size_t(m), n: size_t(n)
) : void // end of [matrix_foreachrow]

    matrix_foreachrow_env

    Synopsis

    fun{
a:vt0p}{env:vt0p
} matrix_foreachrow_env{m,n:int}
(
  M: &matrix(INV(a), m, n) >> _, m: size_t(m), n: size_t(n), env: &(env) >> _
) : void // end of [matrix_foreachrow_env]

    matrix_foreachrow$fwork

    Synopsis

    fun{
a:vt0p}{env:vt0p
} matrix_foreachrow$fwork
  {n:int}
(
  A: &array(INV(a), n) >> _, n: size_t(n), env: &(env) >> _
) : void // end of [matrix_foreachrow$fwork]

    matrix_initize

    Synopsis

    fun{a:vt0p}
matrix_initize{m,n:int}
(
  M: &matrix(a?, m, n) >> matrix(a, m, n), m: size_t(m), n: size_t(n)
) : void // end of [matrix_initize]

    matrix_initize$init

    Synopsis

    fun{a:vt0p}
matrix_initize$init
  (i: size_t, j: size_t, x: &a? >> a): void

    matrix_mapto

    Synopsis

    fun
{a:vt0p}
{b:vt0p}
matrix_mapto
  {m,n:int}
(
  A: &matrix(INV(a), m, n)
, B: &matrix(b?, m, n) >> matrix(b, m, n)
, m: size_t m, n: size_t n
) : void // end of [matrix_mapto]

    matrix_mapto$fwork

    Synopsis

    fun
{a:vt0p}
{b:vt0p}
matrix_mapto$fwork
  (x: &a, y: &b? >> b): void

    matrix_map2to

    Synopsis

    fun
{a,b:vt0p}
{c:vt0p}
matrix_map2to
  {m,n:int}
(
  A: &matrix(INV(a), m, n)
, B: &matrix(INV(b),  m, n)
, C: &matrix(c?, m, n) >> matrix(c, m, n)
, m: size_t m, n: size_t n
) : void // end of [matrix_map2to]

    matrix_map2to$fwork

    Synopsis

    fun
{a,b:vt0p}
{c:vt0p}
matrix_map2to$fwork
  (x: &a, y: &b, z: &c? >> c): void

    Overloaded Symbols

    []

    Synopsis

    overload [] with matrix_get_at_int
    overload [] with matrix_get_at_size
    overload [] with matrix_set_at_int
    overload [] with matrix_set_at_size

    fprint

    Synopsis

    Synopsis for [fprint] is unavailable.
    This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. SourceForge.net Logo