ATSLIB/libats/ML/list0

The functions declared in this package are primarily for supporting ML-style processing of list-values. The programmer is encouraged to use the dependent datatype list instead of list0 after gaining familiarity with dependent types.

list0

list0_of_list

list0_of_list_vt

list0_make_intrange_lr

list0_make_intrange_lrd

list0

Synopsis

The full name of the list0-type constructor is list0_t0ype_type, which is given to the datatype declared as follows:

datatype // t@ype+: covariant
list0_t0ype_type (a: t@ype+) =
  | list0_nil of ()
  | list0_cons of (a, list0_t0ype_type a)
// end of [list0_t0ype_type]

list0_of_list

Synopsis

castfn
list0_of_list
  {a:t@ype}(List(INV(a))):<> list0(a)

Description

This function casts a list-value of indexed type to a list-value of unindexed type.

list0_of_list_vt

Synopsis

castfn
list0_of_list_vt
  {a:t@ype}(List_vt(INV(a))):<> list0(a)

Description

This function casts a linear list-value of indexed type to a list-value of unindexed type.

g0ofg1_list

Synopsis

castfn
g0ofg1_list
  {a:t@ype}(List(INV(a))):<> list0(a)

Description

This function, which overloads the symbol g0ofg1, casts a list-value of indexed type to another list-value of unindexed type.

g1ofg0_list

Synopsis

castfn
g1ofg0_list
  {a:t@ype}(xs: list0(INV(a))):<> List0(a)

Description

This function, which overloads the symbol g1ofg0, casts a list-value of unindexed type to another list-value of indexed type.

list0_make_sing

Synopsis

fun{a:t0p}
list0_make_sing(x: a):<> list0(a)

Description

This function constructs a singleton list.

list0_make_pair

Synopsis

fun{a:t0p}
list0_make_pair(x1: a, x2: a):<> list0(a)

Description

Given two elements x1 and x2, this function returns a list consisting of x1 and x2 as its first and second elements, respectively.

list0_make_elt

Synopsis

fun{a:t0p}
list0_make_elt(n: int, x: a):<!exn> list0(a)

Description

Given an integer n and an element x, this function returns a list consisting of n occurrences of x if n is a natural number. Otherwise it raises an exception (IllegalArgExn).

list0_make_intrange

Synopsis

overload
list0_make_intrange with list0_make_intrange_lr

overload
list0_make_intrange with list0_make_intrange_lrd

list0_make_intrange_lr

Synopsis

fun{}
list0_make_intrange_lr
  (l: int, r: int):<> list0(int)

Description

Given integers l and r, this function returns the list consisting of integers l, l+1, ..., and r-1, inclusive if l <= r holds. Otherwise, it returns the list l, l-1, ..., r+1, inclusive.

list0_make_intrange_lrd

Synopsis

fun{}
list0_make_intrange_lrd
  (l: int, r: int, d: int):<!exn> list0(int)

Description

Given integers l, r and d, if l < r and d > 0, then this function returns the list consisting of integers l, l+d, ..., l+n*d, where n is the largest natural number satisfying l+n*d < r; if l > r and d < 0, this function returns the list consisting of integers l, l-d, ..., l-n*d, where n is the largest natural number satisfying l-n*d > r; if d = 0, then this function raises an exception (IllegalArgExn); otherwise, this function returns the empty list.

list0_make_arrpsz

Synopsis

fun{a:t0p}
list0_make_arrpsz{n:int}
  (psz: arrpsz(INV(a), n)):<!wrt> list0(a)

Description

This function, which overloads the symbol list0, is often conveniently employed to build a list of some fixed length.

Example

The following code builds a list of digits and then prints them out:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
main0 () =
{
//
val xs = (list0)$arrpsz{int}(0, 1, 2, 3, 4, 5, 6, 7, 8, 9)
val () = list0_foreach<int> (xs, lam (x) => print_int (x))
val () = print_newline ((*void*))
//
} (* end of [main0] *)

