{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Utils.MeasuredList
 ( type MeasuredList
 , pattern (:#)
 , cons
 , uncons
 , head
 , tail
 , concat
 , reverse
 , length
 , splitAt
 , fromList
 , zip
 , zipWith
 ) where

import Control.Applicative (Applicative(..))
import Data.Bool
import Data.Eq (Eq(..))
import Data.Foldable (Foldable)
import Data.Function ((.), flip)
import Data.Functor (Functor(..), (<$>))
import Data.Int (Int)
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..))
import Data.Ord (Ord(..), Ordering(..))
import Data.Proxy (Proxy(..))
import Data.Traversable (Traversable(..))
import Data.Tuple (fst, snd)
import Data.Type.Equality ((:~:)(..))
import GHC.TypeNats
import Numeric.Natural (Natural)
import Prelude ((-), undefined, fromIntegral)
import Text.Show (Show(..))
import Unsafe.Coerce (unsafeCoerce)
import qualified Control.Monad.Trans.State.Strict as S
import qualified Data.ByteString as BS
import qualified Data.List as List

import Utils.Constraint
import Utils.Natural

-- * Type 'List'
-- | A list whose length is known at the type-level.
newtype MeasuredList (n::Nat) a = ML [a]
 deriving (Eq,Ord,Functor,Foldable,Traversable)
instance Show a => Show (MeasuredList n a) where
	showsPrec p (ML xs) = showsPrec p xs

cons :: a -> MeasuredList n a -> MeasuredList (n+1) a
cons x (ML xs) = ML (x:xs)
uncons :: (1<=n) => MeasuredList n a -> (a, MeasuredList (n-1) a)
uncons (ML (x:xs)) = (x, ML xs)

pattern (:#) :: (1<=n) => a -> MeasuredList (n-1) a -> MeasuredList n a
pattern (:#) x xs <- (uncons -> (x,xs))
 where  (:#) x xs | ML l <- cons x xs = ML l
infixr 5 :#

fromList :: forall n a. KnownNat n => [a] -> Maybe (MeasuredList n a)
fromList xs | List.length xs == fromIntegral (natVal (Proxy::Proxy n)) = Just (ML xs)
            | otherwise = Nothing

head :: (1<=n) => MeasuredList n a -> a
head (ML xs) = List.head xs
tail :: (1<=n) => MeasuredList n a -> MeasuredList (n-1) a
tail (ML xs) = ML (List.tail xs)
concat :: MeasuredList n a -> MeasuredList m a -> MeasuredList (n+m) a
concat (ML xs) (ML ys) = ML (xs List.++ ys)
reverse :: MeasuredList n a -> MeasuredList n a
reverse (ML xs) = ML (List.reverse xs)
length :: forall n a. KnownNat n => MeasuredList n a -> Natural
length _xs = natVal (Proxy::Proxy n)

splitAt :: forall i n a proxy.
 KnownNat i => (i<=n) =>
 proxy i -> MeasuredList n a -> (MeasuredList i a, MeasuredList (n-i) a)
splitAt _i (ML xs) = (ML ls, ML rs)
	where
	(ls,rs) = List.splitAt i xs
	i = fromIntegral (natVal (Proxy::Proxy i))

zip :: MeasuredList n a -> MeasuredList n b -> MeasuredList n (a,b)
zip (ML as) (ML bs) = ML (List.zip as bs)
zipWith :: (a -> b -> c) -> MeasuredList n a -> MeasuredList n b -> MeasuredList n c
zipWith f (ML as) (ML bs) = ML (List.zipWith f as bs)