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