(*
 *     THE LIST DATATYPE (BUILTIN)
 *
 *     data list A -> C = nil : 1     -> C
 *                      | cons: A * C -> C.
 *
 *)


def reverse: list A -> list A

           = l      => p0 {| nil : ()                     => ([],          l)
                           | cons: (_, (r, cons (a, l'))) => (cons (a, r), l')
                                 | _                      => ([],          l)
                           |}
                              l.


def isEmpty: list A -> bool

           = nil    => true
           | _      => false.


def length: list A -> nat

          = l      => {| nil : ()     => zero
                       | cons: (_, n) => succ n
                       |}
                          l.


def hd: list A      -> SF A

      = nil         => ff
      | cons (a, _) => ss a.


def tl: list A      -> SF list A

      = nil         => ff
      | cons (_, l) => ss l.


def init: list A -> SF list A

    = l => {| nil : ()         => ff
            | cons: (_, ff)    => ss []
                  | (a, ss l') => ss cons (a, l')
            |}
               l.


def last: list A -> SF A

        = l      =>  hd reverse l.


def append: list A * list A -> list A

          = (l1,      l2)   => {| nil : () => l2
                                | cons: p  => cons p
                                |}
                                   l1.


def flatten: list list A -> list A

           = ll          => {| nil : () => []
                             | cons: p  => append p
                             |}
                                ll.


def remove{p: A -> bool}: list A -> list A

    = l => {| nil : ()           => []
            | cons: (a, r) | p a => p1 #
                           | ..  => cons (a, r)
            |}
               l.


def filter{p: A -> bool}: list A -> list A

    = l => {| nil : ()           => []
            | cons: (a, r) | p a => cons (a, r)
                           | ..  => r
            |}
               l.


def takewhile{p: A -> bool}: list A -> list A

    = l => {| nil : ()           => []
            | cons: (a, r) | p a => cons (a, r)
                           | ..  => []
            |}
               l.


def dropwhile{p: A -> bool}: list A -> list A

    = l => {| nil : ()           => []
            | cons: (a, r) | p a => r
                           | ..  => cons #
            |}
               l.


def OR: list bool -> bool

      = lb        => {| nil : ()          => false
                      | cons: (b, r) | b  => true
                                     | .. => r
                      |}
                         lb.


def AND: list bool -> bool

       = lb        => {| nil : ()          => true
                       | cons: (b, r) | b  => r
                                      | .. => false
                       |}
                          lb.


def ADD: list nat -> nat

       = ln       => {| nil : () => zero
                      | cons: pn => add pn
                      |}
                         ln.


def MUL: list nat -> nat

       = ln       => {| nil : () => one
                      | cons: pn => mul pn
                      |}
                         ln.


def rep: nat * A  -> list A

       = (n,   a) => {| zero: () => []
                      | succ: l  => cons (a, l)
                      |}
                         n.


def test_list{p: A -> bool}: list A -> bool

    = l => {| nil : ()           => false
            | cons: (a, r) | p a => true
                           | ..  => r
            |}
               l.


def eq_list{eq_A: A * A -> bool}: list A * list A -> bool

    = (l1, l2) => {| nil : ()           => (fn: nil                        => true
                                              | cons _                     => false
                                           )
                   | cons: (a, (fn: f)) => (fn: nil                        => false
                                              | cons (b, bs) | eq_A (a, b) => f bs
                                                             | ..          => false
                                           )
                   |}
                      l1

    ; (fn: f) => f l2.


def zip: list A * list B -> list (A * B)

    = (l1, l2) => {| nil : ()           => (fn: _            => [])
                   | cons: (a, (fn: f)) => (fn: nil          => []
                                              | cons (b, bs) => cons ((a, b), f bs)
                                           )
                   |}
                      l1

    ; (fn: f) => f l2.


% cartesian product, sub_list (--),
% relational operators (<, >, =>, <=)
% noDups, take, drop, index, max_list, min_list