list0_is_nil

Synopsis

fun{a:t0p}
list0_is_nil(list0(a)):<> bool

Description

This function returns true if and only if its list argument is empty.

list0_is_cons

Synopsis

fun{a:t0p}
list0_is_cons(list0(a)):<> bool

Description

This function returns true if and only if its list argument is not empty.

list0_is_empty

Synopsis

fun{a:t0p}
list0_is_empty(list0(a)):<> bool

Description

This function does the same as list0_is_nil.

list0_isnot_empty

Synopsis

fun{a:t0p}
list0_isnot_empty(list0(a)):<> bool

Description

This function does the same as list0_is_cons.

list0_head_exn

Synopsis

fun{a:t0p}
list0_head_exn
  (xs: list0(INV(a))):<!exn> (a)

Description

This function returns the head of a given list if the list is non-empty or raises an exception (ListSubscriptExn) if the list is empty. It is O(1)-time.

list0_head_opt

Synopsis

fun{a:t0p}
list0_head_opt
  (xs: list0(INV(a))):<> Option_vt(a)

Description

This function is the optional version of list0_head_exn.

list0_tail_exn

Synopsis

fun
{a:t0p}
list0_tail_exn
  (xs: SHR(list0(INV(a)))):<!exn> list0(a)

Description

This function returns the tail of a given list if the list is non-empty. Otherwise, it raises an exception (ListSubscriptExn). The function is O(1)-time.

list0_tail_opt

Synopsis

fun
{a:t0p}
list0_tail_opt
  (xs: SHR(list0(INV(a)))):<> Option_vt(list0(a))

Description

This function is the optional version of list0_tail_exn.

list0_last_exn

Synopsis

fun
{a:t0p}
list0_last_exn
  (xs: list0(INV(a))):<!exn> (a)

Description

This function returns the last element of a given list if the list is non-empty. Otherwise, it raises an exception (ListSubscriptExn). The function is O(n)-time, where n is the length of its argument.

list0_last_opt

Synopsis

fun
{a:t0p}
list0_last_opt
  (xs: list0(INV(a))):<> Option_vt(a)

Description

This function is the optional version of list0_last_exn.

list0_nth_exn

Synopsis

fun{a:t0p}
list0_nth_exn
(xs: list0(INV(a)), i0: int):<!exn> (a)

Description

This function returns element i of a given list if i is a natural number less than the length of the list. Otherwise, it raises an exception (ListSubscriptExn). The function is O(i)-time.

Example

The following code gives a terribly inefficient O(n^2)-time implementation of list concatenation:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
list0_append (xs, ys) = let
  fun loop (
    xs: list0 a, i: int, res: list0 a
  ) : list0 a =
    if i > 0 then let
      val i1 = i - 1
      val res = list0_cons (list0_nth_exn (xs, i1), res)
    in
      loop (xs, i1, res)
    end else res // end of [if]
  // end of [loop]
in
  $effmask_all (loop (xs, list0_length (xs), ys))
end // end of [list0_append]

list0_nth_opt

Synopsis

fun{a:t0p}
list0_nth_opt
(xs: list0(INV(a)), i0: int):<> Option_vt(a)

Description

This function is the optional version of list0_nth_exn.

list0_get_at_exn

Synopsis

fun{a:t0p}
list0_get_at_exn
(xs: list0(INV(a)), i0: int):<!exn> (a)

Description

This function, which overloads the symbol [], does the same as list0_nth_exn.

print_list0

Synopsis

fun{a:t0p}
print_list0(xs: list0(INV(a))): void

Description

This function prints a given list onto STDOUT.

prerr_list0

Synopsis

fun{a:t0p}
prerr_list0(xs: list0(INV(a))): void

Description

This function prints a given list onto STDERR.

fprint_list0

Synopsis

fun{a:t0p}
fprint_list0
(
  out: FILEref, xs: list0(INV(a))
) : void // end of [fprint_list0]

