ATSLIB/prelude/string
This package contains various common functions for processing (immutable)
strings.
Synopsis
dataprop
string_index_p
(
n: int, int, int
) =
| string_index_p_eqz(n, n, 0)
| {i:int | n > i}
{c:int8 | c != 0}
string_index_p_neqz(n, i, c)
Description
Given a string str of length n and an index i, string_index_p(n,
i, c) means that str[i] in the string is of the type char(c).
If str[i] equals the null character, then i equals n.
Synopsis
exception StringSubscriptExn of ()
Synopsis
praxi
lemma_string_param{n:int}(string n): [n >= 0] void
Synopsis
castfn
string2ptr (x: string):<> Ptr1
Synopsis
castfn g0ofg1_string (x: String):<> string
Synopsis
castfn g1ofg0_string (x: string):<> String0
Synopsis
fun{}
string_sing(chr: charNZ):<!wrt> strnptr(1)
Description
This function constructs a singleton string consisting of its char argument.
Return Value
A linear string of length 1 is returned.
Synopsis
fun{}
string_is_empty
{n:int}(str: string(n)):<> bool(n==0)
Description
This funtion returns true if and only if its string argument is empty.
Return Value
A boolean value is returned.
Synopsis
fun{}
string_isnot_empty
{n:int}(str: string(n)):<> bool(n > 0)
Description
This funtion returns true if and only if its string argument is non-empty.
Return Value
A boolean value is returned.
Synopsis
overload string_is_atend with string_is_atend_gint
overload string_is_atend with string_is_atend_guint
Synopsis
fun{tk:tk}
string_is_atend_gint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1int(tk, i)):<> bool(i==n)
Description
Given a string of length n and an index i <= n, this function returns true
if and only if i equals n. Return Value
A boolean value is returned.
Synopsis
fun{tk:tk}
string_is_atend_guint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1uint(tk, i)):<> bool(i==n)
Description
This function does the same as string_is_atend_gint except for
taking an unsigned integer as the string index. Return Value
A boolean value is returned.
Synopsis
fun{}
string_head{n:pos} (str: string(n)):<> charNZ
Synopsis
fun{}
string_tail{n:pos} (str: string(n)):<> string(n-1)
Synopsis
overload string_get_at with string_get_at_size of 1
overload string_get_at with string_get_at_gint of 0
overload string_get_at with string_get_at_guint of 0
Synopsis
fun{tk:tk}
string_get_at_gint
{n:int}{i:nat | i < n}
(s: string(n), i: g1int(tk, i)):<> charNZ
Description
This function, which overloads the symbol [], returns the char
stored in cell i of the given string. Note that the given index i is
guranteed to be legal and the returned character is always non-null. Return Value
A non-null char is returned.
Synopsis
fun{tk:tk}
string_get_at_guint
{n:int}{i:nat | i < n}
(s: string(n), i: g1uint(tk, i)):<> charNZ
Description
This function, which overloads the symbol [], does the same as
string_get_at_gint except for taking an unsigned integer as the
string index. Return Value
A non-null char is returned.
Synopsis
overload string_test_at with string_test_at_size of 1
overload string_test_at with string_test_at_gint of 0
overload string_test_at with string_test_at_guint of 0
Synopsis
fun{tk:tk}
string_test_at_gint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1int(tk, i)):<> [c:int] (string_index_p(n, i, c) | char(c))
Description
Given a string of length n and an index i <= n, this function returns a
char c paired with a proof stating that i < n holds if and only if c is
non-null. Return Value
A char is returned.Example
The following code implements a function for computing the length of a
given string:
fun
string1_length
{n:int} .<>.
(str: string n): size_t(n) = let
#define NUL '\000'
prval () = lemma_string_param (str)
fun loop
{i:nat | i <= n} .<n-i>.
(
str: string (n), i: size_t (i)
) :<> size_t (n) = let
val (pf | c) = string_test_at (str, i)
in
if c != NUL then let
prval
string_index_p_neqz () = pf in loop (str, succ(i))
end else let
prval string_index_p_eqz () = pf in i
end
end
in
loop (str, g1i2u(0))
end
Synopsis
fun{tk:tk}
string_test_at_guint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1uint(tk, i)):<> [c:int] (string_index_p(n, i, c) | char(c))
Description
This function does the same as string_test_at_gint except for
taking an unsigned integer as the string index. Return Value
A char is returned.
Synopsis
fun lt_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is less than
its second argument according to the lexicographic ordering on signed
characters.
Synopsis
fun lte_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is less than
or equal to its second argument according to the lexicographic ordering on
signed characters.
Synopsis
fun gt_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is greater
than its second argument according to the lexicographic ordering on
signed characters.
Synopsis
fun gte_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is greater
than or equal to its second argument according to the lexicographic
ordering on signed characters.
Synopsis
fun eq_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is equal to
its second argument according to the lexicographic ordering on
signed characters.
Synopsis
fun neq_string_string
(x1: string, x2: string):<> bool = "mac#%"
Description
This function returns true if and only if its first argument is unequal
to its second argument according to the lexicographic ordering on signed
characters.
Synopsis
fun compare_string_string
(x1: string, x2: string):<> Sgn = "mac#%"
Description
This function returns ~1, 0 and 1 if and only if its first argument is
less than, equal to and greater than its second argument according to the
lexicographic ordering on signed characters.
Return Value
An integer between ~1 (negative 1) and 1, inclusive, is returned.
Synopsis
fun{
} strcmp (x1: string, x2: string):<> int
Description
This function returns a negative integer, 0 and a postive integer to
indicate that its first string argument is less than, equal to and greater
than its second string argument, respectively, where the comparison is
based on the lexicographic ordering on signed chars.
Synopsis
fun{
} strintcmp
{n1,n2:int | n2 >=0}
(x1: string n1, n2: int n2):<> int(sgn(n1-n2))
Description
This function returns ~1,0 and 1 to indicate that the length of its first
string argument is less than, equal to and greater than the value of its
second integer argument, respectively. Return Value
An integer between ~1 (negative 1) and 1 is returned.
Synopsis
fun{
} strlencmp
{n1,n2:int}
(x1: string n1, x2: string n2):<> int(sgn(n1-n2))
Description
This function returns -1, 0 and 1 to indicate that the length of its first
string argument is less than, equal to and greater than the length of its
second string argument, respectively.
Return Value
An integer between ~1 (negative 1) and 1 is returned.
Synopsis
fun{}
string_make_list
{n:int}
(cs: list(charNZ, n)):<!wrt> strnptr(n)
Description
This function returns a linear string consisting of the same sequence of
non-null chars in its argument. Return Value
A linear string is returned.Example
The following code implements a function that returns a linear string
consisting of the reverse of the sequence of chars in its argument:
staload UN = "prelude/SATS/unsafe.sats"
fun
string_reverse
{n:int} .<>.
(
str: string(n)
) : strnptr(n) = let
prval () = lemma_string_param (str)
val cs = string_explode (str)
val cs = list_vt_reverse (cs)
val res = string_make_list ($UN.list_vt2t(cs))
val () = list_vt_free (cs)
in
res
end
Synopsis
fun{}
string_make_listlen
{n:int}
(cs: list(charNZ, n), n: int(n)):<!wrt> strnptr(n)
Description
This function does the same as string_make_list except for
taking the length of the given string as its second argument.
Synopsis
fun{}
string_make_rlist
{n:int}
(cs: list(charNZ, n)):<!wrt> strnptr(n)
Description
This function returns a linear string consisting of the reverse of the
sequence of non-null chars in its argument. Return Value
A linear string is returned.
Synopsis
fun{}
string_make_rlistlen
{n:int}
(cs: list(charNZ, n), n: int(n)):<!wrt> strnptr(n)
Description
This function does the same as string_make_rlist except for
taking the length of the given string as its second argument. Return Value
A linear string is returned.
Synopsis
fun{}
string_make_substring
{n:int}{st,ln:nat | st+ln <= n}
(str: string(n), st: size_t st, ln: size_t ln):<!wrt> strnptr(ln)
Description
Given a string str of length n and integers st and ln, this function
returns a string that equals the substring in str that starts at char st
and is of length ln.
Return Value
A linear string is returned.
Synopsis
fun
fprint_string(out: FILEref, x: string): void = "mac#%"
Description
This function prints a string (its second argument) to a given output
channel (its first argument). The implementation of this function calls the
libc-function fputs declared in [stdio.h].
Synopsis
fun{}
strchr{n:int}
(str: string(n), c0: char):<> ssizeBtwe(~1, n)
Description
Given a string str and a char c0, this function returns the index of the
first char in str that equals c0 if there is such a char. Otherwise, it
returns ~1 (negative 1). The implementation of this function in ATSLIB
calls the libc-function of the same name (declared in [string.h]).
Synopsis
fun{}
strrchr{n:int}
(str: string(n), c0: char):<> ssizeBtwe(~1, n)
Description
Given a string str and a char c0, this function returns the index of the
last char in str that equals c0 if there is such a char. Otherwise, it
returns ~1 (negative 1). The implementation of this function in ATSLIB
calls the libc-function of the same name (declared in [string.h]).
Synopsis
fun{}
strstr{n:int}
(haystack: string(n), needle: string):<> ssizeBtw(~1, n)
Description
Given a string str1 and a string str2, this function returns the index of
the first substring in str1 that equals str2 if there is such a
substring. Otherwise, it returns ~1 (negative 1). Note that the function
returns 0 in the special case where str2 is empty, The implementation of
this function in ATSLIB calls the libc-function of the same name (declared
in [string.h]).
Synopsis
fun{}
strspn{n:int}
(str: string(n), accept: string):<> sizeLte(n)
Synopsis
fun{}
strcspn{n:int}
(str: string(n), accept: string):<> sizeLte(n)
Synopsis
fun{}
string_index{n:int}
(str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
Description
This function is the same as strchr except for requiring that
its second argument be a non-null char. The implementation of this
function in ATSLIB calls the libc-function of the same name (declared in
[strings.h]).
Synopsis
fun{}
string_rindex{n:int}
(str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
Description
This function is the same as strrchr except for requiring that
its second argument be a non-null char. The implementation of this
function in ATSLIB calls the libc-function of the same name (declared in
[strings.h]).
Synopsis
overload string_length with string0_length of 0
overload string_length with string1_length of 10
Synopsis
fun{}
string0_length
(x: NSH(string)):<> size_t
Description
This function, which overloads the symbol string_length, computes
the length of a given string.
Synopsis
fun{}
string1_length
{n:int} (x: NSH(string(n))):<> size_t(n)
Description
This function, which overloads the symbol string_length, does the
same as string0_length but is assigned a more informative type.
Synopsis
fun{}
string0_copy
(cs: NSH(string)):<!wrt> Strptr1
Description
This function returns a linear string that is the copy of its argument.
Synopsis
fun{}
string1_copy
{n:int}
(cs: NSH(string(n))):<!wrt> strnptr(n)
Description
This function does the same as string0_copy but is assigned
a more accurate type.
Synopsis
overload string_append with string0_append of 0
overload string_append with string0_append3 of 0
overload string_append with string0_append4 of 0
overload string_append with string0_append5 of 0
overload string_append with string0_append6 of 0
Synopsis
fun{}
string0_append
(
x1: NSH(string), x2: NSH(string)
) :<!wrt> Strptr1
Description
This function, which overloads the symbol string_append,
returns a linear string equal to the concatenation of its two string
arguments.
Synopsis
fun{}
string1_append
{n1,n2:int} (
x1: NSH(string(n1)), x2: NSH(string(n2))
) :<!wrt> strnptr(n1+n2)
Description
This function, which overloads the symbol string_append, does
the same as string0_append but is assigned a more informative
type.
Synopsis
Synopsis for [string_append3] is unavailable.
Synopsis
fun{}
string0_append3
(
x1: NSH(string)
, x2: NSH(string), x3: NSH(string)
) :<!wrt> Strptr1
Description
This function, which overloads the symbol string_append,
returns a linear string equal to the concatenation of its three string
arguments.
Synopsis
fun{}
stringlst_concat(List(string)):<!wrt> Strptr1
Description
This function returns a linear string that is the concatenation of the
strings in its argument. It is implemented based on
stringarr_concat.
Example
The following code builds a linear string "Hello" by concatenating five
singleton strings and then prints it (plus a newline) onto the standard
output channel:
implement
main0 () =
{
val xs =
$list{string}("H", "e", "l", "l", "o")
val Hello = stringlst_concat (xs)
val () = fprintln! (stdout_ref, Hello)
val () = strptr_free (Hello)
}
Note that the created linear string is freed before the code exits.
Synopsis
fun{}
stringarr_concat{n:int}
(
xs: arrayref(string, n), n: size_t(n)
) :<!wrt> Strptr1
Description
This function returns a linear string that is the concatenation of the
strings in its argument.
Synopsis
fun{}
string_explode
{n:int} (x: string(n)):<!wrt> list_vt(charNZ, n)
Description
Given a string of length n, this function returns a linear list
such that element i in the list equals char i in the string for
0 <= i < n.
Synopsis
fun{}
string_tabulate{n:int}(n: size_t(n)): strnptr(n)
Description
Given an integer n, this function returns a string of length n
such that char i in the string equals f(i) for 0 <= i < n,
where f is the function implemented by string_tabulate$fopr.
Return Value
A linear string is returned.Example
The following code gives an implementation of
string_make_substring, which constructs a linear string
consisting of the chars in a segment of a given string:
staload UN = "prelude/SATS/unsafe.sats"
implement{}
string_make_substring
{n}{st,ln} (str, st, ln) = let
implement
string_tabulate$fopr<> (i) = let
val i = $UN.cast{sizeLt(ln)} (i) in str[st+i]
end
in
$effmask_all (string_tabulate (ln))
end
Synopsis
fun{}
string_tabulate$fopr(size_t): charNZ
Synopsis
fun{}
string_foreach{n:int}(str: string(n)): sizeLte(n)
Description
This function traverses a given string from left to right and applies to
each encountered char the function implemented by
string_foreach$fwork. The traversal stops if the function
implemented by string_foreach$cont returns false. Parameters
- str : the string to be traversed.
Return Value
The number of processed chars is returned.Example
The following code implements the function strspn that computes
the length of the longest prefix of a given string consisting of only chars
contained in the second argument of this function:
implement{}
strspn (str, accept) = let
val accept = g1ofg0_string (accept)
implement{env}
string_foreach$cont (c, env) = strchr (accept, c) >= 0
in
$effmask_all (string_foreach<> (str))
end
Synopsis
fun{
env:vt0p
} string_foreach_env
{n:int}(str: string(n), env: &(env) >> _): sizeLte(n)
Description
This function does essentially the same as string_foreach
except for taking an additional argument that serves as an environment. Return Value
The number of processed chars is returned.Example
The following code implements a function that computes the value of an
unsigned integer represented as a sequence of digits (of base 10):
fun atoi
(str: string): int = let
val str = g1ofg0_string (str)
var env: int = 0
implement
string_foreach$fwork<int>
(c, env) = env := 10 * env + (c - '0')
val _ = string_foreach_env<int> (str, env)
in
env
end
Note that this function assumes its string argument consisting of
a sequence of digits.
Synopsis
fun{
env:vt0p
} string_foreach$cont(c: char, env: &env): bool
Synopsis
fun{
env:vt0p
} string_foreach$fwork(c: char, env: &(env) >> _): void
Synopsis
fun{}
string_rforeach{n:int}(str: string(n)): sizeLte(n)
Description
This function traverses a given string from right to left and applies to
each encountered char the function implemented by
string_rforeach$fwork. The traversal stops if the function
implemented by string_rforeach$cont returns false.
Return Value
The number of processed chars is returned.Example
The following code implements the function strrchr that finds
the index of the last occurrence of a char in a given string. If there is
no such occurrence, then ~1 (negative 1) is returned.
implement{}
strrchr (str, c0) = let
implement{env}
string_rforeach$cont (c, env) = c0 != c
val i = $effmask_all (string_rforeach<> (str))
in
if string_is_atend (str, i) then g1i2i(~1) else g1u2i(i)
end
Synopsis
fun{
env:vt0p
} string_rforeach_env
{n:int}(str: string(n), env: &(env) >> _): sizeLte(n)
Description
This function does essentially the same as string_rforeach
except for taking an additional argument that serves as an environment. Return Value
The number of processed chars is returned.
Synopsis
fun{
env:vt0p
} string_rforeach$cont(c: char, env: &env): bool
Synopsis
fun{
env:vt0p
} string_rforeach$fwork(c: char, env: &(env) >> _): void
Synopsis
fun stropt_none(): stropt(~1) = "mac#%"
Return Value
The null pointer is returned as a stropt-value.
Synopsis
overload stropt_some with stropt0_some of 0
overload stropt_some with stropt1_some of 10
Description
This function casts a string into a stropt-value.
Synopsis
fun{}
stropt_is_none{n:int}(stropt(n)):<> bool(n < 0)
Description
This function tests whether a stropt-value (optional string) is null. Return Value
A boolean value is returned.
Synopsis
fun{}
stropt_is_some{n:int}(stropt(n)):<> bool(n >= 0)
Description
This function tests whether a stropt-value (optional string) is non-null. Return Value
A boolean value is returned.
Synopsis
castfn
stropt_unsome{n:nat}(opt: stropt(n)):<> string(n)
Description
This function casts a non-null stropt-value (optional string) to a
string-value. Return Value
A string is returned.
Synopsis
fun{}
stropt_length{n:int}(opt: stropt(n)):<> ssize_t(n)
Description
This function computes the length of a given stropt-value (optional
string). If the argument is the null pointer, then the returned value is ~1
(negative 1).
Return Value
A signed-size integer is returned.
Synopsis
fun
fprint_stropt(out: FILEref, opt: Stropt0): void = "mac#%"
Description
This function prints a stropt-value (optional string) to a given output
channel (its first argument). If the stropt-value is not null, then it is
treated as a string. Otherwise, it is treated as the null pointer. Parameters
- out : the channel for receiving the output.
- opt : the optional string to be printed. Note that an optional string is either a
string or a null pointer.
Return Value
The void value is returned.
Synopsis
overload g0ofg1 with g0ofg1_string
Synopsis
overload g1ofg0 with g1ofg0_string
Synopsis
overload
[] with string_get_at_size of 1
overload
[] with string_get_at_gint of 0
overload
[] with string_get_at_guint of 0
Synopsis
overload < with lt_string_string
Synopsis
overload <= with lte_string_string
Synopsis
overload > with gt_string_string
Synopsis
overload >= with gte_string_string
Synopsis
overload = with eq_string_string
Synopsis
overload != with neq_string_string
Synopsis
overload compare with compare_string_string
Synopsis
overload .head with string_head of 10
Synopsis
overload .tail with string_tail of 10
Synopsis
overload
iseqz with string_is_empty of 10
overload iseqz with stropt_is_none
Synopsis
overload
isneqz with string_isnot_empty of 10
overload isneqz with stropt_is_some
Synopsis
overload length with string_length
overload length with stropt_length of 0
Synopsis
overload copy with string0_copy of 0
Synopsis
overload print with print_string of 0
overload print with print_stropt of 0
Synopsis
overload prerr with prerr_string of 0
overload prerr with prerr_stropt of 0
Synopsis
overload fprint with fprint_string of 0
overload fprint with fprint_stropt of 0