module Data.List 
export  { singleton;    replicate
        ; enumFromTo
        ; append
        ; length
        ; head
        ; tail; tail1
        ; last; index
        ; reverse 
        ; map;    mapS
        ; forS
        ; zipWith; zipWithS
        ; foldl;  foldlS;       sum;    prod
        ; foldr;  foldrS
        ; scanl
        ; filter; filterS
        ; any }
import  Data.Numeric.Nat
where

-- | Standard Cons-lists.
data List (a: Data) where
        Nil     : List a
        Cons    : a -> List a -> List a


-- Constructors ---------------------------------------------------------------
-- | Construct a list containing a single element.
singleton (x: a): List a
 = Cons x Nil


-- | Construct a list of the given length where all elements are'
--   the same value.
replicate (n: Nat#) (x: a): List a
 | n == 0       = Nil
 | otherwise    = Cons x (replicate (n - 1) x)


-- | Construct a range of values.
enumFromTo (start: Nat#) (end: Nat#): List Nat#
 | start >= end = singleton start
 | otherwise    = Cons start (enumFromTo (start + 1) end)


-- | Append two lists.
append (xx yy: List a): List a
 = case xx of
        Nil             -> yy
        Cons x xs       -> Cons x (append xs yy)


-- Projections ----------------------------------------------------------------
-- | Take the length of a list.
length (xx: List a): Nat#
 = case xx of
        Nil             -> 0
        Cons x xs       -> 1 + length xs


-- | Take the head of a list, if there is one.
head (def: a) (xx: List a): a
 = case xx of
        Nil             -> def
        Cons x xs       -> x


-- | Take the tail of a list, if there is one.
tail (def: List a) (xx: List a): List a
 = case xx of
        Nil             -> def
        Cons x xs       -> xs


-- | Like `tail`, but if there is only one element then keep it.
tail1   (def: a) (xx: List a): List a
 = case xx of
        Nil             -> singleton def
        Cons x xs        
         -> case xs of
                Nil     -> singleton x
                _       -> xs


-- | Take the last element of a list, if there is one.
last (def: a) (xx: List a): a
 = case xx of
        Nil                     -> def
        Cons x xs
         -> case xs of
                Nil             -> x
                Cons y ys       -> last def xs


index (def: a) (n: Nat#) (xx: List a): a
 = case xx of   
        Nil     -> def
        Cons x xs 
         -> case n of
                0       -> x
                _       -> index def (n - 1) xs


-- Transforms -----------------------------------------------------------------
-- | Reverse the elements of a list.
--   This is a naive O(n^2) version for testing purposes.
reverse (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs       -> append (reverse xs) (singleton x)


-- Maps -----------------------------------------------------------------------
-- | Apply a worker function to every element of a list, yielding a new list.
map     (f: a -> b) (xx: List a): List b
 = case xx of
        Nil             -> Nil
        Cons x xs       -> Cons (f x) (map f xs)


-- | Apply a stateful worker function to every element of a list,
--   yielding a new list. 
--   The worker is applied to the source elements left-to-right.
mapS    (f: a -> S e b) (xx: List a): S e (List b)
 = case xx of
        Nil             -> Nil
        Cons x xs       -> Cons (f x) (mapS f xs)


-- | Apply a function to all elements of a list, yielding nothing.
forS (xx: List a) (f: a -> S e Unit): S e Unit
 = case xx of
        Nil     -> ()
        Cons x xs       
         -> do  f x
                forS xs f


-- Zips -----------------------------------------------------------------------
zipWith (f: a -> b -> c) 
        (xx: List a) (yy: List b): List c
 = case xx of
        Nil     -> Nil
        Cons x xs
         -> case yy of
                Cons y ys
                 -> Cons (f x y) (zipWith f xs ys)

                Nil -> Nil


zipWithS (f: a -> b -> S e c) 
         (xx: List a) (yy: List b): S e (List c)
 = case xx of
        Nil     -> Nil
        Cons x xs
         -> case yy of
                Cons y ys
                 -> Cons (f x y) (zipWithS f xs ys)

                Nil -> Nil


-- Folds ----------------------------------------------------------------------
-- | Reduce a list with a binary function and zero value, 
--   from left to right.
foldl (f: b -> a -> b) (z: b) (xx: List a): b
 = case xx of
        Nil             -> z
        Cons x xs       -> foldl f (f z x) xs


-- | Reduce a list with a stateful binary function and zero value, 
--   from left to right.
foldlS (f: b -> a -> S e b) (z: b) (xx: List a): S e b
 = case xx of
        Nil             -> z
        Cons x xs       -> foldlS f (f z x) xs


-- | Reduce a list with a binary function and zero value,
--   from right to left.
foldr (f: a -> b -> b) (z: b) (xx: List a): b
 = case xx of
        Nil             -> z
        Cons x xs       -> f x (foldr f z xs)


-- | Reduce a list with a stateful binary function and zero value, 
--   from right to left.
foldrS (f: a -> b -> S e b) (z: b) (xx: List a): S e b
 = case xx of
        Nil             -> z
        Cons x xs       -> f x (foldrS f z xs)


-- | Take the sum of a list of Nats.
sum (xs: List Nat#): Nat#
 = foldl (+) 0 xs


-- | Take the product of a list of Nats.
prod (xs: List Nat#): Nat#
 = foldl (*) 1 xs


-- Scans ----------------------------------------------------------------------
scanl (f: b -> a -> b) (acc: b) (xx: List a): List b
 = case xx of
        Nil     
         -> Cons acc Nil

        Cons x xs
         -> let acc' = f acc x
            in  Cons acc (scanl f acc' xs)


-- Filters --------------------------------------------------------------------
-- | Keep only those elements that match the given predicate.
filter (p: a -> Bool#) (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs  
         -> if p x 
                then Cons x (filter p xs)
                else filter p xs


-- | Keep only those elements that match the given stateful predicate.
--   The predicate is applied to the list elements from left to right.
filterS (p: a -> S e Bool#) (xx: List a): S e (List a)
 = case xx of
        Nil             -> Nil
        Cons x xs  
         -> if p x 
                then Cons x (filterS p xs)
                else filterS p xs


-- | Check if any of the members of the list match the given predicate.
any (p: a -> Bool#) (xx: List a): Bool#
 = case xx of
        Nil
         -> False

        Cons x xs 
         | p x          -> True
         | otherwise    -> any p xs