module Data.List 
export
{       singleton;  replicate;
        enumFromTo; append; concat;
        length;
        head;
        tail; tail1;
        last; index;
        lookupBy; find;
        reverse;
        map; mapS; for;
        forS;
        zipWith; zipWithS;
        foldl;  foldlS;       sum;    prod;
        foldr;  foldrS;
        scanl;
        filter; filterS;
        any;
}
import  Data.Numeric.Nat
import  Data.Numeric.Bool
import  Data.Tuple
import  Data.Maybe
import  Data.Function
import  Class.Functor
import  Class.Monad
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)


-- | Concatenate a list of lists.
concat (xss0: List (List a)): List a
 = case xss0 of
        Nil             -> Nil
        Cons xs xss1    -> go xs xss1
 where
        go Nil         Nil              = Nil
        go Nil         (Cons xs' xss')  = go xs' xss'
        go (Cons x xs) xss              = Cons x (go xs xss)


-- | Generate a list of the given length by repeatedly 
--   applying a stateful function.
unfold   (s0: s) (f: s -> Maybe (Tup2 a s)): List a
 = case f s0 of
        Nothing         -> Nil
        Just (T2 a s1)  -> Cons a (unfold s1 f)


generate (len: Nat) (f: Nat -> a): List a
 = unfold 0
 $ (\ix -> if ix >= len 
                then Nothing
                else Just (T2 (f ix) (ix + 1)))


-- 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 Nil      -> singleton x
        Cons _ xs       -> 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 Nil              -> x
        Cons x (Cons y ys)      -> last def (Cons y ys)


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


-- Searches -------------------------------------------------------------------
-- | Given a list of key value pairs, lookup the first
--   value whose key is selected by the given predicate.
lookupBy (f: a -> Bool) (xx: List (Tup2 a b)): Maybe b
 = case xx of
        Nil             -> Nothing
        Cons (T2 x y) xs
         | f x          -> Just y
         | otherwise    -> lookupBy f xs


-- | Find the first element in a list that matches the given predicate.
find (f: a -> Bool) (xx: List a): Maybe a
 = case xx of
        Nil             -> Nothing
        Cons x xs
         | f x          -> Just x
         | otherwise    -> find f 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)


-- | Like `map`, but with the arguments swapped.
for     (xx: List a) (f: a -> b): List b
 = case xx of
        Nil             -> Nil
        Cons x xs       -> Cons (f x) (for xs f)


-- | Functor instance for List.
functor_list 
 = Functor map


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


-- | Monadic map.
mapM    (dMonad: Monad m) 
        (f: a -> m b) (xx: List a): m (List b)
 = case xx of
        Nil    
         -> return dMonad Nil

        Cons x xs
         -> bind   dMonad (f x)              $ λx'
         -> bind   dMonad (mapM dMonad f xs) $ λxs'
         -> return dMonad (Cons x' xs')


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


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


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


-- | Monadic sequence.
sequence (dMonad: Monad m) (xs: List (m a)): m (List a)
 = mapM dMonad id 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  
         | p x          -> Cons x (filter p xs)
         | otherwise    -> 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  
         | p x          -> Cons x (filterS p xs)
         | otherwise    -> 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