ATSLIB/prelude/giterator

This package contains common functions for assembling/deassembling and manipulating iterators.

lemma_giter_param

Synopsis

prfun
lemma_giter_param
  {knd:tk}{kpm:tk}{x:vt0p}{f,r:int}
  (itr: !giter (knd, kpm, x, f, r)): [f>=0;r>=0] void

giter_make_list

Synopsis

fun
{x:t0p}
giter_make_list
  {n:int}
(
  xs: list (INV(x), n)
) : giter
  (giter_list_kind, giter_list_param(), x, 0, n)

giter_free_list

Synopsis

fun
giter_free_list
  {x:t0p}{f,r:int}
(
  itr: giter
    (giter_list_kind, giter_list_param(), x, f, r)
) : list (x, r) // end of [giter_free_list]

giter_make_list_vt

Synopsis

fun
{x:t0p}
giter_make_list_vt
  {n:int}
(
  xs: list_vt (INV(x), n)
) : giter
  (giter_list_vt_kind, giter_list_vt_param(), x, 0, n)

giter_free_list_vt

Synopsis

fun
giter_free_list_vt
  {x:t0p}{f,r:int}
(
  itr: giter
    (giter_list_vt_kind, giter_list_vt_param(), x, f, r)
) : list_vt (x, f+r) // end of [giter_free_list_vt]

giter_make_array

Synopsis

fun
{x:vt0p}
giter_make_array
  {l:addr}{n:int}
(
  pf: array_v (INV(x), l, n) | p: ptr l, n: size_t n
) : giter (giter_array_kind, giter_array_param(l), x, 0, n)

giter_free_array

Synopsis

fun
giter_free_array
  {x:vt0p}{l:addr}{f,r:int}
(
  itr: giter
    (giter_array_kind, giter_array_param(l), x, f, r)
) : (array_v (x, l, f+r) | void) // endfun

giter_make_string

Synopsis

fun
giter_make_string
  {n:int}
(
  str: string (n)
) : giter (
  giter_string_kind, giter_string_param(), char, 0, n
) // end of [giter_make_string]

giter_free_string

Synopsis

fun
giter_free_string
  {f,r:int}
(
  itr: giter (giter_string_kind, giter_string_param(), char, f, r)
) : string (f+r) // end of [giter_free_string]

giter_is_atbeg

Synopsis

fun{
knd:tk}{x:vt0p
} giter_is_atbeg
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)):<> bool (f==0)

giter_isnot_atbeg

Synopsis

fun{
knd:tk}{x:vt0p
} giter_isnot_atbeg
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)):<> bool (f > 0)

giter_is_atend

Synopsis

fun{
knd:tk}{x:vt0p
} giter_is_atend
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)):<> bool (r==0)

giter_isnot_atend

Synopsis

fun{
knd:tk}{x:vt0p
} giter_isnot_atend
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)):<> bool (r > 0)

giter_get

Synopsis

fun{
knd:tk}{x:t0p
} giter_get
  {kpm:tk}{f,r:int | r > 0}
  (itr: !giter (knd, kpm, INV(x), f, r)): x

giter_set

Synopsis

fun{
knd:tk}{x:t0p
} giter_set
  {kpm:tk}{f,r:int | r > 0}
  (itr: !giter (knd, kpm, INV(x), f, r), x: x): void

giter_exch

Synopsis

fun{
knd:tk}{x:vt0p
} giter_exch
  {kpm:tk}{f,r:int | r > 0}
  (itr: !giter (knd, kpm, INV(x), f, r), x: &x >> x): void

giter_getref

Synopsis

fun{
knd:tk}{x:vt0p
} giter_getref
  {kpm:tk}{f,r:int | r > 0}
  (itr: !giter (knd, kpm, INV(x), f, r)): Ptr1

giter_vttake

Synopsis

fun{
knd:tk}{x:vt0p
} giter_vttake
  {kpm:tk}{f,r:int | r > 0}
  (itr: !giter (knd, kpm, INV(x), f, r)): vttakeout0 (x)

giter_inc

Synopsis

fun{
knd:tk}{x:vt0p
} giter_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1)
) : void // end of [giter_inc]

giter_dec

Synopsis

fun{
knd:tk}{x:vt0p
} giter_dec
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1)
) : void // end of [giter_dec]

giter_get_inc

Synopsis

fun{
knd:tk}{x:t0p
} giter_get_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1)
) : x // end of [giter_get_inc]

giter_set_inc

Synopsis

fun{
knd:tk}{x:t0p
} giter_set_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1), x: x
) : void // end of [giter_set_inc]

giter_exch_inc

Synopsis

fun{
knd:tk}{x:vt0p
} giter_exch_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1)
, x: &x >> x
) : void // end of [giter_exch_inc]

giter_getref_inc

Synopsis

fun{
knd:tk}{x:vt0p
} giter_getref_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1)
) : Ptr1 // end of [giter_getref_inc]

giter_vttake_inc

Synopsis

fun{
knd:tk}{x:vt0p
} giter_vttake_inc
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r-1)
) : vttakeout0 (x) // end of [giter_vttake_inc]

giter_dec_get

Synopsis

fun{
knd:tk}{x:t0p
} giter_dec_get
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1)
) : x // end of [giter_dec_get]

giter_dec_set

Synopsis

fun{
knd:tk}{x:t0p
} giter_dec_set
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1), x: x
) : void // end of [giter_dec_set]

giter_dec_exch

Synopsis

fun{
knd:tk}{x:vt0p
} giter_dec_exch
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1)
, x: &x >> x
) : void // end of [giter_dec_exch]

giter_dec_getref

