-- |
-- Module      : Basement.Sized.List
-- License     : BSD-style
-- Maintainer  : Vincent Hanquez <vincent@snarc.org>
-- Stability   : experimental
-- Portability : portable
--
-- A Nat-sized list abstraction
--
-- Using this module is limited to GHC 7.10 and above.
--
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE FlexibleContexts          #-}
module Basement.Sized.List
    ( ListN
    , toListN
    , toListN_
    , unListN
    , length
    , create
    , createFrom
    , empty
    , singleton
    , uncons
    , cons
    , unsnoc
    , snoc
    , index
    , indexStatic
    , updateAt
    , map
    , mapi
    , elem
    , foldl
    , foldl'
    , foldl1'
    , scanl'
    , scanl1'
    , foldr
    , foldr1
    , reverse
    , append
    , minimum
    , maximum
    , head
    , tail
    , init
    , take
    , drop
    , splitAt
    , zip, zip3, zip4, zip5
    , unzip
    , zipWith, zipWith3, zipWith4, zipWith5
    , replicate
    -- * Applicative And Monadic
    , replicateM
    , sequence
    , sequence_
    , mapM
    , mapM_
    ) where

import           Data.Proxy
import qualified Data.List
import           Basement.Compat.Base
import           Basement.Compat.CallStack
import           Basement.Compat.Natural
import           Basement.Nat
import           Basement.NormalForm
import           Basement.Numerical.Additive
import           Basement.Numerical.Subtractive
import           Basement.Types.OffsetSize
import           Basement.Compat.ExtList ((!!))
import qualified Prelude
import qualified Control.Monad as M (replicateM, mapM, mapM_, sequence, sequence_)

impossible :: HasCallStack => a
impossible = error "ListN: internal error: the impossible happened"

-- | A Typed-level sized List equivalent to [a]
newtype ListN (n :: Nat) a = ListN { unListN :: [a] }
    deriving (Eq,Ord,Typeable,Generic)

instance Show a => Show (ListN n a) where
    show (ListN l) = show l

instance NormalForm a => NormalForm (ListN n a) where
    toNormalForm (ListN l) = toNormalForm l

-- | Try to create a ListN from a List, succeeding if the length is correct
toListN :: forall (n :: Nat) a . (KnownNat n, NatWithinBound Int n) => [a] -> Maybe (ListN n a)
toListN l
    | expected == Prelude.fromIntegral (Prelude.length l) = Just (ListN l)
    | otherwise                                           = Nothing
  where
    expected = natValInt (Proxy :: Proxy n)

-- | Create a ListN from a List, expecting a given length
--
-- If this list contains more or less than the expected length of the resulting type,
-- then an asynchronous error is raised. use 'toListN' for a more friendly functions
toListN_ :: forall n a . (HasCallStack, NatWithinBound Int n, KnownNat n) => [a] -> ListN n a
toListN_ l
    | expected == got = ListN l
    | otherwise       = error ("toListN_: expecting list of " <> show expected <> " elements, got " <> show got <> " elements")
  where
    expected = natValInt (Proxy :: Proxy n)
    got      = Prelude.length l

-- | performs a monadic action n times, gathering the results in a List of size n.
replicateM :: forall (n :: Nat) m a . (NatWithinBound Int n, Monad m, KnownNat n) => m a -> m (ListN n a)
replicateM action = ListN <$> M.replicateM (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) action

-- | Evaluate each monadic action in the list sequentially, and collect the results.
sequence :: Monad m => ListN n (m a) -> m (ListN n a)
sequence (ListN l) = ListN <$> M.sequence l

-- | Evaluate each monadic action in the list sequentially, and ignore the results.
sequence_ :: Monad m => ListN n (m a) -> m ()
sequence_ (ListN l) = M.sequence_ l

-- | Map each element of a List to a monadic action, evaluate these
-- actions sequentially and collect the results
mapM :: Monad m => (a -> m b) -> ListN n a -> m (ListN n b)
mapM f (ListN l) = ListN <$> M.mapM f l

