ATSLIB/prelude/strptr

This package contains common functions for processing linear strings.


  • lemma_strptr_param
  • lemma_strnptr_param
  • strptr2ptr
  • strnptr2ptr
  • strptr2strnptr
  • strnptr2strptr
  • strptr2string
  • strnptr2string
  • strptr2stropt
  • strnptr2stropt
  • strptr_is_null
  • strptr_isnot_null
  • lt_strptr_strptr
  • lte_strptr_strptr
  • gt_strptr_strptr
  • gte_strptr_strptr
  • eq_strptr_strptr
  • neq_strptr_strptr
  • compare_strptr_strptr
  • print_strptr
  • prerr_strptr
  • fprint_strptr
  • strnptr_get_at
  • strnptr_get_at_gint
  • strnptr_get_at_guint
  • strnptr_set_at
  • strnptr_set_at_gint
  • strnptr_set_at_guint
  • strptr_length
  • strnptr_length
  • strptr_append
  • strnptr_append
  • strptrlst_concat
  • strnptr_foreach$cont
  • strnptr_foreach$fwork
  • strnptr_foreach
  • strnptr_foreach_env
  • strnptr_rforeach$cont
  • strnptr_rforeach$fwork
  • strnptr_rforeach
  • strnptr_rforeach_env
  • Overloaded Symbols
  • []
  • <
  • <=
  • >
  • >=
  • =
  • !=
  • compare
  • iseqz
  • isneqz
  • length
  • copy
  • free
  • print
  • prerr
  • fprint

  • lemma_strptr_param

    Synopsis

    praxi
    lemma_strptr_param
      {l:addr} (x: !strptr l): [l>=null] void

    lemma_strnptr_param

    Synopsis

    praxi
    lemma_strnptr_param
      {l:addr}{n:int}
    (
      x: !strnptr (l, n)
    ) : [(l>null&&n>=0) || (l==null&&n==(~1))] void

    strptr2ptr

    Synopsis

    castfn
    strptr2ptr
      {l:addr} (x: !strptr l):<> ptr (l)

    strnptr2ptr

    Synopsis

    castfn
    strnptr2ptr
      {l:addr}{n:int} (x: !strnptr(l, n)):<> ptr(l)

    strptr2strnptr

    Synopsis

    castfn
    strptr2strnptr
      {l:addr} (x: strptr(l)):<> [n:int] strnptr(l, n)

    strnptr2strptr

    Synopsis

    castfn
    strnptr2strptr
      {l:addr}{n:int} (x: strnptr(l, n)):<> strptr(l)

    strptr2string

    Synopsis

    castfn
    strptr2string(x: Strptr1):<> String

    strnptr2string

    Synopsis

    castfn
    strnptr2string
      {l:addr}{n:nat}(x: strnptr(l, n)):<> string(n)

    strptr2stropt

    Synopsis

    castfn
    strptr2stropt
      {l:addr}
    (
      x: strptr (l)
    ) :<>
    [n:int
    |(l==null&&n < 0)||(l>null&&n>=0)
    ] stropt(n)

    strnptr2stropt

    Synopsis

    castfn
    strnptr2stropt
      {l:addr}{n:int}
      (x: strnptr(l, n)):<> stropt(n)

    strptr_is_null

    Synopsis

    fun{}
    strptr_is_null
      {l:addr} (x: !strptr l):<> bool (l==null)

    strptr_isnot_null

    Synopsis

    fun{}
    strptr_isnot_null
      {l:addr} (x: !strptr l):<> bool (l > null)

    lt_strptr_strptr

    Synopsis

    fun lt_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    lte_strptr_strptr

    Synopsis

    fun lte_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    gt_strptr_strptr

    Synopsis

    fun gt_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    gte_strptr_strptr

    Synopsis

    fun gte_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    eq_strptr_strptr

    Synopsis

    fun eq_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    neq_strptr_strptr

    Synopsis

    fun neq_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"

    compare_strptr_strptr

    Synopsis

    fun compare_strptr_strptr
      (x1: !Strptr0, x2: !Strptr0):<> Sgn = "mac#%"

    print_strptr

    Synopsis

    fun print_strptr (x: !Strptr0): void = "mac#%"

    prerr_strptr

    Synopsis

    fun prerr_strptr (x: !Strptr0): void = "mac#%"

    fprint_strptr

    Synopsis

    fun
    fprint_strptr
    (
      out: FILEref, x: !Strptr0
    ) : void = "mac#%"

    strnptr_get_at

    Synopsis

    overload strnptr_get_at with strnptr_get_at_size of 1
    overload strnptr_get_at with strnptr_get_at_gint of 0
    overload strnptr_get_at with strnptr_get_at_guint of 0

    strnptr_get_at_gint

    Synopsis

    fun{tk:tk}
    strnptr_get_at_gint
      {n:int}{i:nat | i < n}
      (s: !strnptr (n), i: g1int (tk, i)):<> charNZ

    strnptr_get_at_guint

    Synopsis

    fun{tk:tk}
    strnptr_get_at_guint
      {n:int}{i:nat | i < n}
      (s: !strnptr (n), i: g1uint (tk, i)):<> charNZ

    strnptr_set_at

    Synopsis

    overload strnptr_set_at with strnptr_set_at_size of 1
    overload strnptr_set_at with strnptr_set_at_gint of 0
    overload strnptr_set_at with strnptr_set_at_guint of 0

    strnptr_set_at_gint

    Synopsis

    fun{tk:tk}
    strnptr_set_at_gint
      {n:int}{i:nat | i < n}
      (s: !strnptr (n), i: g1int (tk, i), c: charNZ):<!wrt> void

    strnptr_set_at_guint

    Synopsis

    fun{tk:tk}
    strnptr_set_at_guint
      {n:int}{i:nat | i < n}
      (s: !strnptr (n), i: g1uint (tk, i), c: charNZ):<!wrt> void

    strptr_length

    Synopsis

    fun{}
    strptr_length (x: !Strptr0):<> ssize_t

    Description

    This function returns the length of a given linear string. In the special case where the argument is the null-pointer, the function returns ~1 (negative 1).

    strnptr_length

    Synopsis

    fun{}
    strnptr_length {n:int} (x: !strnptr n):<> ssize_t (n)

    Description

    This function does the same as strptr_length but it is assigned a more informative type.

    strptr_append

    Synopsis

    fun{}
    strptr_append (x1: !Strptr0, x2: !Strptr0):<!wrt> Strptr0

    Description

    This function returns a linear string that is the concatenation of its two arguments. In the case where both of the arguments are null, the function returns the null-pointer.

    strnptr_append

    Synopsis

    fun{}
    strnptr_append {n1,n2:nat}
      (x1: !strnptr n1, x2: !strnptr n2):<!wrt> strnptr (n1+n2)

    Description

    This function returns a linear string that is the concatenation of its two arguments. Note that neither of the two arguments can be null.

    strptrlst_concat

    Synopsis

    fun{}
    strptrlst_concat (xs: List_vt (Strptr0)):<!wrt> Strptr0

    Description

    This function returns a linear string that is the concatenation of the linear strings in its argument. Note that the argument (including all of the linear strings in it) is freed or consumed after a call to the function returns.

    strnptr_foreach$cont

    Synopsis

    fun{
    env:vt0p
    } strnptr_foreach$cont (c: &charNZ, env: &env): bool

    strnptr_foreach$fwork

    Synopsis

    fun{
    env:vt0p
    } strnptr_foreach$fwork (c: &charNZ >> _, env: &env): void

    strnptr_foreach

    Synopsis

    fun{}
    strnptr_foreach {n:nat} (str: !strnptr n): sizeLte(n)

    Description

    This function traverses a given linear string from left to right and applies to each encountered char-cell the function implemented by strnptr_foreach$fwork. The traversal stops if the function implemented by strnptr_foreach$cont returns false.

    Example

    The following code implements a function that captializes each letter in a given linear string:
    //
    staload UN = "prelude/SATS/unsafe.sats"
    //
    fun strnptr_upperize
      {n:nat} (str: !strnptr n): void = let
    //
    implement(env)
    strnptr_foreach$fwork<env>
      (c, env) = c := $UN.cast{charNZ}(toupper_char(c))
    //
    val _(*n*) = strnptr_foreach (str)
    //
    in
      // nothing
    end // end of [strnptr_upperize]
    

    strnptr_foreach_env

    Synopsis

    fun{
    env:vt0p
    } strnptr_foreach_env
      {n:nat} (str: !strnptr n, env: &(env) >> _): sizeLte(n)

    strnptr_rforeach$cont

    Synopsis

    fun{
    env:vt0p
    } strnptr_rforeach$cont (c: &charNZ, env: &env): bool

    strnptr_rforeach$fwork

    Synopsis

    fun{
    env:vt0p
    } strnptr_rforeach$fwork (c: &charNZ >> _, env: &env): void

    strnptr_rforeach

    Synopsis

    fun{}
    strnptr_rforeach {n:nat} (str: !strnptr n): sizeLte(n)

    strnptr_rforeach_env

    Synopsis

    fun{
    env:vt0p
    } strnptr_rforeach_env
      {n:nat} (str: !strnptr n, env: &(env) >> _): sizeLte(n)

    Overloaded Symbols


    []

    Synopsis

    overload
    [] with strnptr_get_at_size of 1
    overload
    [] with strnptr_get_at_gint of 0
    overload
    [] with strnptr_get_at_guint of 0
    overload
    [] with strnptr_set_at_size of 1
    overload
    [] with strnptr_set_at_gint of 0
    overload
    [] with strnptr_set_at_guint of 0

    <

    Synopsis

    overload < with lt_strptr_strptr

    <=

    Synopsis

    overload <= with lte_strptr_strptr

    >

    Synopsis

    overload > with gt_strptr_strptr

    >=

    Synopsis

    overload >= with gte_strptr_strptr

    =

    Synopsis

    overload = with eq_strptr_strptr
    overload = with eq_strptr_string

    !=

    Synopsis

    overload != with neq_strptr_strptr
    overload != with neq_strptr_string

    compare

    Synopsis

    overload
    compare with compare_strptr_strptr
    overload
    compare with compare_strptr_string

    iseqz

    Synopsis

    overload iseqz with strptr_is_null
    overload iseqz with strnptr_is_null

    isneqz

    Synopsis

    overload isneqz with strptr_isnot_null
    overload isneqz with strnptr_isnot_null

    length

    Synopsis

    overload length with strptr_length
    overload length with strnptr_length

    copy

    Synopsis

    overload copy with strptr0_copy of 0
    overload copy with strptr1_copy of 10

    free

    Synopsis

    overload free with strptr_free
    overload free with strnptr_free

    print

    Synopsis

    overload print with print_strptr
    overload print with print_strbuf

    prerr

    Synopsis

    overload prerr with prerr_strptr
    overload prerr with prerr_strbuf

    fprint

    Synopsis

    overload fprint with fprint_strptr
    overload fprint with fprint_strbuf

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