ATSLIB/libats/gvector

This package contains various functions for manipulating generic vectors, that is, one-dimensional arrays.
  • gvector
  • gvector_t0ype
  • gvector_v
  • GVT
  • lemma_gvector_param
  • lemma_gvector_v_param
  • gvector_v_cons
  • gvector_v_uncons
  • gvector_v_renil
  • gvector_get_at
  • gvector_set_at
  • gvector_getref_at
  • fprint_gvector
  • fprint_gvector$sep
  • gvector_foreach
  • gvector_foreach_env
  • gvector_foreach$fwork

  • 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. SourceForge.net Logo