fprint_list0_sep

Synopsis

fun{a:t0p}
fprint_list0_sep
(
  out: FILEref, xs: list0(INV(a)), sep: string
) : void // end of [fprint_list0_sep]

list0_insert_at_exn

Synopsis

fun{a:t0p}
list0_insert_at_exn
(
  SHR(list0(INV(a))), i: int, x: (a)
) :<!exn> list0(a) // endfun

Description

Given a list xs of length n, an integer i and an element x, this function builds a list xs1 by inserting x into xs at position i if i is between 0 and n, inclusive. Otherwise, it raises an exception (IllegalArgExn). Clearly, if the function returns a list, then element i in the returned list must be x. The function is O(i)-time.

list0_remove_at_exn

Synopsis

fun{a:t0p}
list0_remove_at_exn
  (SHR(list0(INV(a))), int):<!exn> list0(a)

Description

Given a list xs of length n, an integer i and an element x, this function builds a list xs1 by removing element i in xs if i is between 0 and n-1, inclusive. Otherwise, it raises an exception (IllegalArgExn). The function is O(i)-time.

Example

Let xs be a list of length n, i an integer between 0 and n-1, inclusive, and xs1 the list obtained from removing element i in xs. The following code checks that xs equals the list built by inserting xs[i] into xs1 at position i:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
main () = let
//
#define N 10
//
val i = N / 2
val xs = list0_make_intrange (0, N)
val ys = list0_insert_at_exn (list0_remove_at_exn (xs, i), i, xs[i])
val iseq = list0_equal (xs, ys, lam (x, y) => x = y)
val ((*void*)) = assertloc (iseq)
//
in
  0(*NormalExit*)
end // end of [main]

list0_takeout_at_exn

Synopsis

fun{a:t0p}
list0_takeout_at_exn
(
xs: SHR(list0(INV(a))), i: int, x: &a? >> a
) :<!exnwrt> list0(a) // end-of-function

Description

This function is similar to list0_remove_at_exn except that it also stores the removed element (in its third call-by-reference argument).

list0_length

Synopsis

fun
{a:t0p}
list0_length
  (xs: list0(INV(a))):<> intGte(0)

Description

This function returns the length of a given list, and its implementation is tail-recursive. It is O(n)-time, where n is the length of the given list. For convenience, list0_length overloads the symbol length.

list0_append

Synopsis

fun
{a:t0p}
list0_append
(
xs: NSH(list0(INV(a))), ys: SHR(list0(a))
) :<> list0(a)

Description

Given two lists xs and ys, this function returns the concatenation of xs and ys. It is O(n)-time, where n is the length of xs. For convenience, list0_append overloads the symbol +. Note that the implementation of list0_append is tail-recursive in ATSLIB.

Example

The following code checks that the length of the concatenation of two lists equals the sum of their individual lengths:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
main () = let
  #define M 10
  #define N 20
  #define length list0_length
  val xs = list0_make_elt<char> (M, 'a')
  val ys = list0_make_elt<char> (N, 'b')
  val () = assertloc (length (xs) + length (ys) = length (xs + ys))
in
  0(*NormalExit*)
end // end of [main]

list0_extend

Synopsis

fun
{a:t0p}
list0_extend
  (xs: NSH(list0(INV(a))), y0: a):<> list0(a)

Description

Given a list xs and an element y, this function returns the concatenation of xs and the singleton list consisting of y. It is O(n)-time, where n is the length of xs.

Example

The following code gives a typical implementation of the list-reverse function by a beginner of functional programming:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
list0_reverse (xs) =
  case+ xs of
  | list0_cons
      (x, xs) => list0_extend (list0_reverse (xs), x)
  | list0_nil () => list0_nil ()
// end of [list0_reverse]

Note that this implementation is terribly inefficient both time-wise and memory-wise: It is O(n^2)-time and non-tail-recursive.

list0_snoc

Synopsis

macdef list0_snoc = list0_extend