-- | Map each element of a List to a monadic action, evaluate these
-- actions sequentially and ignore the results
mapM_ :: Monad m => (a -> m b) -> ListN n a -> m ()
mapM_ f (ListN l) = M.mapM_ f l

-- | Create a list of n elements where each element is the element in argument
replicate :: forall (n :: Nat) a . (NatWithinBound Int n, KnownNat n) => a -> ListN n a
replicate a = ListN $ Prelude.replicate (Prelude.fromIntegral $ natVal (Proxy :: Proxy n)) a

-- | Decompose a list into its head and tail.
uncons :: (1 <= n) => ListN n a -> (a, ListN (n-1) a)
uncons (ListN (x:xs)) = (x, ListN xs)
uncons _ = impossible

-- | prepend an element to the list
cons :: a -> ListN n a -> ListN (n+1) a
cons a (ListN l) = ListN (a : l)

-- | Decompose a list into its first elements and the last.
unsnoc :: (1 <= n) => ListN n a -> (ListN (n-1) a, a)
unsnoc (ListN l) = (ListN $ Data.List.init l, Data.List.last l)

-- | append an element to the list
snoc :: ListN n a -> a -> ListN (n+1) a
snoc (ListN l) a = ListN (l Prelude.++ [a])

-- | Create an empty list of a
empty :: ListN 0 a
empty = ListN []

-- | Get the length of a list
length :: forall a (n :: Nat) . (KnownNat n, NatWithinBound Int n) => ListN n a -> CountOf a
length _ = CountOf $ natValInt (Proxy :: Proxy n)

-- | Create a new list of size n, repeately calling f from 0 to n-1
create :: forall a (n :: Nat) . KnownNat n => (Natural -> a) -> ListN n a
create f = ListN $ Prelude.map (f . Prelude.fromIntegral) [0..(len-1)]
  where
    len = natVal (Proxy :: Proxy n)

-- | Same as create but apply an offset
createFrom :: forall a (n :: Nat) (start :: Nat) . (KnownNat n, KnownNat start)
           => Proxy start -> (Natural -> a) -> ListN n a
createFrom p f = ListN $ Prelude.map (f . Prelude.fromIntegral) [idx..(idx+len-1)]
  where
    len = natVal (Proxy :: Proxy n)
    idx = natVal p

-- | create a list of 1 element
singleton :: a -> ListN 1 a
singleton a = ListN [a]

-- | Check if a list contains the element a
elem :: Eq a => a -> ListN n a -> Bool
elem a (ListN l) = Prelude.elem a l

-- | Append 2 list together returning the new list
append :: ListN n a -> ListN m a -> ListN (n+m) a
append (ListN l1) (ListN l2) = ListN (l1 <> l2)

-- | Get the maximum element of a list
maximum :: (Ord a, 1 <= n) => ListN n a -> a
maximum (ListN l) = Prelude.maximum l

-- | Get the minimum element of a list
minimum :: (Ord a, 1 <= n) => ListN n a -> a
minimum (ListN l) = Prelude.minimum l

-- | Get the head element of a list
head :: (1 <= n) => ListN n a -> a
head (ListN (x:_)) = x
head _ = impossible

-- | Get the tail of a list
tail :: (1 <= n) => ListN n a -> ListN (n-1) a
tail (ListN (_:xs)) = ListN xs
tail _ = impossible

-- | Get the list with the last element missing
init :: (1 <= n) => ListN n a -> ListN (n-1) a
init (ListN l) = ListN $ Data.List.init l

-- | Take m elements from the beggining of the list.
--
-- The number of elements need to be less or equal to the list in argument
take :: forall a (m :: Nat) (n :: Nat) . (KnownNat m, NatWithinBound Int m, m <= n) => ListN n a -> ListN m a
take (ListN l) = ListN (Prelude.take n l)
  where n = natValInt (Proxy :: Proxy m)

