ATSLIB/prelude/giterator

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


  • lemma_giter_param
  • giter_make_list
  • giter_free_list
  • giter_make_list_vt
  • giter_free_list_vt
  • giter_make_array
  • giter_free_array
  • giter_make_string
  • giter_free_string
  • giter_is_atbeg
  • giter_isnot_atbeg
  • giter_is_atend
  • giter_isnot_atend
  • giter_get
  • giter_set
  • giter_exch
  • giter_getref
  • giter_vttake
  • giter_inc
  • giter_dec
  • giter_get_inc
  • giter_set_inc
  • giter_exch_inc
  • giter_getref_inc
  • giter_vttake_inc
  • giter_dec_get
  • giter_dec_set
  • giter_dec_exch
  • giter_dec_getref
  • giter_dec_vttake
  • giter_get_fofs
  • giter_get_rofs
  • giter_fjmp
  • giter_fget_at
  • giter_fset_at
  • giter_fexch_at
  • giter_fgetref_at
  • giter_fbjmp
  • giter_fbget_at
  • giter_fbset_at
  • giter_fbexch_at
  • giter_fbgetref_at
  • giter_fgetlst
  • giter_bgetlst
  • giter_ins
  • giter_ins_inc
  • giter_rmv
  • giter_dec_rmv

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