Description

This function does the same as list0_extend.

list0_reverse

Synopsis

fun{a:t0p}
list0_reverse
  (xs: list0(INV(a))):<> list0(a)

Description

This function returns the reverse of a given list. It is O(n)-time, where n is the length of the given list, and its implementation in ATSLIB is tail-recurisive.

list0_reverse_append

Synopsis

fun{a:t0p}
list0_reverse_append
  (xs: list0(INV(a)), ys: list0(a)):<> list0(a)

Description

Given two lists xs and ys, this function returns the concatenation of rxs and ys, where rxs refers to the reverse of xs. It is O(n)-time, where n is the length of the given list, and its implementation in ATSLIB is tail-recurisive.

list0_concat

Synopsis

fun{a:t0p}
list0_concat
  (xss: NSH(list0(list0(INV(a))))):<> list0(a)

Description

Given a list xss of lists, this funciton returns the concatenation of xss[0], xss[1], ..., and xss[n-1], where n is the length of xss.

list0_take_exn

Synopsis

fun{a:t0p}
list0_take_exn
  (xs: NSH(list0(INV(a))), i: int):<!exn> list0(a)

Description

Given a list xs and an integer i, this function contructs another list consisting of the first i elemements of xs. If i is negative, the function raises the exception IllegalArgExn. If i exceeds the length of xs, then the function raises the exception ListSubscriptExn. The time-complexity of the function is O(i).

list0_drop_exn

Synopsis

fun{a:t0p}
list0_drop_exn
  (xs: SHR(list0(INV(a))), i: int):<!exn> list0(a)

Description

Given a list xs and an integer i, this function returns the suffix of xs that is of length n-i, where n is the length of xs. If i is negative, the function raises the exception IllegalArgExn. If i exceeds the length of xs, then the function raises the exception ListSubscriptExn. The time-complexity of the function is O(i).

list0_tabulate

Synopsis

fun{a:t0p}
list0_tabulate
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): list0(a)

Description

Given an integer n and a function f, this function returns a list consisting of the elements f(0), f(1), ..., f(n-1) if n is a natural number. Otherwise, it raises an exception (IllegalArgExn).

Example

The following code builds a list of digits and then prints them onto the standard output channel:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
main () = 0 where {
  val xs = list0_tabulate<int> (10, lam i => i)
  val () = fprint_list0_sep<int> (stdout_ref, xs, ", ")
} // end of [main]

As a more elaborate example, the following code implements a function list0_permute that returns a list consisting of all the permutations of a given list:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
fun{a:t0p}
list0_permute
(
  xs0: list0 (a)
) : list0 (list0 a) = let
  val n = list0_length (xs0)
in
//
case+ xs0 of
| list0_cons
    (x0, xs1) => let
    val yss = list0_permute (xs1)
    val f = lam (ys: list0 a) =<cloref1>
      list0_tabulate<list0(a)> (n, lam i => list0_insert_at_exn (ys, i, x0))
    // end of [lam] // end of [val]
  in
    list0_concat (list0_map (yss, f))
  end // end of [list0_cons]
| list0_nil () => list0_sing (list0_nil ())
//
end // end of [list0_permute]

list0_tabulate_opt

Synopsis

fun{a:t0p}
list0_tabulate_opt
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), Option_vt(a))): list0(a)

Description

Given an integer n and a function f, this function returns a list that collects precisely every x whenever Some0(x) is returned by f(i), where i ranges from 0 until n-1, inclusive.

list0_app

Synopsis

fun
{a:t0p}
list0_app
(
xs: list0(INV(a)), fwork: cfun(a, void)
) : void // end of [list0_app]

Description

This function is idential to list0_foreach.

list0_foreach

Synopsis

fun{a:t0p}
list0_foreach
(
xs: list0(INV(a)), fwork: cfun(a, void)
) : void // end of [list0_foreach]

Description

This function applies its second argument to each element in its first argument.

list0_iforeach

