ATSLIB/libats/ML/string

The functions declared in this package are primarily for processing C-style strings in functional programming.
  • itoa
  • string_sing
  • string_copy
  • string_make_substring
  • string_append
  • stringlst_concat
  • string_explode
  • string_implode
  • string_tabulate
  • string_foreach
  • Overloaded Symbols
  • +

  • itoa

    Synopsis

    fun{}
    itoa (x: int):<> string

    Description

    This function is for turning integers into their string representations.

    string_sing

    Synopsis

    fun{}
    string_sing (c: charNZ):<> string

    Description

    Given a non-null character, this function returns a singleton string consisting of the character.

    string_copy

    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))
    } // end of [main]
    

    string_make_substring

    Synopsis

    fun{}
    string_make_substring
    (
      x0: NSH(string), start: size_t, len: size_t
    ) :<> string // end-of-function

    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)
    } // end of [main]
    

    string_append

    Synopsis

    fun{}
    string_append
    (
      x1: NSH(string), x2: NSH(string)
    ) :<> string // end of [string_append]

    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")
    } (* end of [main0] *)
    
    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".

    stringlst_concat

    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")
    ) (* end of [val] *)
    //
    val ((*void*)) = print (Hello + ", world!\n")
    //
    } (* end of [main0] *)
    
    Note that the call to stringlst_concat constructs the string "Hello" without generating any intermediate substrings.

    string_explode

    Synopsis

    fun{}
    string_explode(x0: 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)))
    } // end of [main]
    

    string_implode

    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)
    } // end of [main]
    

    string_tabulate

    Synopsis

    fun{}
    string_tabulate
      {n:int}
    (
      n0: size_t(n), fopr: (sizeLt(n)) -<cloref1> charNZ
    ) : string // end of [string_tabulate]

    string_foreach

    Synopsis

    fun{}
    string_foreach
      (x: 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 ()
    } // end of [main]
    

    Overloaded Symbols


    +

    Synopsis

    overload + with string_append of 0

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