ATSLIB/libats/gvector

gvector

Synopsis

typedef
gvector (a:t0p, n:int, d:int) = gvector_t0ype (a, n, d)

gvector_t0ype

Synopsis

abst@ype
gvector_t0ype (a:t@ype, n:int, d:int) (*irregular*)

gvector_v

Synopsis

viewdef
gvector_v
  (a:t0p, l:addr, n:int, d:int) = gvector (a, n, d) @ l

GVT

Synopsis

stadef GVT = gvector

stadef GVT = gvector_v

lemma_gvector_param

Synopsis

praxi
lemma_gvector_param
  {a:t0p}{n:int}{d:int}
  (v: &GVT(a, n, d)): [n >= 0; d >= 1] void

lemma_gvector_v_param

Synopsis

praxi
lemma_gvector_v_param
  {a:t0p}{l:addr}{n:int}{d:int}
  (pf: !GVT(a, l, n, d)): [n >= 0; d >= 1] void

gvector_v_cons

Synopsis

praxi
gvector_v_cons
  {a:t0p}{l:addr}{n:int}{d:int}
(
  pf1: a @ l, pf2: GVT(a, l+d*sizeof(a), n, d)
) : GVT(a, l, n+1, d) // endfun

gvector_v_uncons

Synopsis

praxi
gvector_v_uncons
  {a:t0p}{l:addr}
  {n:int | n > 0}{d:int}
  (pf: GVT(a, l, n, d)): (a @ l, GVT(a, l+d*sizeof(a), n-1, d))

gvector_v_renil

Synopsis

praxi
gvector_v_renil
  {a1,a2:t0p}
  {l:addr}{n:int}{d:int} (pf: GVT(a1, l, 0, d)): GVT(a2, l, 0, d)

gvector_get_at

Synopsis

fun{a:t0p}
gvector_get_at
  {n:int}{d:int}
(
  V: &GVT(a, n, d), d: int d, i: natLt(n)
) : a // end of [gvector_get_at]

gvector_set_at

Synopsis

fun{a:t0p}
gvector_set_at
  {n:int}{d:int}
(
  V: &GVT(a, n, d), d: int d, i: natLt(n), x: a
) : void // end of [gvector_set_at]

gvector_getref_at

Synopsis

fun{a:t0p}
gvector_getref_at
  {n:int}{d:int}
  (V: &GVT(a, n, d), d: int d, i: natLt(n)): cPtr1(a)

fprint_gvector

Synopsis

fun{a:t0p}
fprint_gvector{n:int}{d:int}
(
  out: FILEref, V: &GVT(a, n, d), int n, int d
) : void // end of [fprint_gvector]

fprint_gvector$sep

Synopsis

fun{}
fprint_gvector$sep (out: FILEref): void

gvector_foreach

Synopsis

fun{a:t0p}
gvector_foreach{n:int}{d:int}
  (V: &GVT(a, n, d) >> _, n: int n, d: int d): natLte(n)

gvector_foreach_env

Synopsis

fun{
a:t0p}{env:vt0p
} gvector_foreach_env{n:int}{d:int}
(
  V: &GVT(a, n, d) >> _, n: int n, d: int d, env: &(env) >> _
) : natLte(n) // end of [gvector_foreach_env]

gvector_foreach$fwork

Synopsis

fun{
a:t0p}{env:vt0p
} gvector_foreach$fwork
  {n:int}{d:int} (x: &a >> _, env: &env >> _): void

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