Synopsis

fun{a:t0p}
list0_iforeach
(
xs: list0(INV(a)), fwork: cfun2(intGte(0), a, void)
) : intGte(0)(*length*) // end of [list0_iforeach]

Description

This function applies its second argument f to (i, x), where i ranges from 0 to the length of xs minus 1 and x is element i in xs.

Example

The following code implements a function for printing out a given list:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
fprint_list0_sep (out, xs, sep) = let
  fun f (
    i: int, x: a
  ) :<cloref1> void = let
    val () = if i > 0 then fprint_string (out, sep)
  in
    fprint_val<a> (out, x)
  end // end of [f]
  val _(*n*) = list0_iforeach (xs, f)
in
  // nothing
end // end of [fprint_list0_sep]

Note that the argument sep of fprint_list0_sep is only printed between list elements.

list0_foreach2

Synopsis

fun
{a1,a2:t0p}
list0_foreach2
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, fwork: cfun2(a1, a2, void)
) : void // end of [list0_foreach2]

Description

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

list0_foreach2_eq

Synopsis

fun{a1,a2:t0p}
list0_foreach2_eq
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, fwork: cfun2(a1, a2, void), sgn: &int? >> int
) : void // end of [list0_foreach2_eq]

Description

This function is largely similar to list0_foreach2. After a call to the function returns, the value stored in the call-by-reference parameter sgn equals sgn(n1-n2), that is, the sign of n1-n2, where n1 and n2 are the lengths of the first and second arguments of the function, respectively.

list0_foldleft

Synopsis

fun{
res:t0p}{a:t0p
} list0_foldleft
(
xs: list0(INV(a)), ini: res, fopr: cfun2(res, a, res)
) : res // end of [list0_foldleft]

Description

Given a list xs of length n, this function returns the value f (...f (f (ini, xs[0]), xs[1])..., xs[n-1]), where the notation xs[i] refers to element i in the list xs. The implementation of this function is tail-recursive.

Example

The following code gives a standard implementation of the list-reverse function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
{a}(*tmp*)
list0_reverse
  (xs) = $effmask_all (
  list0_foldleft<a><list0(a)> (xs, list0_nil, lam (res, x) => list0_cons (x, res))
) // end of [list0_reverse]

list0_ifoldleft

Synopsis

fun{
res:t0p}{a:t0p
} list0_ifoldleft
(
xs: list0(INV(a)), ini: res, fopr: cfun3(res, int, a, res)
) : res // end of [list0_ifoldleft]

Description

Given a list xs of length n, this function returns the value f (...f (f (ini, 0, xs[0]), 1, xs[1])..., n-1, xs[n-1]), where the notation xs[i] refers to element i in the list xs. The implementation of this function is tail-recursive.

list0_foldleft2

Synopsis

fun
{res:t0p}
{a1,a2:t0p}
list0_foldleft2
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, ini: res, fopr: cfun3(res, a1, a2, res)
) : res // end of [list0_foldleft2]

Description

Given two lists xs1 and xs2 of length n1 and n2, respectively, this function returns the value f (...f (ini, xs1[0], xs2[0])..., xs1[n-1], xs2[n-1]), where n equals min(n1, n2).

list0_foldright

Synopsis

fun{
a:t0p}{res:t0p
} list0_foldright
(
xs: list0(INV(a)), fopr: cfun2(a, res, res), snk: res
) : res // end of [list0_foldright]

Description

Given a list xs of length n, this function returns the value f (xs[0], f (xs[1], ...f (xs[n-1], snk)...)), where the notation xs[i] refers to element i in the list xs. The implementation of this function is not tail-recursive, and stack-overflow may occur if the xs is long (e.g., containing 1,000,000 elements).

Example

The following code gives a standard implementation of the list-append function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
list0_append (xs, ys) = $effmask_all (
  list0_foldright<a><list0(a)> (xs, lam (x, res) => list0_cons (x, res), ys)
) // end of [list0_append]

