ATSLIB/libats/gmatrix

mord

Synopsis

Synopsis for [mord] is unavailable.

MORD

Synopsis

datatype MORD (int) =
  | MORDrow (mrow) of () | MORDcol (mcol) of ()

typedef MORD = [mo:mord] MORD(mo)

transp

Synopsis

Synopsis for [transp] is unavailable.

TRANSP

Synopsis

datatype TRANSP (transp) =
  | TPN (tpn) of () | TPT (tpt) of () | TPC (tpc) of ()

typedef TRANSP = [tp:transp] TRANSP(tp)

transpdim

Synopsis

dataprop
transpdim
(
  transp
, int // row
, int // col
, int // row_new
, int // col_new
) =
  | {m,n:int} TPDIM_N (tpn, m, n, m, n) of ()
  | {m,n:int} TPDIM_T (tpt, m, n, n, m) of ()
  | {m,n:int} TPDIM_C (tpc, m, n, n, m) of ()

transpdim_transp

Synopsis

prfun
transpdim_transp
  {tp:transp}{m1,n1:int}{m2,n2:int}
  (pf: transpdim (tp, m1, n1, m2, n2)): transpdim (tp, n1, m1, n2, m2)

gmatrix

Synopsis

typedef gmatrix
  (a:t0p, mo:mord, m:int, n:int, ld:int) = gmatrix_t0ype (a, mo, m, n, ld)

gmatrix_t0ype

Synopsis

abst@ype
gmatrix_t0ype
  (a:t@ype, mo:mord, m:int, n:int, ld:int) (* irregular *)

gmatrix_v

Synopsis

viewdef gmatrix_v
  (a:t0p, mo:mord, l:addr, m:int, n:int, ld:int) = gmatrix_t0ype (a, mo, m, n, ld) @ l

GMX

Synopsis

stadef GMX = gmatrix

stadef GMX = gmatrix_v

lemma_gmatrix_param

Synopsis

praxi
lemma_gmatrix_param
  {a:t0p}{mo:mord}
  {m,n:int}{ld:int}
  (M: &GMX (a, mo, m, n, ld))
: [0 <= mo; mo <= 1; 0 <= m; 0 <= n; 0 <= ld] void

lemma_gmatrix_v_param

Synopsis

praxi
lemma_gmatrix_v_param
  {a:t0p}{mo:mord}
  {l:addr}{m,n:int}{ld:int}
  (pf: !GMX (a, mo, l, m, n, ld))
: [0 <= mo; mo <= 1; 0 <= m; 0 <= n; 0 <= ld] void

gmatrow

Synopsis

typedef gmatrow
  (a:t0p, m:int, n:int, ld:int) = gmatrix_t0ype (a, mrow, m, n, ld)

gmatrow_v

Synopsis

viewdef gmatrow_v
  (a:t0p, l:addr, m:int, n:int, ld:int) = gmatrix_t0ype (a, mrow, m, n, ld) @ l

GMR

Synopsis

stadef GMR = gmatrow

stadef GMR = gmatrow_v

gmatcol

Synopsis

typedef gmatcol
  (a:t0p, m:int, n:int, ld:int) = gmatrix_t0ype (a, mcol, m, n, ld)

gmatcol_v

Synopsis

viewdef gmatcol_v
  (a:t0p, l:addr, m:int, n:int, ld:int) = gmatrix_t0ype (a, mcol, m, n, ld) @ l

GMC

Synopsis

stadef GMC = gmatcol

stadef GMC = gmatcol_v

gmatrix_flipord

Synopsis

praxi
gmatrix_flipord
  {a:t0p}{mo:mord}
  {m,n:int}{ld:int}
  (M: &GMX(a, mo, m, n, ld) >> GMX(a, 1-mo, n, m, ld)): void

gmatrix_v_flipord

Synopsis

praxi
gmatrix_v_flipord
  {a:t0p}{mo:mord}
  {l:addr}{m,n:int}{ld:int}
  (pf: !GMX(a, mo, l, m, n, ld) >> GMX(a, 1-mo, l, n, m, ld)): void

fprint_gmatrix

Synopsis

fun{a:t0p}
fprint_gmatrix
  {mo:mord}{m,n:int}{ld:int}
