ATSLIB/libats/gmatrix_row
This package contains various functions for manipulating generic matrices,
that is, two-dimensional arrays of row-major style.
Synopsis
praxi
lemma_gmatrow_param
{a:t0p}{m,n:int}{ld:int}
(M: &GMR(a, m, n, ld)): [m >= 0; n >= 1; ld >= n] void
Synopsis
praxi
lemma_gmatrow_v_param
{a:t0p}{l:addr}{m,n:int}{ld:int}
(pf: !GMR(a, l, m, n, ld)): [m >= 0; n >= 1; ld >= n] void
Synopsis
praxi
gmatrow_v_cons0
{a:t0p}{l:addr}
{m,n:int}{ld:int}
(
GVT(a, l, n, 1)
, GMR(a, l+ld*sizeof(a), m, n, ld)
) : GMR(a, l, m+1, n, ld)
Synopsis
praxi
gmatrow_v_uncons0
{a:t0p}{l:addr}
{m,n:int | m > 0}{ld:int}
(GMR(a, l, m, n, ld))
:
(
GVT(a, l, n, 1), GMR(a, l+ld*sizeof(a), m-1, n, ld)
)
Synopsis
praxi
gmatrow_v_renil0
{a1,a2:t0p}
{l:addr}{n:int}{ld:int} (GMR(a1, l, 0, n, ld)): GMR(a2, l, 0, n, ld)
Synopsis
praxi
gmatrow_v_cons1
{a:t0p}{l:addr}
{m,n:int}{ld:int}
(
GVT(a, l, m, ld)
, GMR(a, l+sizeof(a), m, n, ld)
) : GMR(a, l, m, n+1, ld)
Synopsis
praxi
gmatrow_v_uncons1
{a:t0p}{l:addr}
{m,n:int | n > 0}{ld:int}
(GMR(a, l, m, n, ld))
: (GVT(a, l, m, ld), GMR(a, l+sizeof(a), m, n-1, ld))
Synopsis
praxi
gmatrow_v_renil1
{a1,a2:t0p}
{l:addr}{m:int}{ld:int} (GMR(a1, l, m, 0, ld)): GMR(a2, l, m, 0, ld)
Synopsis
praxi
gmatrow_v_split1x2
{a:t0p}{l:addr}
{m,n:int}{ld:int}
{j:nat | j <= n}
(
GMR(a, l, m, n, ld), int j
) :
(
GMR(a, l , m, j , ld)
, GMR(a, l+j*sizeof(a), m, n-j, ld)
)
Synopsis
praxi
gmatrow_v_unsplit1x2
{a:t0p}{l:addr}
{m,j,j2:int}{ld:int}
(
GMR(a, l , m, j , ld)
, GMR(a, l+j*sizeof(a), m, j2, ld)
) : GMR(a, l, m, j+j2, ld)
Synopsis
praxi
gmatrow_v_split_2x1
{a:t0p}{l:addr}
{m,n:int}{ld:int}
{i,j:nat | i <= m}
(
GMR(a, l, m, n, ld), int i
) :
(
GMR(a, l , i , n, ld)
, GMR(a, l+i*ld*sizeof(a), m-i, n, ld)
)
Synopsis
praxi
gmatrow_v_unsplit_2x1
{a:t0p}{l:addr}
{i,i2,n:int}{ld:int}
(
GMR(a, l , i , n, ld)
, GMR(a, l+i*ld*sizeof(a), i2, n, ld)
) : GMR(a, l, i+i2, n, ld)
Synopsis
praxi
gmatrow_v_split_2x2
{a:t0p}{l:addr}
{m,n:int}{ld:int}
{i,j:nat | i <= m; j <= n}
(
GMR(a, l, m, n, ld), int i, int j
) :
(
GMR(a, l , i , j , ld)
, GMR(a, l +j*sizeof(a), i , n-j, ld)
, GMR(a, l+i*ld*sizeof(a) , m-i, j , ld)
, GMR(a, l+i*ld*sizeof(a)+j*sizeof(a), m-i, n-j, ld)
)
Synopsis
praxi
gmatrow_v_unsplit_2x2
{a:t0p}{l:addr}
{i,i2,j,j2:int}{ld:int}
(
GMR(a, l , i , j , ld)
, GMR(a, l +j*sizeof(a), i , j2, ld)
, GMR(a, l+i*ld*sizeof(a) , i2, j , ld)
, GMR(a, l+i*ld*sizeof(a)+j*sizeof(a), i2, j2, ld)
) : GMR(a, l, i+i2, j+j2, ld)
Synopsis
fun{a:t0p}
gmatrow_get_at
{m,n:int}{ld:int}
(
M: &GMR(a, m, n, ld), int(ld), i: natLt(m), j: natLt(n)
) : (a)
Synopsis
fun{a:t0p}
gmatrow_set_at
{m,n:int}{ld:int}
(
M: &GMR(a, m, n, ld), int(ld), i: natLt(m), j: natLt(n), x: a
) : void
Synopsis
fun{a:t0p}
gmatrow_getref_at
{m,n:int}{ld:int}
(
M: &GMR(a, m, n, ld), int(ld), i: natLt(m), j: natLt(n)
) : cPtr1(a)
Synopsis
fun{a:t0p}
gmatrow_getref_col_at
{m,n:int}{ld:int}
(
M: &GMR(a, m, n, ld), int(ld), j: natLt(n)
) : cPtr1(GVT(a, m, ld))
Synopsis
fun{a:t0p}
gmatrow_getref_row_at
{m,n:int}{ld:int}
(
M: &GMR(a, m, n, ld), int(ld), i: natLt(m)
) : cPtr1(GVT(a, n, 1))
Synopsis
fun{a:t0p}
gmatrow_copyto
{m,n:int}{ld1,ld2:int}
(
M1: &GMR(a, m, n, ld1)
, M2: &GMR(a?, m, n, ld2) >> GMR(a, m, n, ld2)
, int(m), int(n), int(ld1), int(ld2)
) : void
Synopsis
fun{a:t0p}
gmatrow_transpto
{m,n:int}{ld1,ld2:int}
(
M1: &GMR(a, m, n, ld1)
, M2: &GMR(a?, n, m, ld2) >> GMR(a, n, m, ld2)
, int(m), int(n), int(ld1), int(ld2)
) : void
Synopsis
fun{a:t0p}
gmatrow_ptr_split_2x2
{l:addr}
{m,n:int}{ld:int}
{i,j:nat | i <= m; j <= n}
(
pf: GMR(a, l, m, n, ld) | ptr(l), int(ld), int(i), int(j)
) : [l01,l10,l11:addr]
(
GMR(a, l , i , j , ld)
, GMR(a, l01, i , n-j, ld)
, GMR(a, l10, m-i, j , ld)
, GMR(a, l11, m-i, n-j, ld)
, (
GMR(a, l , i , j , ld)
, GMR(a, l01, i , n-j, ld)
, GMR(a, l10, m-i, j , ld)
, GMR(a, l11, m-i, n-j, ld)
) -<prf> GMR(a, l, m, n, ld)
| ptr(l01), ptr(l10), ptr(l11)
)
Synopsis
fun{
a:t0p
} gmatrow_foreachrow{m,n:int}{ld:int}
(
M: &gmatrow(a, m, n, ld) >> _, int(m), int(n), int(ld)
) : void
Synopsis
fun{
a:t0p}{env:vt0p
} gmatrow_foreachrow_env{m,n:int}{ld:int}
(
M: &gmatrow(a, m, n, ld) >> _, int(m), int(n), int(ld), env: &(env) >> _
) : void
Synopsis
fun{
a1,a2:t0p
} gmatrow_foreachrow2
{m,n:int}{ld1,ld2:int}
(
M1: &gmatrow(a1, m, n, ld1) >> _
, M2: &gmatrow(a2, m, n, ld2) >> _
, int(m), int(n), int(ld1), int(ld2)
) : void
Synopsis
fun{
a1,a2:t0p}{env:vt0p
} gmatrow_foreachrow2_env
{m,n:int}{ld1,ld2:int}
(
M1: &gmatrow(a1, m, n, ld1) >> _
, M2: &gmatrow(a2, m, n, ld2) >> _
, int(m), int(n), int(ld1), int(ld2)
, env: &(env) >> _
) : void