ATSLIB/libats/ML/string
The functions declared in this package are primarily for processing
C-style strings in functional programming.
Synopsis
fun{}
itoa(x: int):<> string
Description
This function is for turning integers into their string representations.
Synopsis
fun{}
string_sing(c: charNZ):<> string
Description
Given a non-null character, this function returns a singleton string
consisting of the character.
Synopsis
fun{}
string_copy(str: NSH(string)):<> string
Description
Given a string, this function returns a copy of it.Example
The following code tests that string_copy indeed returns a copy
of a given string:
staload "libats/ML/SATS/string.sats"
implement
main () = 0 where {
val str = "abcdefg"
val () = assertloc (str = string_copy (str))
}
Synopsis
fun{}
string_make_substring
(
x0: NSH(string), start: size_t, len: size_t
) :<> string
Description
Given a string str of length n and integers st and ln, this function
returns a string consisting of chars str[st], str[st+1], ...,
str[st+min(n-st,ln)-1] if st is less than n. Otherwise, it returns the
empty string.
Example
The following code makes a simple use of substring_copy:
staload "libats/ML/SATS/string.sats"
implement
main () = 0 where {
val str = "abcdefg"
val str2 = substring_copy (str, g1int2uint(0), string_length(str))
val () = assertloc (str = str2)
}
Synopsis
fun{}
string_append
(
x1: NSH(string), x2: NSH(string)
) :<> string
Description
This function, which overload the symbol +, returns the
concatenation of two given strings.
Example
The following code shows a typical way of combining strings:
staload "libats/ML/SATS/string.sats"
implement
main0 () =
{
val Hello = "H"+"e"+"l"+"l"+"o"
val () = print (Hello + ", world!\n")
}
Note that the evaluation of the expression
"H" + "e" + "l" + "l" + "o"
generates the following intermediate strings "H", "He", "Hel", and
"Hell", which all become garbage once the evaluation returns the string
"Hello".
Synopsis
fun{}
stringlst_concat
(xs: list0(string)):<> string
Description
Given a list xs of strings, this function returns the concatenation of
xs[0], xs[1], ,,,, xs[n-1], where n is the length of xs and the notation
xs[i] refers element i in xs. Example
The following code shows a way to form the string "Hello" by
concatenating a list of singleton strings:
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/string.sats"
implement
main0 () =
{
val Hello =
stringlst_concat
(
(list0)$arrpsz{string}("H","e","l","l","o")
)
val () = print (Hello + ", world!\n")
}
Note that the call to stringlst_concat constructs the string
"Hello" without generating any intermediate substrings.
Synopsis
fun{}
string_explode(string):<> list0(char)
Description
Given a string str of length n, this function returns a list consisting
of str[0], str[1], ..., and str[n-1], where each str[i] refers to char i in
str. Example
The following code checks that the length of the list obtained from calling
string_explode on a given string equals the length of the string:
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/string.sats"
implement
main () = 0 where {
val str = "abcdefg"
val cs = string_explode (str)
val () = assertloc (string_length (str) = g0i2u(list0_length (cs)))
}
Synopsis
fun{}
string_implode(list0(char)):<> string
Description
Given a list cs of chars, this functions returns a string consisting of
cs[0], cs[1], ..., and cs[n-1], where n is the length of cs and each cs[i]
refers to char i in cs. Note that the length of the returned string is n
only if there is no null char in cs.
Example
The following code checks that the string obtained from calling
string_implode on the list returned from a call to
string_explode on a given string equals the given string:
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/string.sats"
implement
main () = 0 where {
val str = "abcdefg"
val cs = string_explode (str)
val str2 = string_implode (cs)
val () = assertloc (str = str2)
}
Synopsis
fun{}
string_tabulate
{n:int}
(
n0: size_t(n)
, fopr: (sizeLt(n)) -<cloref1> charNZ
) : string
Synopsis
fun{}
string_foreach
(cs: string, fwork: cfun(char, void)): void
Description
This function traverses its first argument (a string) and applies to each
encountered character its second argument (a closure-function). Example
The following code prints a given string onto the standard output channel:
staload "libats/ML/SATS/string.sats"
implement
main0 () = {
val str = "abcdefg"
val () = string_foreach (str, lam (c) => print_char (c))
val () = print_newline ()
}
Synopsis
overload + with string_append of 0