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_reverse_append1_vt

list_reverse_append2_vt

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: 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}
  (list(INV(x), n), 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}
  (list(INV(x), n), natLt(n)):<> (x)

Description

This function does the same as list_nth.

list_set_at

Synopsis

Synopsis for [list_set_at] is unavailable.

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

Synopsis for [list_exch_at] is unavailable.

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{n:int}
(
  xs: list(INV(x), n), x0: &(x)? >> opt(x, i >= 0)
) :<!wrt> #[i:int | i < n] int(i) // end-of-function

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))

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}
{res:vt0p}
list_zipwith{m,n:int}
(
  xs: list(INV(x), m)
, ys: list(INV(y), n)
) : list_vt(res, 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}
{res:vt0p}
list_zipwith$fopr (x: x, y: y): (res)

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}
{res:vt0p}
list_crosswith
  {m,n:int}
(
  xs: list(INV(x), m)
, ys: list(INV(y), n)
) : list_vt(res, 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}
{res:vt0p}
list_crosswith$fopr(x: x, y: y): (res)

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.