ATSLIB/libats/gmatrix_row

This package contains various functions for manipulating generic matrices, that is, two-dimensional arrays of row-major style.
  • lemma_gmatrow_param
  • lemma_gmatrow_v_param
  • gmatrow_v_cons0
  • gmatrow_v_uncons0
  • gmatrow_v_renil0
  • gmatrow_v_cons1
  • gmatrow_v_uncons1
  • gmatrow_v_renil1
  • gmatrow_v_split1x2
  • gmatrow_v_unsplit1x2
  • gmatrow_v_split_2x1
  • gmatrow_v_unsplit_2x1
  • gmatrow_v_split_2x2
  • gmatrow_v_unsplit_2x2
  • gmatrow_get_at
  • gmatrow_set_at
  • gmatrow_getref_at
  • gmatrow_getref_col_at
  • gmatrow_getref_row_at
  • gmatrow_copyto
  • gmatrow_transpto
  • gmatrow_ptr_split_2x2
  • gmatrow_foreachrow
  • gmatrow_foreachrow_env
  • gmatrow_foreachrow2
  • gmatrow_foreachrow2_env

  • lemma_gmatrow_param

    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

    lemma_gmatrow_v_param

    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

    gmatrow_v_cons0

    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)

    gmatrow_v_uncons0

    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)
    ) (* end of [gmatrow_v_uncons0] *)

    gmatrow_v_renil0

    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)

    gmatrow_v_cons1

    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) // end of [gmatrow_v_cons2]

    gmatrow_v_uncons1

    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))

    gmatrow_v_renil1

    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)

    gmatrow_v_split1x2

    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)
    ) (* end of [gmatrow_v_split1x2] *)

    gmatrow_v_unsplit1x2

    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) // end of [praxi]

    gmatrow_v_split_2x1

    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)
    ) (* end of [gmatrow_v_split_2x1] *)

    gmatrow_v_unsplit_2x1

    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) // end of [praxi]

    gmatrow_v_split_2x2

    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)
    ) (* end of [gmatrow_v_split_2x2] *)

    gmatrow_v_unsplit_2x2

    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) // end of [praxi]

    gmatrow_get_at

    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) // end of [gmatrow_get_at]

    gmatrow_set_at

    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 // end of [gmatrow_set_at]

    gmatrow_getref_at

    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) // end of [gmatrow_getref_at]

    gmatrow_getref_col_at

    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)) // endfun

    gmatrow_getref_row_at

    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(*d*))) // endfun

    gmatrow_copyto

    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 // end of [gmatrow_copyto]

    gmatrow_transpto

    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 // end of [gmatrow_transpto]

    gmatrow_ptr_split_2x2

    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)
    ) (* end of [gmatrow_ptr_split_2x2] *)

    gmatrow_foreachrow

    Synopsis

    fun{
    a:t0p
    } gmatrow_foreachrow{m,n:int}{ld:int}
    (
      M: &gmatrow(a, m, n, ld) >> _, int(m), int(n), int(ld)
    ) : void // end of [gmatrow_foreachrow]

    gmatrow_foreachrow_env

    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 // end of [gmatrow_foreachrow_env]

    gmatrow_foreachrow2

    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 // end of [gmatrow_foreachrow]

    gmatrow_foreachrow2_env

    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 // end of [gmatrow_foreachrow2_env]

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