ATSLIB/libats/ML/string
The functions declared in this package are primarily for processing
C-style strings in functional programming.
Synopsis
fun string_copy (s: 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
(s: NSH(string), st: size_t, ln: 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
(s1: NSH(string), s2: 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
main () = 0 where {
val Hello = "H" + "e" + "l" + "l" + "o"
val _rest = ", world!\n"
val () = print (Hello + _rest)
}
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
main () = 0 where {
val Hello = stringlst_concat (
(list0)$arrpsz{string} ("H", "e", "l", "l", "o")
)
val _rest = ", world!\n"
val () = print (Hello + _rest)
}
Note that the call to stringlst_concat constructs the string
"Hello" without generating any intermediate substrings.
Synopsis
fun string_explode (s: 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 (cs: 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: size_t, f: (size_t) -<cloref1> charNZ): string
Synopsis
fun string_foreach (s: string, f: 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