(
  FILEref
, V: &GMX(a, mo, m, n, ld), MORD(mo), int(m), int(n), int(ld)
) : void // end of [fprint_gmatrix]

fprint_gmatrix$sep1

Synopsis

fun{}
fprint_gmatrix$sep1 (out: FILEref): void

fprint_gmatrix$sep2

Synopsis

fun{}
fprint_gmatrix$sep2 (out: FILEref): void

fprint_gmatrix_sep

Synopsis

fun{a:t0p}
fprint_gmatrix_sep
  {mo:mord}{m,n:int}{ld:int}
(
  FILEref
, V: &GMX(a, mo, m, n, ld)
, MORD(mo), int(m), int(n), int(ld), sep1: string, sep: string
) : void // end of [fprint_gmatrix_sep]

gmatrix_iforeach

Synopsis

fun{
a:t0p
} gmatrix_iforeach
  {mo:mord}{m,n:int}{ld:int}
(
  M: &GMX(a, mo, m, n, ld) >> _, MORD(mo), int m, int n, int ld
) : void // end of [gmatrix_iforeach]

gmatrix_iforeach_env

Synopsis

fun{
a:t0p}{env:vt0p
} gmatrix_iforeach_env
  {mo:mord}{m,n:int}{ld:int}
(
  M: &GMX(a, mo, m, n, ld) >> _, MORD(mo), int m, int n, int ld, env: &(env) >> _
) : void // end of [gmatrix_iforeach_env]

gmatrix_iforeach$fwork

Synopsis

fun{
a:t0p}{env:vt0p
} gmatrix_iforeach$fwork{n:int}
(
  i: int, j: int, x: &(a) >> _, env: &(env) >> _
) : void // end of [gmatrix_iforeach$fwork]

gmatrix_imake_arrayptr

Synopsis

fun{a:t0p}
gmatrix_imake_arrayptr
  {mo:mord}{m,n:int}{ld:int}
(
  M: &GMX(a, mo, m, n, ld), mo: MORD(mo), int m, int n, int(ld)
) : arrayptr (a, m*n) // end of [gmatrix_imake_arrayptr]

gmatrix_imake_matrixptr

Synopsis

fun{a:t0p}
gmatrix_imake_matrixptr
  {mo:mord}{m,n:int}{ld:int}
(
  M: &GMX(a, mo, m, n, ld), mo: MORD(mo), int m, int n, int(ld)
) : matrixptr (a, m, n) // end of [gmatrix_imake_matrixptr]

gmatrix_imake$fopr

Synopsis

fun{a:t0p}
gmatrix_imake$fopr
  (i: int, j: int, x: a): a

trmatrix

Synopsis

typedef trmatrix
(
  a:t0p, mo:mord, ul: uplo, dg: diag, n:int, ld:int
) = trmatrix_t0ype (a, mo, ul, dg, n, ld)

trmatrix_t0ype

Synopsis

abst@ype
trmatrix_t0ype
(
  a:t@ype
, mo: mord, ul: uplo, dg: diag, n:int, ld: int
)

trmatrix_v

Synopsis

viewdef trmatrix_v
(
  a:t0p, mo:mord, ul: uplo, dg: diag, l:addr, n:int, ld:int
) = trmatrix_t0ype (a, mo, ul, dg, n, ld) @ l

TRMX

Synopsis

stadef TRMX = trmatrix

stadef TRMX = trmatrix_v

trmatrix_flipord

Synopsis

praxi
trmatrix_flipord
  {a:t0p}
  {mo:mord}
  {ul:uplo}
  {dg:diag}
  {n:int}{ld:int}
  (M: &TRMX(a, mo, ul, dg, n, ld) >> TRMX(a, 1-mo, 1-ul, dg, n, ld)): void

trmatrix_v_flipord

Synopsis

praxi
trmatrix_v_flipord
  {a:t0p}
  {mo:mord}
  {ul:uplo}
  {dg:diag}
  {l:addr}
  {n:int}{ld:int}
  (pf: !TRMX(a, mo, ul, dg, l, n, ld) >> TRMX(a, 1-mo, 1-ul, dg, l, n, ld)): void

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