list0_exists

Synopsis

fun
{a:t0p}
list0_exists
  (xs: list0(INV(a)), pred: cfun(a, bool)): bool

Description

This function returns true if and only if there exists an element in its first argument that satisfies the predicated provided as its second argument.

list0_exists2

Synopsis

fun
{a1,a2:t0p}
list0_exists2
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool)
) : bool // end of [list0_exists2]

Description

Given two lists xs1 and xs2 of length n1 and n2, respectively, this function returns true if and only if p(xs1[i], xs2[i]) returns true for some i between 0 and min(n1,n2)-1, inclusive.

list0_forall

Synopsis

fun
{a:t0p}
list0_forall
  (xs: list0(INV(a)), pred: cfun(a, bool)): bool

Description

This function returns true if and only if every element in its first argument satisfies the predicated provided as its second argument.

Example

The following code tests whether the integers in a given list are all even:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
main (
) = 0 where {
  val xs = list0_of_list ($list{int}(0, 2, 4, 6, 8))
  val isevn = list0_forall<int> (xs, lam (x) => x mod 2 = 0)
  val () = assertloc (isevn)
} // end of [main]

list0_forall2

Synopsis

fun
{a1,a2:t0p}
list0_forall2 (
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool)
) : bool // end of [list0_forall2]

Description

Given two lists xs1 and xs2 of length n1 and n2, respectively, this function returns true if and only if p(xs1[i], xs2[i]) returns true for every i between 0 and min(n1,n2)-1, inclusive.

list0_forall2_eq

Synopsis

fun
{a1,a2:t0p}
list0_forall2_eq
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool), sgn: &int? >> int
) : bool // end of [list0_forall2_eq]

Description

This function is largely similar to list0_forall2. Given two lists xs1 and xs2 of length n1 and n2, respectively, this function returns true if and only if p(xs1[i], xs2[i]) returns true for every i between 0 and min(n1,n2)-1, inclusive. If this function returns true, then the value stored in the call-by-reference parameter sgn equals sgn(n1-n2), that is, the sign of n1-n2. Otherwise, the value equals 0.

Example

The following code implements a function that checks whether two given lists are equal based on a given equality funtion on list elements:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
list0_equal
  (xs1, xs2, eqfn) = let
//
var sgn: int // uninitialied
val ans = list0_forall2_eq (xs1, xs2, eqfn, sgn)
//
in
//
if
sgn = 0
then ans // [xs1] and [xs2] are of the same length
else false // [xs1] and [xs2] are of different length
//
end // end of [list0_equal]

list0_equal

Synopsis

fun
{a:t0p}
list0_equal
(
  xs1: list0(INV(a))
, xs2: list0(INV(a)), eqfn: cfun2(a, a, bool)
) : bool // end of [list0_equal]

Description

Given two lists xs1 and xs2 and a function eqfn, this function returns true if and only if xs1 and xs2 are of the same length and eqfn(xs1[i], xs2[i]) holds for each natural number i less than the length of xs1.

list0_find_exn

Synopsis

fun
{a:t0p}
list0_find_exn
(xs: list0(INV(a)), pred: cfun(a, bool)): (a)

Description

This functions returns the first element in its first argument that satisfies the predicate given as its second argument. In case that such an element does not exist, the function raises an exception (NotFoundExn).

list0_find_opt

Synopsis

fun
{a:t0p}
list0_find_opt
(xs: list0(INV(a)), pred: cfun(a, bool)): Option_vt(a)

Description

This function is the optional version of list0_find_exn.

list0_filter

Synopsis

fun
{a:t0p}
list0_filter
(xs: list0(INV(a)), pred: cfun(a, bool)): list0(a)

Description

This function returns a list consisting of the sequence of elements in its first argument that satisfy the predicate provided as its second argument. Following is a standard implementation of this function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}
list0_filter (xs, p) = let
in
//
case+ xs of
| list0_cons
    (x, xs) =>
    if p(x)
      then list0_cons (x, list0_filter<a> (xs, p))
      else list0_filter<a> (xs, p)
    // end of [if]
