{-# 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 Data.Bool
import Data.Eq (Eq(..))
import Data.Foldable (Foldable)
import Data.Functor (Functor(..))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord(..))
import Data.Proxy (Proxy(..))
import Data.Traversable (Traversable(..))
import GHC.TypeNats
import Numeric.Natural (Natural)
import Prelude (fromIntegral, error)
import Text.Show (Show(..))
import qualified Data.List as List

-- * 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)
uncons (ML []) = error "MeasuredList.uncons: impossible happened"

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)