List.ds

module Data.List
export
{       eq_List;
        singleton;  replicate;
        enumFromTo; append; concat;
        unfold; generate; intersperse;
        null;
        length;
        head; init;
        tail; tail1;
        last;
        index; takeIndex;
        take; takeWhile;
        drop; dropWhile;
        elem;
        lookup; find;
        minimum; maximum;
        reverse;
        map; mapS; mapM; mapMaybe;
        for; forS;
        zip;
        zipWith; zipWithS;
        foldl;  foldlS;       sum;    prod;     sequence;
        foldr;  foldrS;
        scanl;
        filter; filterS;
        all; any;
}
import Data.Numeric.Nat
import Data.Numeric.Bool
import Data.Tuple
import Data.Maybe
import Data.Function
import Class.Numeric
import Class.Category
import Class.Functor
import Class.Monad
import Class.Ord
import Class.Eq
where


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


-- Dictionaries ---------------------------------------------------------------
eq_List {eqa: Eq a}: Eq (List a)
 = Eq eq' neq'
 where

        eq' {@b: Data} {Eq b} (xx: List b) (yy: List b): Bool
         = case (xx, yy) of
                (Nil,           Nil)            -> True
                (Cons x1 xs,    Cons y1 ys)
                 | x1 == y1                     -> eq' xs ys
                 | otherwise                    -> False
                (_, _)                          -> False

        neq' {@b: Data} {Eq b} (xx: List b) (yy: List b): Bool
         = case (xx, yy) of
                (Nil,           Nil)            -> False
                (Cons x1 xs,    Cons y1 ys)
                 | x1 == y1                     -> neq' xs ys
                 | otherwise                    -> True
                (_, _)                          -> True


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


-- | Intersperse the given element between all elements of a list.
intersperse (c: a) (xx: List a): List a
 = case xx of
        Nil
         -> Nil

        Cons x Nil
         -> Cons x Nil

        Cons x (Cons y xs)
         -> Cons x (Cons c (intersperse c (Cons y xs)))


-- Projections ----------------------------------------------------------------
-- | Check if a list is empty
null   (xx: List a): Bool
 = case xx of
        Nil             -> True
        _               -> False


-- | 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 initial part of a list, not including the final element.
init (def: List a) (xx: List a): List a
 = case xx of
        Nil             -> def
        Cons x xs
         -> case xs of
                Nil             -> Nil
                Cons x2 xs2     -> Cons x (init def (Cons x2 xs2))


-- | 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 (xx: List a): Maybe a
 = case xx of
        Nil                     -> Nothing
        Cons x Nil              -> Just x
        Cons x (Cons y ys)      -> last (Cons y ys)


-- | Get a numbered element from a list,
--   returning a default value if we try to index off the end of the list.
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


-- | Get a numbered element from a list,
--   or Nothing
takeIndex (n: Nat) (xx: List a): Maybe a
 = case xx of
        Nil     -> Nothing
        Cons x xs
         -> case n of
                0       -> Just x
                _       -> takeIndex (n - 1) xs


-- | Take the given number of elements from the front of a list.
take  (n: Nat) (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs
         | n == 0       -> Nil
         | otherwise    -> Cons x (take (n - 1) xs)


-- | Take elements from the front of a list while they match
--   the given predicate.
takeWhile (f: a -> Bool) (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs
         | f x          -> Cons x (takeWhile f xs)
         | otherwise    -> Nil


-- | Drop the given number of elements from the front of a list.
drop  (n: Nat) (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs
         | n == 0       -> xx
         | otherwise    -> drop (n - 1) xs


-- | Drop elements from the front of a list while they match
--   the given predicate.
dropWhile (f: a -> Bool) (xx: List a): List a
 = case xx of
        Nil             -> Nil
        Cons x xs
          | f x         -> dropWhile f xs
          | otherwise   -> xx


-- Searches -------------------------------------------------------------------
-- | Check if the given element is an element of the list.
elem   {Eq a} (k: a) (xx: List a): Bool
 = case xx of
        Nil             -> False
        Cons x xs
         | x == k       -> True
         | otherwise    -> elem k xs


-- | Given a list of key value pairs, lookup the first
--   value whose key is selected by the given predicate.
lookup {Eq a} (k: a) (xx: List (Tup2 a b)): Maybe b
 = case xx of
        Nil             -> Nothing
        Cons (T2 k' y) xs
         | k == k'      -> Just y
         | otherwise    -> lookup k 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


-- | Take the maximum element of a list.
minimum {Ord a} (xx: List a): Maybe a
 = case xx of
        Nil        -> Nothing
        Cons x1 xs -> go x1 xs
 where
        go x1 Nil       = Just x1
        go x1 (Cons x2 xs)
         | x2 < x1      = go x2 xs
         | otherwise    = go x1 xs


-- | Take the maximum element of a list.
maximum {Ord a} (xx: List a): Maybe a
 = case xx of
        Nil        -> Nothing
        Cons x1 xs -> go x1 xs
 where
        go x1 Nil       = Just x1
        go x1 (Cons x2 xs)
         | x2 > x1      = go x2 xs
         | otherwise    = go x1 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)


-- | Like map, but the worker doesn't always produce an element.
mapMaybe (f: a -> Maybe b) (xx: List a): List b
 = case xx of
        Nil             -> Nil
        Cons x xs
         -> case f x of
                Nothing -> mapMaybe f xs
                Just x' -> Cons x' (mapMaybe 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


-- | Zip two lists component-wise into a list of tuples.
zip : {@a b: Data} -> List a -> List b -> List (Tup2 a b)
zip _   Nil                     = Nil
zip Nil _                       = Nil
zip (Cons a as) (Cons b bs)     = Cons (T2 a b) (zip as bs)


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

        Cons x xs
         -> bind   (f x)       $ λx'
         -> bind   (mapM f xs) $ λxs'
         -> return (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 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 all the members of the list match the given predicate.
all (p: a -> Bool) (xx: List a): Bool
 = case xx of
        Nil             -> True

        Cons x xs
         | p x          -> all p xs
         | otherwise    -> False


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