ATSLIB/prelude/list

This package contains a variety of common functions for creating and manipulationg functional lists.

A functional data structure is one that is immutable after creation; the memory it occupies is heap-allocated, which can only be safely freed by a garbage collector (GC). The type for a singly-linked functional list containing N elements of type T is denoted by list(T, N), where T is nonlinear. Note that the type constructor list is co-variant in its first argument, that is, list(T1, N) is a subtype of list(T2, N) if T1 is a subtype of T2.

Please see list.sats and list.dats for the SATS file and DATS file in ATSLIB where the functions in this package are declared and implemented.


  • list
  • List
  • List0
  • List1
  • listLt
  • listLte
  • listGt
  • listGte
  • listBtw
  • listBtwe
  • ListSubscriptExn
  • lemma_list_param
  • list_cast
  • list_vt2t
  • list_of_list_vt
  • list_make_sing
  • list_make_pair
  • list_make_elt
  • list_make_intrange
  • list_make_array
  • list_make_arrpsz
  • fprint_list
  • fprint_list$sep
  • fprint_list_sep
  • list_head
  • list_head_exn
  • list_tail
  • list_tail_exn
  • list_last
  • list_last_exn
  • list_nth
  • list_get_at
  • list_set_at
  • list_exch_at
  • list_insert_at
  • list_remove_at
  • list_takeout_at
  • list_length
  • list_copy
  • list_append
  • list_append1_vt
  • list_append2_vt
  • list_extend
  • list_snoc
  • list_reverse
  • list_reverse_append
  • list_reverse_append1_vt
  • list_reverse_append2_vt
  • list_concat
  • list_take
  • list_take_exn
  • list_drop
  • list_drop_exn
  • list_split_at
  • list_exists
  • list_exists$pred
  • list_forall
  • list_forall$pred
  • list_equal
  • list_equal$eqfn
  • list_find
  • list_find$pred
  • list_find_exn
  • list_find_opt
  • list_assoc
  • list_assoc$eqfn
  • list_assoc_exn
  • list_assoc_opt
  • list_filter
  • list_filter$pred
  • list_labelize
  • list_app
  • list_app$fwork
  • list_map
  • list_map$fopr
  • list_imap
  • list_imap$fopr
  • list_mapopt
  • list_mapopt$fopr
  • list_map2
  • list_map2$fopr
  • list_tabulate
  • list_tabulate$fopr
  • list_zip
  • list_zipwith
  • list_zipwith$fopr
  • list_cross
  • list_crosswith
  • list_crosswith$fopr
  • list_foreach
  • list_foreach_env
  • list_foreach$cont
  • list_foreach$fwork
  • list_foreach2
  • list_foreach2_env
  • list_foreach2$cont
  • list_foreach2$fwork
  • list_iforeach
  • list_iforeach_env
  • list_iforeach$cont
  • list_iforeach$fwork
  • list_iforeach2
  • list_iforeach2_env
  • list_foldleft
  • list_foldleft$fopr
  • list_mergesort
  • list_mergesort$cmp
  • list_quicksort
  • list_quicksort$cmp
  • Overloaded Symbols
  • +
  • []
  • .head
  • .tail
  • iseqz
  • isneqz
  • length
  • copy
  • print
  • prerr
  • fprint

  • list

    Synopsis

    The full name for the list-type constructor list is list_t0ype_int_type, which is given to the datatype declared as follows:

    datatype // t@ype+: covariant
    list_t0ype_int_type
      (a:t@ype+, int) =
      | list_nil (a, 0) of ()
      | {n:int | n >= 0}
        list_cons (a, n+1) of (a, list_t0ype_int_type (a, n))
     // end of [list_t0ype_int_type]
    

    Description

    There are two data constructors list_nil and list_cons associated with list; the former constructs a list of length 0, that is, an empty list while the latter takes an element x and a list xs of length n to construct a list of length n+1 such that x and xs are the head and tail of the newly constructed list, respectively.

    List

    Synopsis

    typedef
    List(a:t0p) = [n:int] list(a, n)

    Description

    This type is for lists of unspecified length.

    List0

    Synopsis

    typedef
    List0(a:t0p) = [n:int | n >= 0] list(a, n)

    Description

    This type is for lists of unspecified length that is greater than or equal to 0. Note that List0 is essentially equivalent to List since the length of a list can never be negative. The proof function lemma_list_param can be called explicitly to cast from List to List0.

    List1

    Synopsis

    typedef
    List1(a:t0p) = [n:int | n >= 1] list(a, n)

    Description

    This type is for lists of unspecified positive length.

    listLt

    Synopsis

    typedef listLt
      (a:t0p, n:int) = [k:nat | k < n] list(a, k)

    listLte

    Synopsis

    typedef listLte
      (a:t0p, n:int) = [k:nat | k <= n] list(a, k)

    listGt

    Synopsis

    typedef listGt
      (a:t0p, n:int) = [k:int | k > n] list(a, k)

    listGte

    Synopsis

    typedef listGte
      (a:t0p, n:int) = [k:int | k >= n] list(a, k)

    listBtw

    Synopsis

    typedef listBtw
      (a:t0p, m:int, n:int) = [k:int | m <= k; k < n] list(a, k)

    listBtwe

    Synopsis

    typedef listBtwe
      (a:t0p, m:int, n:int) = [k:int | m <= k; k <= n] list(a, k)

    ListSubscriptExn

    Synopsis

    exception
    ListSubscriptExn of ()

    Description

    By convention, this exception is raised to indicate a situation where a list expected to be non-empty is actually empty.

    lemma_list_param

    Synopsis

    prfun
    lemma_list_param
      {x:t0p}{n:int}
      (xs: list(INV(x), n)): [n >= 0] void

    Description

    This proof function establishes that the integer n in any list type list(T, n) is a natural number, where T is a nonlinear type.

    list_cast

    Synopsis

    castfn
    list_cast
      {x:t0p}{n:int}
      (xs: list(INV(x), n)):<> list(x, n)

    Description

    This function can be employed to explicitly cast a list containing elements of type T1 into another list containing elements of type T2 whenever T1 is a subtype of T2.

    list_vt2t

    Synopsis

    castfn
    list_vt2t
      {x:t0p}{n:int}
      (xs: list_vt(INV(x), n)):<> list(x, n)

    Description

    This function does the same as list_of_list_vt

    list_of_list_vt

    Synopsis

    castfn
    list_of_list_vt
      {x:t0p}{n:int}
      (xs: list_vt(INV(x), n)):<!wrt> list(x, n)

    Description

    This function casts a linear list-value into a nonlinear list-value.

    list_make_sing

    Synopsis

    fun{x:t0p}
    list_make_sing (x: x):<!wrt> list_vt(x, 1)

    Description

    This function returns a list consisting of a single given value.

    list_make_pair

    Synopsis

    fun{x:t0p}
    list_make_pair (x1: x, x2: x):<!wrt> list_vt(x, 2)

    Description

    This function returns a list consisting of a pair of given values.

    list_make_elt

    Synopsis

    fun{x:t0p}
    list_make_elt
      {n:nat} (n: int n, x: x):<!wrt> list_vt(x, n)

    Description

    Given a natural number n and an element x, this function returns a list consisting of n occurrences of x.

    list_make_intrange

    Synopsis

    fun{
    } list_make_intrange
      {l,r:int | l <= r}
      (l: int l, r: int r):<!wrt> list_vt(intBtw (l, r), r-l)

    Description

    Given integers l and r satisfying l <= r, this function returns a list of integers ranging from l until r-1, inclusive.

    Example

    The following code demonstrates two ways of constructing the same list of digits:
    //
    staload UN = "prelude/SATS/unsafe.sats"
    //
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val xs1 = list_make_intrange (0, 10)
    val xs2 = (list)$arrpsz{T}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
    val ((*void*)) = assertloc ($UN.list_vt2t{T}(xs1) = $UN.list_vt2t(xs2))
    val ((*void*)) = list_vt_free (xs1)
    val ((*void*)) = list_vt_free (xs2)
    //
    } (* end of [main0] *)
    

    list_make_array

    Synopsis

    fun{a:vt0p}
    list_make_array
      {n:int} (
      A: &(@[INV(a)][n]) >> @[a?!][n], n: size_t n
    ) :<!wrt> list_vt(a, n) // endfun

    Description

    Given an array of size n, this function returns a linear list of length n such that element i in the list is the element stored in cell i of the array, where i ranges from 0 until n-1, inclusive.

    list_make_arrpsz

    Synopsis

    fun{a:vt0p}
    list_make_arrpsz
      {n:int} (psz: arrpsz (INV(a), n)):<!wrt> list_vt(a, n)

    Description

    This function, which overloads the symbol list, is often conveniently employed to build a list of some fixed length. Note that the argument of list_make_arrpsz is a linear arrpsz-value, which is consumed after list_make_arrpsz returns.

    Example

    The following code demonstrates two ways of constructing lists of fixed length:
    implement
    main0 () = {
      typedef T = int
      val xs1 = $list{T}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
      val xs2 = (list)$arrpsz{T}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
      val ((*void*)) = assertloc (xs1 = list_vt2t(xs2))
    } // end of [main0]
    

    fprint_list

    Synopsis

    fun{x:t0p}
    fprint_list(out: FILEref, xs: List(INV(x))): void

    Description

    This function prints the elements in a given list to the output channel provided as its first argument, and it calls the function fprint_list$sep before printing an element as long as the element is not the first one. Note that printing each list element is handled by calling the function fprint_val.

    Example

    The following code builds a list of digits and then prints them onto the standard output channel:
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val out = stdout_ref
    val digits =
      $list{T}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
    val ((*void*)) = fprint_list<T> (out, digits)
    val ((*void*)) = fprint_newline (out)
    //
    } (* end of [main0] *)
    

    fprint_list$sep

    Synopsis

    fun{}
    fprint_list$sep (out: FILEref): void

    Description

    This function is called by fprint_list to print a separator between two consecutive list elements. By default, it prints the comma symbol (,).

    fprint_list_sep

    Synopsis

    fun{x:t0p}
    fprint_list_sep
      (out: FILEref, xs: List(INV(x)), sep: NSH(string)): void

    Description

    This function prints the elements in a given list to the output channel provided as its first argument, interspersing the string sep between the printed list elements. Note that printing each list element is handled by calling the function fprint_val.

    list_head

    Synopsis

    fun{x:t0p}
    list_head{n:pos} (xs: list(INV(x), n)):<> (x)

    Description

    This function returns the head of a given non-empty list. It is O(1)-time.

    list_head_exn

    Synopsis

    fun{x:t0p}
    list_head_exn{n:int} (xs: list(INV(x), n)):<!exn> (x)

    Description

    This function returns the head of a given list if the list is not empty. Otherwise, it raise a run-time exception (ListSubscriptExn).

    list_tail

    Synopsis

    fun{x:t0p}
    list_tail{n:pos}
      (xs: SHR(list(INV(x), n))):<> list(x, n-1)

    Description

    This function returns the tail of a given non-empty list. It is O(1)-time.

    list_tail_exn

    Synopsis

    fun{x:t0p}
    list_tail_exn{n:int}
      (xs: SHR(list(INV(x), n))):<!exn> list(x, n-1)

    Description

    This function returns the tail of a given list if the list is not empty. Otherwise, it raise a run-time exception (ListSubscriptExn).

    list_last

    Synopsis

    fun{x:t0p}
    list_last{n:pos} (xs: list(INV(x), n)):<> (x)

    Description

    This function returns the last element of a given non-empty list. It is O(n)-time, when n is the length of the given list.

    list_last_exn

    Synopsis

    fun{x:t0p}
    list_last_exn{n:int} (xs: list(INV(x), n)):<!exn> (x)

    Description

    This function returns the last element of a given list if the list is not empty. Otherwise, it raise a run-time exception (ListSubscriptExn).

    list_nth

    Synopsis

    fun{
    x:t0p
    } list_nth{n:int}
      (xs: list(INV(x), n), i: natLt (n)):<> (x)

    Description

    Given a list of length n and a natural number i less than n, this function returns xs[i], that is, element i in xs.

    list_get_at

    Synopsis

    fun{x:t0p}
    list_get_at{n:int}
      (xs: list(INV(x), n), i: natLt (n)):<> (x)

    Description

    This function does the same as list_nth.

    list_set_at

    Synopsis

    fun{x:t0p}
    list_set_at{n:nat}
      (xs: list(INV(x), n), i: natLt (n), x: x):<> list(x, n)

    Description

    Given a list xs of length n, a natural number i less than n, and an element x, this function returns another list obtained from replacing element i in xs with x.

    list_exch_at

    Synopsis

    fun{x:t0p}
    list_exch_at{n:nat}
      (xs: list(INV(x), n), i: natLt (n), x: x):<> (list(x, n), x)

    Description

    Given a list xs of length n, a natural number i less than n, and an element x, this function returns another list and another element such that the list is obtained from replacing element i in xs with x and the element is xs[i].

    list_insert_at

    Synopsis

    fun{x:t0p}
    list_insert_at
      {n:int} (
      xs: SHR(list(INV(x), n)), i: natLte (n), x: x
    ) :<> list(x, n+1) // end of [list_insert_at]

    Description

    Given a list xs of length n, a natural number i <= n, and an element x, this function inserts x into xs so that x becomes element i in the returned list.

    list_remove_at

    Synopsis

    fun{x:t0p}
    list_remove_at
      {n:int} (
      xs: SHR(list(INV(x), n)), i: natLt (n)
    ) :<> list(x, n-1) // end of [list_remove_at]

    Description

    Given a list xs of length n and a natural number i < n, this function returns a list obtained from removing xs[i] from xs.

    list_takeout_at

    Synopsis

    fun{x:t0p}
    list_takeout_at
      {n:int} (
      xs: SHR(list(INV(x), n)), i: natLt (n), x: &(x)? >> x
    ) :<!wrt> list(x, n-1) // end of [list_takeout_at]

    Description

    This function does the same as list_remove_at except for storing the removed element in its third call-by-reference argument.

    list_length

    Synopsis

    fun{x:t0p}
    list_length
      {n:int} (xs: list(INV(x), n)):<> int (n)

    Description

    This function returns the length of a given list.

    list_copy

    Synopsis

    fun{
    x:t0p
    } list_copy
      {n:int}
      (xs: list(INV(x), n)):<!wrt> list_vt(x, n)

    Description

    Given a list xs, this function returns a copy of xs. Note that the returned copy is a linear list.

    list_append

    Synopsis

    fun{a:t0p}
    list_append
      {m,n:int}
    (
      xs: NSH(list(INV(a), m)), ys: SHR(list(a, n))
    ) :<> list(a, m+n) // end of [list_append]

    Description

    This function, which overloads the symbol +, returns a concatenation of its first argument xs and second argument ys. The time-complexity of this function is O(m), where m is the length of xs. What is special about the implementation of this function in ATSLIB is that it is tail-recursive.

    Example

    The following code makes a simple use of list_append:
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val xs1 = $list{T} (0, 1, 2, 3, 4)
    val xs2 = $list{T} (5, 6, 7, 8, 9)
    val xs12 = $list{T} (0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
    val ((*void*)) = assertloc (xs1+xs2 = xs12)
    //
    } // end of [main0]
    

    list_append1_vt

    Synopsis

    fun{
    a:t0p
    } list_append1_vt
      {i,j:int} (
      xs: list_vt(INV(a), i), ys: SHR(list(a, j))
    ) :<!wrt> list(a, i+j) // endfun

    Description

    Given a linear list xs and a list ys, this function returns a concatenation of xs and ys. Note that the linear list xs is consumed in the construction of the concatenation.

    list_append2_vt

    Synopsis

    fun{
    a:t0p
    } list_append2_vt
      {i,j:int} (
      xs: NSH(list(INV(a), i)), ys: list_vt(a, j)
    ) :<!wrt> list_vt(a, i+j) // endfun

    Description

    Given a list xs and a linear list ys, this function returns a concatenation of xs and ys. Note that the linear list ys is consumed in the construction of the concatenation.

    list_extend

    Synopsis

    fun{
    x:t0p
    } list_extend{n:int}
      (xs: list(INV(x), n), x: x):<!wrt> list_vt(x, n+1)

    Description

    Given a list xs and an element x, this function returns a list that is the concatenation of xs and [x], which [x] refers to the singleton list consisting of x alone. Note that the time-complexity of this is function is O(n), where n is the length of xs.

    list_snoc

    Synopsis

    macdef list_snoc (xs, x) = list_extend (,(xs), ,(x))

    list_reverse

    Synopsis

    fun{x:t0p}
    list_reverse
      {n:int} (xs: list(INV(x), n)):<!wrt> list_vt(x, n)

    Description

    This function returns a list that is the reverse of its argument.

    list_reverse_append

    Synopsis

    fun{a:t0p}
    list_reverse_append{m,n:int}
      (xs: NSH(list(INV(a), m)), ys: SHR(list(a, n))):<> list(a, m+n)

    Description

    This function returns a list that is the concatenation of the reverse of its first argument and its second argument.

    list_reverse_append1_vt

    Synopsis

    fun{a:t0p}
    list_reverse_append1_vt{m,n:int}
      (xs: list_vt(INV(a), m), ys: SHR(list(a, n))):<!wrt> list(a, m+n)

    Description

    Given a linear list xs and a list ys, this function returns a concatenation of the reverse of xs and ys. Note that the linear list xs is consumed in the construction of the concatenation.

    list_reverse_append2_vt

    Synopsis

    fun{a:t0p}
    list_reverse_append2_vt{m,n:int}
      (xs: NSH(list(INV(a), m)), ys: list_vt(a, n)):<!wrt> list_vt(a, m+n)

    Description

    Given a list xs and a linear list ys, this function returns a concatenation of the reverse of xs and ys. Note that the linear list ys is consumed in the construction of the concatenation.

    list_concat

    Synopsis

    fun{x:t0p}
    list_concat (xss: List(List(INV(x)))):<!wrt> List0_vt(x)

    Description

    Given a list xss, this function builds a concatenation of xss[0], xss[1], ..., and xss[n-1], where n is the length of xss and each xss[i] refers to element i in xss.

    Example

    The following code makes a simple use of list_concat:
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val xs1 = $list{T}(1)
    val xs2 = $list{T}(2)
    val xs3 = $list{T}(3)
    val xss = $list{List(T)}(xs1, xs2, xs3)
    val xs123 = list_concat (xss) // xs123 = [1, 2, 3]
    //
    val out = stdout_ref
    val ((*void*)) = fprintln! (out, "xs123 = ", xs123) // output 1,2,3
    val ((*void*)) = list_vt_free (xs123)
    //
    } (* end of [main0] *)
    

    list_take

    Synopsis

    fun{
    x:t0p
    } list_take
      {n:int}{i:nat | i <= n}
      (xs: list(INV(x), n), i: int i):<!wrt> list_vt(x, i)

    Description

    This function returns a prefix of its first argument, where the length of the prefix is specified by its second argument.

    Example

    The following code makes a simple use of list_take:
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val out = stdout_ref
    val xs1 = $list{T}(0, 1, 2, 3, 4)
    val n1 = list_length (xs1)
    val xs2 = $list{T}(5, 6, 7, 8, 9)
    //
    val ((*void*)) = assertloc (xs1 = list_vt2t(list_take (xs1 + xs2, n1)))
    //
    } (* end of [main0] *)
    

    list_take_exn

    Synopsis

    fun{
    x:t0p
    } list_take_exn
      {n:int}{i:nat} // it may raise [ListSubscriptException]
      (xs: list(INV(x), n), i: int i):<!exnwrt> [i <= n] list_vt(x, i)

    Description

    This function is like list_take except that it raises an exception (ListSubscriptExn) if its second argument exceeds the length of its first argument.

    list_drop

    Synopsis

    fun{
    x:t0p
    } list_drop
      {n:int}{i:nat | i <= n}
      (xs: SHR(list(INV(x), n)), i: int i):<> list(x, n-i)

    Description

    This function returns a suffix of its first argument, where the length of the suffix is the length of the first argument minus the integer provided as its second argument.

    Example

    The following code makes a simple use of list_drop:
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val out = stdout_ref
    val xs1 = $list{T}(0, 1, 2, 3, 4)
    val n1 = list_length (xs1)
    val xs2 = $list{T}(5, 6, 7, 8, 9)
    //
    val () = assertloc (xs2 = list_drop (xs1 + xs2, n1))
    //
    } (* end of [main0] *)
    

    list_drop_exn

    Synopsis

    fun{
    x:t0p
    } list_drop_exn
      {n:int}{i:nat} // it may raise [ListSubscriptException]
      (xs: SHR(list(INV(x), n)), i: int i):<!exn> [i <= n] list(x, n-i)

    Description

    This function is like list_drop except that it raises an exception (ListSubscriptExn) if its second argument exceeds the length of its first argument.

    list_split_at

    Synopsis

    fun{
    x:t0p
    } list_split_at
      {n:int}{i:nat | i <= n}
      (xs: SHR(list(INV(x), n)), i: int i):<!wrt> (list_vt(x, i), list(x, n-i))

    Description

    Given a list xs of length n and an integer i between 0 and n, inclusive, this function returns a pair of lists of length i and n-i such that the concatenation of the pair equals the given list xs.

    list_exists

    Synopsis

    fun{x:t0p}
    list_exists(xs: List(INV(x))):<> bool

    Description

    Given a list xs, this function returns true if and only if there exists an element in xs that satisfies the predicate implemented by list_exists$pred.

    Example

    The following code implements a function for removing the duplicates in a given list:
    //
    staload UN = "prelude/SATS/unsafe.sats"
    //
    fun{a:t0p}
    list_remove_dup (
      xs: List (a), eq: (a, a) -<0> bool
    ) : List_vt (a) = let
      fun loop (
        xs: List (a), ys: List0_vt (a)
      ) : List_vt (a) =
        case+ xs of
        | list_cons (x, xs) => let
            implement
            list_exists$pred<a> (y) = eq (x, y)
            val found = list_exists<a> ($UN.list_vt2t(ys))
          in
            if found then loop (xs, ys) else loop (xs, list_vt_cons (x, ys))
          end // end of [list_cons]
        | list_nil () => ys
      // end of [loop]
    in
      list_vt_reverse (loop (xs, list_vt_nil))
    end // end of [list_remove_dup]
    
    Note that the order of elements in the returned list is consistent with their order in the original list.

    list_exists$pred

    Synopsis

    fun{x:t0p}
    list_exists$pred(x: x):<> bool

    list_forall

    Synopsis

    fun{x:t0p}
    list_forall(xs: List(INV(x))):<> bool

    Description

    Given a list xs, this function returns true if and only if every element in xs satisfies the predicate implemented by list_forall$pred.

    list_forall$pred

    Synopsis

    fun{x:t0p}
    list_forall$pred(x: x):<> bool

    list_equal

    Synopsis

    fun{x:t0p}
    list_equal(xs1: List(INV(x)), xs2: List(x)):<> bool

    Description

    Given two lists xs1 and xs2 of length n1 and n2, respectively, this function returns true if and only if xs1 and xs2 are of the same length and the predicate implemented by list_equal$pred holds on each pair (xs1[i], xs2[i]), where i ranges from 0 until n1-1, inclusive, and xs1[i] (xs2[i]) refers to element i in xs1 (xs2).

    list_equal$eqfn

    Synopsis

    fun{x:t0p}
    list_equal$eqfn(x1: x, x2: x):<> bool

    Description

    This function is called in the implementation of list_equal to perform equality test on list elements, and its default implementation is based on gequal_val:
    implement{a}
    list_equal$eqfn (x, y) = gequal_val<a> (x, y)
    

    list_find

    Synopsis

    fun{
    x:t0p
    } list_find
      (List(INV(x)), x: &(x)? >> opt(x, b)):<> #[b:bool] bool(b)

    list_find$pred

    Synopsis

    fun{x:t0p} list_find$pred (x):<> bool

    list_find_exn

    Synopsis

    fun{x:t0p} list_find_exn (xs: List(INV(x))):<!exn> x

    Description

    Given a list xs, this function returns xs[i] (element i in xs) for the least index i such that xs[i] satisfies the predicate implemented by list_find$pred. In case there is no such an element, the function raises an exception (NotFoundExn).

    Example

    The following code finds the first odd number in a give list:
    implement
    main () = 0 where {
    //
    val xs = $list{int}(0, 1, 2, 3, 4)
    //
    implement
    list_find$pred<int> (x) = x mod 2 = 1
    //
    val () = assertloc (1 = list_find_exn<int> (xs))
    } // end of [main]
    

    list_find_opt

    Synopsis

    fun{x:t0p} list_find_opt (xs: List(INV(x))):<> Option_vt(x)

    Description

    This function is the optional version of list_find_exn.

    list_assoc

    Synopsis

    fun{
    key,itm:t0p
    } list_assoc
    (
      List @(INV(key), itm), key, x: &itm? >> opt(itm, b)
    ) :<> #[b:bool] bool(b) // end of [list_assoc]

    list_assoc$eqfn

    Synopsis

    fun{key:t0p}
    list_assoc$eqfn (k1: key, k2: key):<> bool

    list_assoc_exn

    Synopsis

    fun{
    key,itm:t0p
    } list_assoc_exn
      (kxs: List @(INV(key), itm), k: key):<!exn> itm

    list_assoc_opt

    Synopsis

    fun{
    key,itm:t0p
    } list_assoc_opt
      (kxs: List @(INV(key), itm), k: key):<> Option_vt(itm)

    list_filter

    Synopsis

    fun{
    x:t0p
    } list_filter{n:int}
      (xs: list(INV(x), n)): listLte_vt(x, n)

    Description

    Given a list xs, this function returns a linear list consisting elements in xs that satisfy the predicate implemented by list_filter$pred. The implementation of this function in ATSLIB is tail-recursive.

    list_filter$pred

    Synopsis

    fun{x:t0p} list_filter$pred (x): bool

    list_labelize

    Synopsis

    fun{
    x:t0p
    } list_labelize{n:int}
      (xs: list(INV(x), n)):<!wrt> list_vt(@(int, x), n)

    Description

    Given a list xs of length n, this function returns a linear list consisting pairs (i, xs[i]), where i ranges from 0 until n-1, inclusive, and xs[i] refers to element i in xs. The implementation of this function in ATSLIB is tail-recursive.

    list_app

    Synopsis

    fun{x:t0p}
    list_app (xs: List(INV(x))): void

    Description

    This function traverses a given list, applying to each encountered element the function implemented by list_app$fwork.

    Example

    The following code tallies all the integers in a given list:
    //
    staload
    UN = "prelude/SATS/unsafe.sats"
    //
    implement
    main () = 0 where {
    //
    var sum: int = 0
    val p_sum = addr@sum
    //
    local
    //
    implement
    list_app$fwork<int> (x) =
      $UN.ptr0_addby<int> (p_sum, x)
    //
    in (*in-of-local*)
    //
    val () = list_app<int> ($list{int}(1, 2, 3, 4, 5))
    //
    end // end of [local]
    //
    val () = assertloc (sum = 1+2+3+4+5)
    //
    } // end of [main]
    

    list_app$fwork

    Synopsis

    fun{x:t0p} list_app$fwork (x): void

    list_map

    Synopsis

    fun{
    x:t0p}{y:vt0p
    } list_map{n:int}
      (xs: list(INV(x), n)): list_vt(y, n)

    Description

    Given a list xs of length n, this function returns a linear list consisting f(xs[i]), where i ranges from 0 until n-1, xs[i] refers to element i in xs and f is the function implemented by list_map$fopr. The implementation of this function in ATSLIB is tail-recursive.

    list_map$fopr

    Synopsis

    fun{x:t0p}{y:vt0p} list_map$fopr (x: x): (y)

    list_imap

    Synopsis

    fun{
    x:t0p}{y:vt0p
    } list_imap{n:int}
      (xs: list(INV(x), n)): list_vt(y, n)

    Description

    Given a list xs of length n, this function returns a linear list consisting f(i, xs[i]), where i ranges from 0 until n-1, xs[i] refers to element i in xs, and f is the function implemented by list_imap$fopr. The implementation of this function in ATSLIB is tail-recursive.

    list_imap$fopr

    Synopsis

    fun{
    x:t0p}{y:vt0p
    } list_imap$fopr (i: intGte(0), x: x): (y)

    list_mapopt

    Synopsis

    fun{
    x:t0p}{y:vt0p
    } list_mapopt{n:int}
      (xs: list(INV(x), n)): listLte_vt(y, n)

    Description

    Given a list xs, this function applies the function implemented by list_mapopt$fopr to each element x in xs; if the application returns an optional value of the form Some(y) for some y, then y is collected in the linear list returned by list_mapopt. The implementation of this function in ATSLIB is tail-recursive.

    list_mapopt$fopr

    Synopsis

    fun{
    x:t0p}{y:vt0p
    } list_mapopt$fopr (x: x): Option_vt(y)

    list_map2

    Synopsis

    fun{
    x1,x2:t0p}{y:vt0p
    } list_map2{n1,n2:int}
    (
      xs1: list(INV(x1), n1)
    , xs2: list(INV(x2), n2)
    ) : list_vt(y, min(n1,n2)) // end of [list_map2]

    Description

    Given lists xs1 and xs2 of length n1 and n2, respectively, this function returns a linear list consisting f(xs1[i], xs2[i]), where i ranges from 0 until min(n1,n2)-1, xs1[i] (xs2[i]) refers to element i in xs1 (xs2) and f is the function implemented by list_map2$fopr. The implementation of this function in ATSLIB is tail-recursive.

    list_map2$fopr

    Synopsis

    fun{
    x1,x2:t0p}{y:vt0p
    } list_map2$fopr (x1: x1, x2: x2): (y)

    list_tabulate

    Synopsis

    fun{
    a:vt0p
    } list_tabulate{n:nat} (int n): list_vt(a, n)

    Description

    Given a natural number n, this function returns a linear list consisting of f(i) for i ranging from 0 until n-1, inclusive, where f is the function implemented by list_tabulate$fwork. The implementation of this function in ATSLIB is tail-recursive.

    Example

    The following code implements a function that returns a list of integers between two given arguments:
    fun list_make_intrange
      {l,r:int | l <= r} (
      l: int l, r: int r
    ) : list_vt (int, r-l) = let
    //
    implement
    list_tabulate$fopr<int> (i) = l + i
    //
    in
      list_tabulate<int> (r-l)
    end // end of [list_make_intrange]
    

    list_tabulate$fopr

    Synopsis

    fun{a:vt0p} list_tabulate$fopr (index: intGte(0)): (a)

    list_zip

    Synopsis

    fun{
    x,y:t0p
    } list_zip{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n)
    ) :<!wrt> list_vt((x, y), min(m,n)) // endfun

    Description

    Given two lists xs and ys of length m and n, respectively, this function zips them into a linear list xys of length min(m,n) such that element i in xys is the pair of element i in xs and element i in ys, where i ranges from 0 until min(m,n)-1, inclusive. The implementation of this function in ATSLIB is tail-recursive.

    list_zipwith

    Synopsis

    fun{
    x,y:t0p}{xy:vt0p
    } list_zipwith{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n)
    ) : list_vt(xy, min(m,n)) // endfun

    Description

    Given two lists xs and ys of length m and n, respectively, this function returns a linear list consisting of f (xs[i], ys[i]), where f is the function implemented by list_zipwith$fopr and i ranges from 0 until min(m,n)-1, inclusive. The implementation of this function in ATSLIB is tail-recursive.

    list_zipwith$fopr

    Synopsis

    fun{
    x,y:t0p}{xy:vt0p
    } list_zipwith$fopr (x: x, y: y): (xy)

    list_cross

    Synopsis

    fun{
    x,y:t0p
    } list_cross{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n)
    ) :<!wrt> list_vt((x, y), m*n) // endfun

    Description

    Given two lists xs and ys of length m and n, respectively, this function returns a linear list xys of length m*n that is the cross-product of xs and ys. More specifically, element k in xys (for each k between 0 and m*n-1, inclusive) equals (xs[i], ys[j]), where i = k/n and j=k-i*n.

    list_crosswith

    Synopsis

    fun{
    x,y:t0p}{xy:vt0p
    } list_crosswith{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n)
    ) : list_vt(xy, m*n) // end of [list_crosswith]

    Description

    Given two lists xs and ys of length m and n, respectively, this function returns a linear list xys of length m*n such that element k in xys (for each k between 0 and m*n-1, inclusive) is the return value of f (xs[i], ys[j]), where f is the function implemented by list_crosswith$fopr, and i = k/n and j=k-i*n.

    Example

    The following code builds a list of natural numbers by calling list_crosswith:
    //
    staload UN = "prelude/SATS/unsafe.sats"
    //
    implement
    main0 () =
    {
    //
    typedef T = int
    //
    val xs = $list{int}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
    val ys = $list{int}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
    //
    val xys = list_make_intrange (0, 100) // = 0, 1, 2, ..., 99
    //
    implement
    list_crosswith$fopr<T,T><T> (x, y) = 10 * x + y
    val xys2 = list_crosswith<T,T><T> (xs, ys) // = 0, 1, ..., 99
    //
    val () = assertloc ($UN.list_vt2t{T}(xys) = $UN.list_vt2t(xys2))
    //
    val () = list_vt_free<T> (xys)
    val () = list_vt_free<T> (xys2)
    //
    } (* end of [main0] *)
    

    list_crosswith$fopr

    Synopsis

    fun{
    x,y:t0p}{xy:vt0p
    } list_crosswith$fopr (x: x, y: y): (xy)

    list_foreach

    Synopsis

    fun{
    x:t0p
    } list_foreach (xs: List(INV(x))): void

    Description

    Given a list xs of length n, this function applies to xs[i] the function implemented by list_foreach$fwork, where i ranges from 0 until n-1, inclusive, and xs[i] refers to element i in xs.

    list_foreach_env

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_foreach_env
      (xs: List(INV(x)), env: &(env) >> _): void

    Description

    This function does essentially the same as list_foreach except for taking an additional argument that serves as an environment.

    Example

    //
    staload "contrib/libats-hwxi/testing/SATS/randgen.sats"
    //
    implement
    main () = let
    //
    typedef T = int
    #define N 1000000
    //
    val xs = randgen_list<T> (N)
    //
    typedef env = T
    implement
    list_foreach$fwork<T><env> (x, env) = env := env + x
    //
    var res: env = 0
    val () = list_foreach_env<T><env> (xs, res)
    //  
    val () = (
      print ("The total equals "); print res; print_newline ()
    ) // end of [val]
    //
    in
      0(*normal*)
    end // end of [main]
    

    list_foreach$cont

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_foreach$cont (x: x, env: &env): bool

    Description

    The default implementation of this function always returns true.

    list_foreach$fwork

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_foreach$fwork (x: x, env: &(env) >> _): void

    list_foreach2

    Synopsis

    fun{
    x,y:t0p
    } list_foreach2
      (xs: List(INV(x)), ys: List(INV(y))): void

    Description

    Given two lists xs and ys of length m and n, respectively, this function applies to each pair (xs[i], ys[i]) the function implemented by list_foreach2$fwork, where i ranges from 0 until min(m, n)-1, inclusive, and xs[i] (ys[i]) refers to element i in xs (ys).

    list_foreach2_env

    Synopsis

    fun{
    x,y:t0p}{env:vt0p
    } list_foreach2_env
      (xs: List(INV(x)), ys: List(INV(y)), env: &(env) >> _): void

    list_foreach2$cont

    Synopsis

    fun{
    x,y:t0p}{env:vt0p
    } list_foreach2$cont(x: x, y: y, env: &env): bool

    Description

    The default implementation of this function always returns true.

    list_foreach2$fwork

    Synopsis

    fun{
    x,y:t0p}{env:vt0p
    } list_foreach2$fwork(x: x, y: y, env: &(env) >> _): void

    list_iforeach

    Synopsis

    fun{
    x:t0p
    } list_iforeach{n:int}
      (xs: list(INV(x), n)): natLte(n)

    Description

    Given a list xs of length n, this function applies to each pair (i, xs[i]) the function implemented by list_iforeach$fwork, where i ranges from 0 until n-1, inclusive, and xs[i] refers to element i in xs.

    list_iforeach_env

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_iforeach_env{n:int}
      (xs: list(INV(x), n), env: &(env) >> _): natLte(n)

    list_iforeach$cont

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_iforeach$cont(i: intGte(0), x: x, env: &env): bool

    Description

    The default implementation of this function always returns true.

    list_iforeach$fwork

    Synopsis

    fun{
    x:t0p}{env:vt0p
    } list_iforeach$fwork(i: intGte(0), x: x, env: &(env) >> _): void

    list_iforeach2

    Synopsis

    fun{
    x,y:t0p
    } list_iforeach2{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n)
    ) : natLte(min(m,n)) // end-of-function

    Description

    Given two lists xs and ys of length m and n, respectively, this function applies to each tuple (i, xs[i], ys[i]) the function implemented by list_iforeach2$fwork, where i ranges from 0 until min(m, n)-1, inclusive, and xs[i] (ys[i]) refers to element i in xs (ys).

    list_iforeach2_env

    Synopsis

    fun{
    x,y:t0p}{env:vt0p
    } list_iforeach2_env{m,n:int}
    (
      xs: list(INV(x), m), ys: list(INV(y), n), env: &(env) >> _
    ) : natLte(min(m,n)) // end-of-function

    list_foldleft

    Synopsis

    fun{
    res:vt0p}{x:t0p
    } list_foldleft
      (xs: List(INV(x)), ini: res): res

    Description

    Given a list xs of length n, this function return the value of f(...f(ini, xs[0])..., xs[n-1]), where the notation xs[i] refers element i in xs and f is the function implemented by list_foldleft$fopr.

    Example

    The following code computes factorial of n for a given natural number n:
    //
    staload UN = "prelude/SATS/unsafe.sats"
    //
    fun factorial
      {n:nat} (n: int n): int = let
    //
    val xs = list_make_intrange (0, n)
    implement
    list_foldleft$fopr<int><int> (acc, x) = acc * (x+1)
    val res = list_foldleft<int><int> ($UN.list_vt2t(xs), 1(*ini*))
    val ((*void*)) = list_vt_free (xs)
    //
    in
      res
    end // end of [factorial]
    

    list_foldleft$fopr

    Synopsis

    fun{
    res:vt0p}{x:t0p
    } list_foldleft$fopr (acc: res, x: x): res

    list_mergesort

    Synopsis

    fun{
    a:t0p
    } list_mergesort{n:int}
      (xs: list(INV(a), n)) :<!wrt> list_vt(a, n)

    Description

    Mergesort is of time-complexity O(n(log(n))), and it is a stable sorting algorithm. This function mergesorts its argument according to the ordering implemented by list_mergesort$cmp and returns a linear list that is a sorted permutation of the argument.

    Example

    The following code mergesorts a given list of integers into a list of ascending integers and a list of descending integers.
    implement
    main () = let
    //
    val N = 10
    val out = stdout_ref
    //
    typedef T = int
    //
    val xs =
      $list{T}(0, 9, 2, 7, 4, 5, 6, 3, 8, 1)
    val ((*void*)) = fprint_list<T> (out, xs)
    val ((*void*)) = fprint_newline (out)
    //
    implement
    list_mergesort$cmp<T> (x1, x2) = compare (x1, x2)
    //
    val ys_inc = list_mergesort<T> (xs)
    val ((*void*)) = fprintln! (out, "ys_inc = ", ys_inc)
    val ((*void*)) = list_vt_free<T> (ys_inc)
    //
    implement
    list_mergesort$cmp<T> (x1, x2) = ~compare (x1, x2)
    //
    val zs_dec = list_mergesort<T> (xs)
    val ((*void*)) = fprintln! (out, "zs_inc = ", zs_dec)
    val ((*void*)) = list_vt_free<T> (zs_dec)
    //
    in
      0(*normal*)
    end // end of [main]
    

    list_mergesort$cmp

    Synopsis

    fun{a:t0p}
    list_mergesort$cmp (x1: a, x2: a):<> int (* sign *)

    Description

    This function is called in the implementation of list_mergesort to perform comparison test on list elements, and its default implementation is based on gcompare_val:
    implement{a}
    list_mergesort$cmp (x, y) = gcompare_val<a> (x, y)
    

    list_quicksort

    Synopsis

    fun{
    a:t0p
    } list_quicksort{n:int}
      (xs: list(INV(a), n)) :<!wrt> list_vt(a, n)

    Description

    Quicksort is of time-complexity O(n(log(n))) on average (but can be O(n^2) in the worse case), and it is not a stable sorting algorithm. This function quicksorts its argument according to the ordering implemented by list_quicksort$cmp and returns a linear list that is a sorted permutation of the argument.

    Example

    The following code quicksorts a given list of integers into a list of ascending integers and a list of descending integers.
    implement
    main () = let
    //
    val N = 10
    val out = stdout_ref
    //
    typedef T = int
    val xs = $list{T}
      (0, 9, 2, 7, 4, 5, 6, 3, 8, 1)
    val () =
      fprint_list<T> (out, xs)
    val () = fprint_newline (out)
    //
    implement
    list_quicksort$cmp<T> (x1, x2) = compare (x1, x2)
    //
    val ys_inc = list_quicksort<T> (xs)
    val ((*void*)) = fprintln! (out, "ys_inc = ", ys_inc)
    val ((*void*)) = list_vt_free<T> (ys_inc)
    //
    implement
    list_quicksort$cmp<T> (x1, x2) = ~compare (x1, x2)
    //
    val zs_dec = list_quicksort<T> (xs)
    val ((*void*)) = fprintln! (out, "zs_dec = ", zs_dec)
    val ((*void*)) = list_vt_free<T> (zs_dec)
    //
    in
      0(*normal*)
    end // end of [main]
    

    list_quicksort$cmp

    Synopsis

    fun{a:t0p}
    list_quicksort$cmp (x1: a, x2: a):<> int (* sign *)

    Description

    This function is called in the implementation of list_quicksort to perform comparison test on list elements, and its default implementation is based on gcompare_val:
    implement{a}
    list_quicksort$cmp (x, y) = gcompare_val<a> (x, y)
    

    Overloaded Symbols


    +

    Synopsis

    overload + with list_append

    []

    Synopsis

    overload [] with list_get_at

    .head

    Synopsis

    overload .head with list_head

    .tail

    Synopsis

    overload .tail with list_tail

    iseqz

    Synopsis

    overload iseqz with list_is_nil

    isneqz

    Synopsis

    overload isneqz with list_is_cons

    length

    Synopsis

    overload length with list_length

    copy

    Synopsis

    overload copy with list_copy

    print

    Synopsis

    overload print with print_list

    prerr

    Synopsis

    overload prerr with prerr_list

    fprint

    Synopsis

    overload fprint with fprint_list
    overload fprint with fprint_list_sep

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