Synopsis

fun{
knd:tk}{x:vt0p
} giter_dec_getref
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1)
) : Ptr1 // end of [giter_dec_getref]

giter_dec_vttake

Synopsis

fun{
knd:tk}{x:vt0p
} giter_dec_vttake
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r+1)
) : vttakeout0 (x) // end of [giter_dec_vttake]

giter_get_fofs

Synopsis

fun{
knd:tk}{x:vt0p
} giter_get_fofs
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)): size_t (f)

giter_get_rofs

Synopsis

fun{
knd:tk}{x:vt0p
} giter_get_rofs
  {kpm:tk}{f,r:int}
  (itr: !giter (knd, kpm, INV(x), f, r)): size_t (r)

giter_fjmp

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fjmp // forward-jmp
  {kpm:tk}
  {f,r:int}
  {i:int | 0 <= i; i <= r}
(
//
// HX: O(log(n))-time expected (O(1) for arrays)
//
  itr: !giter (knd, kpm, INV(x), f, r)
         >> giter (knd, kpm, x, f+i, r-i), i: size_t (i)
) : void // end of [giter_fjmp]

giter_fget_at

Synopsis

fun{
knd:tk}{x:t0p
} giter_fget_at // forward-get
  {kpm:tk}
  {f,r:int}
  {i:int | 0 <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: size_t (i)
) : x // end of [giter_fget_at]

giter_fset_at

Synopsis

fun{
knd:tk}{x:t0p
} giter_fset_at // forward-set
  {kpm:tk}
  {f,r:int}
  {i:int | 0 <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: size_t (i), x: x
) : void // end of [giter_fset_at]

giter_fexch_at

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fexch_at // forward-exch
  {kpm:tk}
  {f,r:int}
  {i:int | 0 <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: size_t (i), x: &x >> x
) : void // end of [giter_fexch_at]

giter_fgetref_at

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fgetref_at // forward-get
  {kpm:tk}
  {f,r:int}
  {i:int | 0 <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: size_t (i)
) : Ptr1 // end of [giter_fgetref_at]

giter_fbjmp

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fbjmp // forward/backward-jmp
  {kpm:tk}
  {f,r:int}
  {i:int | ~f <= i; i <= r}
(
//
// HX: O(log(n))-time expected (O(1) for arrays)
//
  itr: !giter (knd, kpm, INV(x), f, r)
         >> giter (knd, kpm, x, f+i, r-i), i: ssize_t (i)
) : void // end of [giter_fbjmp]

giter_fbget_at

Synopsis

fun{
knd:tk}{x:t0p
} giter_fbget_at // forward/backward-get
  {kpm:tk}
  {f,r:int}
  {i:int | ~f <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: ssize_t (i)
) : x // end of [giter_fbget_at]

giter_fbset_at

Synopsis

fun{
knd:tk}{x:t0p
} giter_fbset_at // forward/backward-set
  {kpm:tk}
  {f,r:int}
  {i:int | ~f <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: ssize_t (i), x: x
) : void // end of [giter_fbset_at]

giter_fbexch_at

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fbexch_at // forward/backward-exch
  {kpm:tk}
  {f,r:int}
  {i:int | ~f <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: ssize_t (i), x: &x >> x
) : void // end of [giter_fbexch_at]

giter_fbgetref_at

Synopsis

fun{
knd:tk}{x:vt0p
} giter_fbgetref_at // forward/backward-getref
  {kpm:tk}
  {f,r:int}
  {i:int | ~f <= i; i < r}
(
  itr: !giter (knd, kpm, INV(x), f, r), i: ssize_t (i)
) : Ptr1 // end of [giter_fbgetref_at]

giter_fgetlst

Synopsis

fun{
knd:tk}{x:t0p
} giter_fgetlst
//
// forward-getlst
//
  {kpm:tk}
  {f,r:int}
  {i:nat}
(
  itr: !giter (knd, kpm, INV(x), f, r)
         >> giter (knd, kpm, x, f+i1, r-i1)
, i: &int i >> int (i-i1)
) : #[
  i1:int | i1==min(i, r)
] list_vt (x, i1) // end of [giter_fgetlst]

giter_bgetlst

Synopsis

fun{
knd:tk}{x:t0p
} giter_bgetlst
//
// backward-getlst
//
  {kpm:tk}
  {f,r:int}
  {i:nat}
(
  itr: !giter (knd, kpm, INV(x), f, r)
         >> giter (knd, kpm, x, f-i1, r+i1)
, i: &int i >> int (i-i1)
) : #[
  i1:int | i1==min(i, f)
] list_vt (x, i1) // end of [giter_bgetlst]

giter_ins

Synopsis

fun{
knd:tk}{x:vt0p
} giter_ins
  {kpm:tk}{f,r:int}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f, r+1), x: x
) : void // end of [giter_ins]

giter_ins_inc

Synopsis

fun{
knd:tk}{x:vt0p
} giter_ins_inc
  {kpm:tk}{f,r:int}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f+1, r), x: x
) : void // end of [giter_ins_inc]

giter_rmv

Synopsis

fun{
knd:tk}{x:vt0p
} giter_rmv
  {kpm:tk}{f,r:int | r > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f, r-1)
) : x(*removed*) // end of [giter_rmv]

giter_dec_rmv

Synopsis

fun{
knd:tk}{x:vt0p
} giter_dec_rmv
  {kpm:tk}{f,r:int | f > 0}
(
  itr: !giter (knd, kpm, INV(x), f, r) >> giter (knd, kpm, x, f-1, r)
) : x(*removed*) // end of [giter_dec_rmv]

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