| list0_nil() => list0_nil(*void*)
//
end // end of [list0_filter]

However, the implementation of this function in ATSLIB is tail-recursive.

list0_map

Synopsis

fun
{a:t0p}
{b:t0p}
list0_map
(
xs: list0(INV(a)), fopr: cfun(a, b)
) : list0(b) // end of [list0_map]

Description

This function returns a list consisting of the sequence of results obtained from applying its second argument f to each element in its first argument xs. Following is a standard implementation of this function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}{b}
list0_map (xs, f) = let
in
//
case+ xs of
| list0_cons (x, xs) =>
    list0_cons (f x, list0_map (xs, f))
| list0_nil () => list0_nil ()
//
end // end of [list0_map]

However, the implementation of this function in ATSLIB is tail-recursive.

list0_mapopt

Synopsis

fun
{a:t0p}
{b:t0p}
list0_mapopt
(
xs: list0(INV(a)), fopr: cfun(a, Option_vt(b))
) : list0(b) // end of [list0_mapopt]

Description

Given a list xs of length n and a function f, this function returns another list that collects precisely every y whenever Some0(y) is returned by f(xs[i]), where i ranges from 0 until n-1, inclusive. The implementation of this function in ATSLIB is tail-recursive.

list0_mapcons

Synopsis

fun
{a:t0p}
list0_mapcons
(x0: a, xss: list0(list0(INV(a)))): list0(list0(a))

Description

Give an element x0 and a list xss of lists, this function returns another list of lists that can also be obtained by applying list0_map to xss and the function lam(xs) => list0_cons(x0, xs).

list0_imap

Synopsis

fun
{a:t0p}
{b:t0p}
list0_imap
(list0(INV(a)), fopr: cfun2(int, a, b)): list0(b)

Description

Given a list xs, this function returns a list consisting of the sequence of results obtained from applying its second argument f to each pair (i, xs[i]), where i ranges from 0 until the length of xs minus 1, inclusive, and xs[i] refers to element i in the list xs. Following is a standard implementation of this function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement{a}{b}
list0_imap (xs, f) = let
//
fun aux (
  i: int, xs: list0 a, f: cfun2 (int, a, b)
) : list0 b = let
in
  case+ xs of
  | list0_cons
      (x, xs) =>
      list0_cons (f (i, x), aux (i+1, xs, f))
    // end of [list0_cons]
  | list0_nil() => list0_nil(*void*)
end // end of [aux]
//
in
  aux (0, xs, f)
end // end of [list0_imap]

However, the implementation of this function in ATSLIB is tail-recursive.

list0_map2

Synopsis

fun{
a1,
a2:t0p}{b:t0p
} list0_map2
(
  list0(INV(a1)), list0(INV(a2)), fopr: cfun2(a1, a2, b)
) : list0(b) // end of [list0_map2]

Description

This function returns a list consisting of the sequence of results obtained from applying its third argument f to each pair in the zip of the first and second arguments. Following is a standard implementation of this function:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
{a1,a2}{b}
list0_map2
  (xs1, xs2, f) = let
in
//
case+ xs1 of
| list0_nil
    () => list0_nil(*void*)
| list0_cons
    (x1, xs1) => (
  case+ xs2 of
  | list0_nil() => list0_nil(*void*)
  | list0_cons
      (x2, xs2) =>
      list0_cons (f(x1, x2), list0_map2 (xs1, xs2, f))
    // end of [list0_cons]
  ) (* end of [list0_cons] *)
//
end // end of [list0_map2]

However, the implementation of this function in ATSLIB is tail-recursive.

list0_zip

Synopsis

fun
{x,y:t0p}
list0_zip
(
  list0(INV(x)), list0(INV(y))
) :<> list0 @(x, y) // end-of-fun

Description