-- | Drop elements from a list keeping the m remaining elements
drop :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> ListN m a
drop (ListN l) = ListN (Prelude.drop n l)
  where n = natValInt (Proxy :: Proxy d)

-- | Split a list into two, returning 2 lists
splitAt :: forall a d (m :: Nat) (n :: Nat) . (KnownNat d, NatWithinBound Int d, (n - m) ~ d, m <= n) => ListN n a -> (ListN m a, ListN (n-m) a)
splitAt (ListN l) = let (l1, l2) = Prelude.splitAt n l in (ListN l1, ListN l2)
  where n = natValInt (Proxy :: Proxy d)

-- | Get the i'th elements
--
-- This only works with TypeApplication:
--
-- > indexStatic @1 (toListN_ [1,2,3] :: ListN 3 Int)
indexStatic :: forall i n a . (KnownNat i, CmpNat i n ~ 'LT, Offsetable a i) => ListN n a -> a
indexStatic (ListN l) = l !! (natValOffset (Proxy :: Proxy i))

-- | Get the i'the element
index :: ListN n ty -> Offset ty -> ty
index (ListN l) ofs = l !! ofs

-- | Update the value in a list at a specific location
updateAt :: forall n a
         .  Offset a
         -> (a -> a)
         -> ListN n a
         -> ListN n a
updateAt o f (ListN l) = ListN (doUpdate 0 l)
  where doUpdate _ []     = []
        doUpdate i (x:xs)
            | i == o      = f x : xs
            | otherwise   = x : doUpdate (i+1) xs

-- | Map all elements in a list
map :: (a -> b) -> ListN n a -> ListN n b
map f (ListN l) = ListN (Prelude.map f l)

-- | Map all elements in a list with an additional index
mapi :: (Natural -> a -> b) -> ListN n a -> ListN n b
mapi f (ListN l) = ListN . loop 0 $ l
  where loop _ []     = []
        loop i (x:xs) = f i x : loop (i+1) xs

-- | Fold all elements from left
foldl :: (b -> a -> b) -> b -> ListN n a -> b
foldl f acc (ListN l) = Prelude.foldl f acc l

-- | Fold all elements from left strictly
foldl' :: (b -> a -> b) -> b -> ListN n a -> b
foldl' f acc (ListN l) = Data.List.foldl' f acc l

-- | Fold all elements from left strictly with a first element
-- as the accumulator
foldl1' :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldl1' f (ListN l) = Data.List.foldl1' f l

-- | Fold all elements from right
foldr :: (a -> b -> b) -> b -> ListN n a -> b
foldr f acc (ListN l) = Prelude.foldr f acc l

-- | Fold all elements from right assuming at least one element is in the list.
foldr1 :: (1 <= n) => (a -> a -> a) -> ListN n a -> a
foldr1 f (ListN l) = Prelude.foldr1 f l

-- | 'scanl' is similar to 'foldl', but returns a list of successive
-- reduced values from the left
--
-- > scanl f z [x1, x2, ...] == [z, z `f` x1, (z `f` x1) `f` x2, ...]
scanl' :: (b -> a -> b) -> b -> ListN n a -> ListN (n+1) b
scanl' f initialAcc (ListN start) = ListN (go initialAcc start)
  where
    go !acc l = acc : case l of
                        []     -> []
                        (x:xs) -> go (f acc x) xs

-- | 'scanl1' is a variant of 'scanl' that has no starting value argument:
--
-- > scanl1 f [x1, x2, ...] == [x1, x1 `f` x2, ...]
scanl1' :: (a -> a -> a) -> ListN n a -> ListN n a
scanl1' f (ListN l) = case l of
                        []     -> ListN []
                        (x:xs) -> ListN $ Data.List.scanl' f x xs

-- | Reverse a list
reverse :: ListN n a -> ListN n a
reverse (ListN l) = ListN (Prelude.reverse l)

-- | Zip 2 lists of the same size, returning a new list of
-- the tuple of each elements
zip :: ListN n a -> ListN n b -> ListN n (a,b)
zip (ListN l1) (ListN l2) = ListN (Prelude.zip l1 l2)

-- | Unzip a list of tuple, to 2 List of the deconstructed tuples
unzip :: ListN n (a,b) -> (ListN n a, ListN n b)
unzip l = (map fst l, map snd l)

-- | Zip 3 lists of the same size
zip3 :: ListN n a -> ListN n b -> ListN n c -> ListN n (a,b,c)
zip3 (ListN x1) (ListN x2) (ListN x3) = ListN (loop x1 x2 x3)
  where loop (l1:l1s) (l2:l2s) (l3:l3s) = (l1,l2,l3) : loop l1s l2s l3s
        loop []       _        _        = []
        loop _        _        _        = impossible

-- | Zip 4 lists of the same size
zip4 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n (a,b,c,d)
zip4 (ListN x1) (ListN x2) (ListN x3) (ListN x4) = ListN (loop x1 x2 x3 x4)
  where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) = (l1,l2,l3,l4) : loop l1s l2s l3s l4s
        loop []       _        _        _        = []
        loop _        _        _        _        = impossible

