ATSLIB/prelude/matrixptr

This package contains some common functions for creating/freeing and manipulating linear matrixptr-values, which are just pointers to matrices without dimension information attached.

matrixptr

Synopsis

stadef
matrixptr = matrixptr_vt0ype_addr_int_int_vtype

vtypedef
matrixptr
  (a:vt@ype, m: int, n: int) = [l:addr] matrixptr(a, l, m, n)

matrixptr_vt0ype_addr_int_int_vtype

Synopsis

absvtype
matrixptr_vt0ype_addr_int_int_vtype
  (a:vt@ype+, l: addr, m: int, n: int) = ptr

lemma_matrixptr_param

Synopsis

praxi
lemma_matrixptr_param{a:vt0p}
  {l:addr}{m,n:int} (A: !matrixptr(a, l, m, n)): [m >= 0; n >= 0] void

matrixptr_make_elt

Synopsis

fun{
a:t0p
} matrixptr_make_elt
  {m,n:int}
  (m: size_t m, n: size_t n, x: a):<!wrt> matrixptr(a, m, n)

matrixptr_get_at

Synopsis

overload matrixptr_get_at with matrixptr_get_at_int of 0

overload matrixptr_get_at with matrixptr_get_at_size of 0

matrixptr_get_at_int

Synopsis

fun{a:t0p}
matrixptr_get_at_int
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n), i: natLt (m), n: int n, j: natLt (n)
) :<> (a) // end of [matrixptr_get_at_int]

matrixptr_get_at_size

Synopsis

fun{a:t0p}
matrixptr_get_at_size
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n), i: sizeLt (m), n: size_t n, j: sizeLt (n)
) :<> (a) // end of [matrixptr_get_at_size]

matrixptr_set_at

Synopsis

overload matrixptr_set_at with matrixptr_set_at_int of 0

overload matrixptr_set_at with matrixptr_set_at_size of 0

matrixptr_set_at_int

Synopsis

fun{a:t0p}
matrixptr_set_at_int
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n), i: natLt (m), n: int n, j: natLt (n), x: a
) :<!wrt> void // end of [matrixptr_set_at_int]

matrixptr_set_at_size

Synopsis

fun{a:t0p}
matrixptr_set_at_size
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n), i: sizeLt (m), n: size_t n, j: sizeLt (n), x: a
) :<!wrt> void // end of [matrixptr_set_at_size]

matrixptr_exch_at

Synopsis

overload matrixptr_exch_at with matrixptr_exch_at_int

overload matrixptr_exch_at with matrixptr_exch_at_size

matrixptr_exch_at_int

Synopsis

fun{a:vt0p}
matrixptr_exch_at_int
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n)
, i: natLt (m), n: int n, j: natLt (n), x: &a>>a
) :<!wrt> void // end of [matrixptr_exch_at_int]

matrixptr_exch_at_size

Synopsis

fun{a:vt0p}
matrixptr_exch_at_size
  {m,n:int}
(
  A: !matrixptr(INV(a), m, n)
, i: sizeLt (m), n: size_t n, j: sizeLt (n), x: &a>>a
) :<!wrt> void // end of [matrixptr_exch_at_size]

fprint_matrixptr

Synopsis

fun{a:vt0p}
fprint_matrixptr{m,n:int}
(
  out: FILEref
, M: !matrixptr(INV(a), m, n), m: size_t m, n: size_t n
) : void // end of [fprint_matrixptr]

fprint_matrixptr_sep

Synopsis

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

matrixptr_tabulate

Synopsis

fun{a:vt0p}
matrixptr_tabulate
  {m,n:int} (nrow: size_t m, ncol: size_t n): matrixptr (a, m, n)

Overloaded Symbols

[]

Synopsis

overload [] with matrixptr_get_at_int

overload [] with matrixptr_get_at_size

overload [] with matrixptr_set_at_int

overload [] with matrixptr_set_at_size

ptrcast

Synopsis

overload ptrcast with matrixptr2ptr

overload ptrcast with matrixptrout2ptr

fprint

Synopsis

overload fprint with fprint_matrixptr

overload fprint with fprint_matrixptr_sep

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.