Given two lists xs and ys of length m and n, respectively, this function returns a list of pairs (xs[i], ys[i]), where i ranges from 0 until min(m,n)-1 and xs[i] (ys[i]) refers to element i in xs (ys).

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
//
implement
{x,y}(*tmp*)
list0_zip (xs, ys) = let
in
//
case+ xs of
| list0_nil
    () => list0_nil(*void*)
| list0_cons
    (x, xs) => (
  case+ ys of
  | list0_nil
      () => list0_nil(*void*)
  | list0_cons
      (y, ys) =>
      list0_cons ((x, y), list0_zip<x,y> (xs, ys))
    // end of [list0_cons]
  ) (* end of [list0_cons] *)
//
end // end of [list0_zip]

However, the implementation of this function in ATSLIB is tail-recursive.

list0_zipwith

Synopsis

macdef
list0_zipwith = list0_map2

Description

This function does exactly the same as list0_map2.

list0_quicksort

Synopsis

fun{a:t0p}
list0_quicksort
(NSH(list0(INV(a))), cmp: (a, a) -<cloref> int):<> list0(a)

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 first argument according to the ordering provided as its second argument.

Example

The following code mergesorts a randomly generated list of integers:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
staload "contrib/libats-hwxi/testing/SATS/randgen.sats"
//
implement
main0 () =
{
#define N 10
typedef T = int
val out = stdout_ref
//
val xs =
list0_of_list
  (randgen_list<T> (N))
//
val () =
  fprint (out, "xs(bef) = ")
val () = fprint_list0_sep (out, xs, ", ")
val () = fprint_newline (out)
//
val xs =
list0_quicksort<T>
  (xs, lam (x1, x2) => compare (x1, x2))
//
val () =
  fprint (out, "xs(aft) = ")
val () = fprint_list0_sep (out, xs, ", ")
val () = fprint_newline (out)
//
} (* end of [main0] *)

list0_mergesort

Synopsis

fun{a:t0p}
list0_mergesort
(NSH(list0(INV(a))), cmp: (a, a) -<cloref> int):<> list0(a)

Description

Mergesort is of time-complexity O(n(log(n))), and it is a stable sorting algorithm. This function mergesorts its first argument according to the ordering implemented by its second argument.

Example

The following code mergesorts a randomly generated list of integers:

//
staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
staload "contrib/libats-hwxi/testing/SATS/randgen.sats"
//
implement
main0 () =
{
#define N 10
typedef T = int
val out = stdout_ref
//
val xs =
list0_of_list
  (randgen_list<T> (N))
//
val () =
  fprint (out, "xs(bef) = ")
val () = fprint_list0_sep (out, xs, ", ")
val () = fprint_newline (out)
//
val xs =
list0_mergesort<T>
  (xs, lam (x1, x2) => compare (x1, x2))
//
val () =
  fprint (out, "xs(aft) = ")
val () = fprint_list0_sep (out, xs, ", ")
val () = fprint_newline (out)
//
} (* end of [main0] *)

Overloaded Symbols

+

Synopsis

overload + with list0_append

[]

Synopsis

overload
[] with list0_get_at_exn // ListSubscriptExn

g0ofg1

Synopsis

overload g0ofg1 with g0ofg1_list

overload g0ofg1 with g0ofg1_list_vt

g1ofg0

Synopsis

overload g1ofg0 with g1ofg0_list

iseqz

Synopsis

overload iseqz with list0_is_empty

isneqz

Synopsis

overload isneqz with list0_isnot_empty

.head

Synopsis

overload .head with list0_head_exn of 0

.tail

Synopsis

overload .tail with list0_tail_exn of 0

length

Synopsis

overload length with list0_length of 0

print

Synopsis

overload print with print_list0

prerr

Synopsis

overload prerr with prerr_list0

fprint

Synopsis

overload fprint with fprint_list0

overload fprint with fprint_list0_sep

overload fprint with fprint_listlist0_sep

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