-- | Zip 5 lists of the same size
zip5 :: ListN n a -> ListN n b -> ListN n c -> ListN n d -> ListN n e -> ListN n (a,b,c,d,e)
zip5 (ListN x1) (ListN x2) (ListN x3) (ListN x4) (ListN x5) = ListN (loop x1 x2 x3 x4 x5)
  where loop (l1:l1s) (l2:l2s) (l3:l3s) (l4:l4s) (l5:l5s) = (l1,l2,l3,l4,l5) : loop l1s l2s l3s l4s l5s
        loop []       _        _        _        _        = []
        loop _        _        _        _        _        = impossible

-- | Zip 2 lists using a function
zipWith :: (a -> b -> x) -> ListN n a -> ListN n b -> ListN n x
zipWith f (ListN (v1:vs)) (ListN (w1:ws)) = ListN (f v1 w1 : unListN (zipWith f (ListN vs) (ListN ws)))
zipWith _ (ListN [])       _ = ListN []
zipWith _ _                _ = impossible

-- | Zip 3 lists using a function
zipWith3 :: (a -> b -> c -> x)
         -> ListN n a
         -> ListN n b
         -> ListN n c
         -> ListN n x
zipWith3 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) =
    ListN (f v1 w1 x1 : unListN (zipWith3 f (ListN vs) (ListN ws) (ListN xs)))
zipWith3 _ (ListN []) _       _ = ListN []
zipWith3 _ _          _       _ = impossible

-- | Zip 4 lists using a function
zipWith4 :: (a -> b -> c -> d -> x)
         -> ListN n a
         -> ListN n b
         -> ListN n c
         -> ListN n d
         -> ListN n x
zipWith4 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) =
    ListN (f v1 w1 x1 y1 : unListN (zipWith4 f (ListN vs) (ListN ws) (ListN xs) (ListN ys)))
zipWith4 _ (ListN []) _       _       _ = ListN []
zipWith4 _ _          _       _       _ = impossible

-- | Zip 5 lists using a function
zipWith5 :: (a -> b -> c -> d -> e -> x)
         -> ListN n a
         -> ListN n b
         -> ListN n c
         -> ListN n d
         -> ListN n e
         -> ListN n x
zipWith5 f (ListN (v1:vs)) (ListN (w1:ws)) (ListN (x1:xs)) (ListN (y1:ys)) (ListN (z1:zs)) =
    ListN (f v1 w1 x1 y1 z1 : unListN (zipWith5 f (ListN vs) (ListN ws) (ListN xs) (ListN ys) (ListN zs)))
zipWith5 _ (ListN []) _       _       _       _ = ListN []
zipWith5 _ _          _       _       _       _ = impossible