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
  • g0ofg1_list
  • g1ofg0_list
  • list0_make_sing
  • list0_make_pair
  • list0_make_elt
  • list0_make_intrange
  • list0_make_intrange_lr
  • list0_make_intrange_lrd
  • list0_make_arrpsz
  • list0_is_nil
  • list0_is_cons
  • list0_is_empty
  • list0_isnot_empty
  • list0_head_exn
  • list0_head_opt
  • list0_tail_exn
  • list0_tail_opt
  • list0_last_exn
  • list0_last_opt
  • list0_nth_exn
  • list0_nth_opt
  • list0_get_at_exn
  • print_list0
  • prerr_list0
  • fprint_list0
  • fprint_list0_sep
  • list0_insert_at_exn
  • list0_remove_at_exn
  • list0_takeout_at_exn
  • list0_length
  • list0_append
  • list0_extend
  • list0_snoc
  • list0_reverse
  • list0_reverse_append
  • list0_concat
  • list0_take_exn
  • list0_drop_exn
  • list0_tabulate
  • list0_tabulate_opt
  • list0_app
  • list0_foreach
  • list0_iforeach
  • list0_foreach2
  • list0_foreach2_eq
  • list0_foldleft
  • list0_ifoldleft
  • list0_foldleft2
  • list0_foldright
  • list0_exists
  • list0_exists2
  • list0_forall
  • list0_forall2
  • list0_forall2_eq
  • list0_equal
  • list0_find_exn
  • list0_find_opt
  • list0_filter
  • list0_map
  • list0_mapopt
  • list0_mapcons
  • list0_imap
  • list0_map2
  • list0_zip
  • list0_zipwith
  • list0_quicksort
  • list0_mergesort
  • Overloaded Symbols
  • +
  • []
  • g0ofg1
  • g1ofg0
  • iseqz
  • isneqz
  • .head
  • .tail
  • length
  • print
  • prerr
  • fprint

  • 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}(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)), i: 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)), i: 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
    (
      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
      (list0(INV(a)), ini: res, fopr: cfun2(res, a, res)): res

    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
      (list0(INV(a)), ini: res, fopr: cfun3(res, int, a, res)): res

    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

    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))
    , p: 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
      (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-function

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

    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

    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. SourceForge.net Logo