ATSLIB/prelude/strptr

This package contains common functions for processing linear strings.

lemma_strptr_param

lemma_strnptr_param

strptr2ptr

compare_strptr_strptr

strnptr_foreach$fwork

strnptr_foreach

strnptr_foreach_env

strnptr_rforeach$cont

strnptr_rforeach$fwork

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}
  (str: !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}
  (str: !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}
  (str: !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}
  (str: !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.