{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE TupleSections #-}

{-# LANGUAGE NoStarIsType #-}

-- |
-- Module      : OAlg.Entity.FinList
-- Description : finite lists, parameterized by there length.
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- finite lists, parameterized by there length.
module OAlg.Entity.FinList
  (
    -- * FinList
    FinList(..), toW, head, tail, zip, zip3, (|:), (++), (**), repeat
  , iFinList, iFinList0, iFinList', toArray

  , someFinList, SomeFinList(..), (<++>)

    -- ** Induction
  , inductionS, FinList'(..)
  )

  where

import Control.Monad (Functor(..))

import Data.Typeable
import Data.Foldable
import Data.Array as A
import qualified Data.List as L

import OAlg.Prelude

import OAlg.Entity.Natural hiding ((++),(**))

--------------------------------------------------------------------------------
-- FinList - 
infixr 5 :|

-- | finite lists, parameterized by there length.
data FinList (n :: N') a where
  Nil  :: FinList N0 a
  (:|) :: a -> FinList n a -> FinList (n+1) a

----------------------------------------
-- FinList - Entity -
deriving instance Show a => Show (FinList n a)
deriving instance Eq a => Eq (FinList n a)
deriving instance Foldable (FinList n)
deriving instance Typeable (FinList n a)
deriving instance Ord x => Ord (FinList n x)

instance Functor (FinList n) where
  fmap :: forall a b. (a -> b) -> FinList n a -> FinList n b
fmap a -> b
_ FinList n a
Nil     = forall a. FinList 'N0 a
Nil
  fmap a -> b
f (a
a:|FinList n a
as) = a -> b
f a
a forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList n a
as

instance Validable a => Validable (FinList n a) where
  valid :: FinList n a -> Statement
valid FinList n a
as = forall a (n :: N'). Validable a => N -> FinList n a -> Statement
vld N
0 FinList n a
as where
    vld :: Validable a => N -> FinList n a -> Statement
    vld :: forall a (n :: N'). Validable a => N -> FinList n a -> Statement
vld N
_ FinList n a
Nil = Statement
SValid
    vld N
i (a
a:|FinList n a
as) = (String -> Label
Label (forall a. Show a => a -> String
show N
i) Label -> Statement -> Statement
:<=>: forall a. Validable a => a -> Statement
valid a
a) forall b. Boolean b => b -> b -> b
&& forall a (n :: N'). Validable a => N -> FinList n a -> Statement
vld (forall a. Enum a => a -> a
succ N
i) FinList n a
as

instance (Typeable n, Entity a) => Entity (FinList n a)

--------------------------------------------------------------------------------
-- toW -

-- | the underlying witness.
toW :: FinList n a -> W n
toW :: forall (n :: N') a. FinList n a -> W n
toW FinList n a
Nil     = W 'N0
W0
toW (a
_:|FinList n a
as) = forall (n :: N'). W n -> W (n + 1)
SW (forall (n :: N') a. FinList n a -> W n
toW FinList n a
as) 

--------------------------------------------------------------------------------
-- head -

-- | the head of a non empty finite list.
head :: FinList (n+1) a -> a
head :: forall (n :: N') a. FinList (n + 1) a -> a
head (a
a :| FinList n a
_) = a
a

-------------------------------------------------------------------------------
-- tail -

-- | the tail of a non empty finite list.
tail :: FinList (n+1) a -> FinList n a
tail :: forall (n :: N') a. FinList (n + 1) a -> FinList n a
tail (a
_ :| FinList n a
as) = FinList n a
as 

--------------------------------------------------------------------------------
-- induction-

-- | Wrapper to switch the parameters.
newtype FinList' a n = FinList' (FinList n a)

hypotheseS :: (FinList i a -> FinList (i+1) a) -> FinList' a i -> FinList' a (i+1)
hypotheseS :: forall (i :: N') a.
(FinList i a -> FinList (i + 1) a)
-> FinList' a i -> FinList' a (i + 1)
hypotheseS FinList i a -> FinList (i + 1) a
hs (FinList' FinList i a
s) = forall a (n :: N'). FinList n a -> FinList' a n
FinList' (FinList i a -> FinList (i + 1) a
hs FinList i a
s)

-- | induction for sequences.
inductionS :: Any n
  -> FinList N0 a
  -> (forall i . FinList i a -> FinList (i+1) a)
  -> FinList n a
inductionS :: forall (n :: N') a.
Any n
-> FinList 'N0 a
-> (forall (i :: N'). FinList i a -> FinList (i + 1) a)
-> FinList n a
inductionS Any n
w FinList 'N0 a
s0 forall (i :: N'). FinList i a -> FinList (i + 1) a
hs = FinList n a
sn where FinList' FinList n a
sn = forall (n :: N') (f :: N' -> Type).
Any n -> f 'N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction Any n
w (forall a (n :: N'). FinList n a -> FinList' a n
FinList' FinList 'N0 a
s0) (forall (i :: N') a.
(FinList i a -> FinList (i + 1) a)
-> FinList' a i -> FinList' a (i + 1)
hypotheseS forall (i :: N'). FinList i a -> FinList (i + 1) a
hs)   

--------------------------------------------------------------------------------
-- zip -

-- | zips two sequences of the same length.
zip :: FinList n a -> FinList n b -> FinList n (a,b)
zip :: forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
zip FinList n a
Nil FinList n b
Nil = forall a. FinList 'N0 a
Nil
zip (a
a:|FinList n a
as) (b
b:|FinList n b
bs) = (a
a,b
b)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
zip FinList n a
as FinList n b
bs

-- | zips three sequences of the same length. 
zip3 :: FinList n a -> FinList n b -> FinList n c -> FinList n (a,b,c)
zip3 :: forall (n :: N') a b c.
FinList n a -> FinList n b -> FinList n c -> FinList n (a, b, c)
zip3 FinList n a
as FinList n b
bs FinList n c
cs = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\((a
a,b
b),c
c) -> (a
a,b
b,c
c)) ((FinList n a
as forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n b
bs) forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n c
cs)

--------------------------------------------------------------------------------
-- (|:) -

infixl 5 |:
-- | appending an element at the end of the finite list.
(|:) :: FinList n a -> a -> FinList (n+1) a
FinList n a
Nil |: :: forall (n :: N') a. FinList n a -> a -> FinList (n + 1) a
|: a
b     = a
b forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| forall a. FinList 'N0 a
Nil
(a
a:|FinList n a
as) |: a
b = a
a forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| (FinList n a
asforall (n :: N') a. FinList n a -> a -> FinList (n + 1) a
|:a
b)

--------------------------------------------------------------------------------
-- (++) -

infixr 5 ++

-- | appending two finite lists.
(++) :: FinList n a -> FinList m a -> FinList (n+m) a
FinList n a
Nil ++ :: forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ FinList m a
bs     = FinList m a
bs
(a
a:|FinList n a
as) ++ FinList m a
bs = a
a forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| (FinList n a
as forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ FinList m a
bs)

--------------------------------------------------------------------------------
-- (**) -

-- | the product of two finite lists.
(**) :: FinList n a -> FinList m b -> FinList (n * m) (a,b)
FinList n a
Nil ** :: forall (n :: N') a (m :: N') b.
FinList n a -> FinList m b -> FinList (n * m) (a, b)
** FinList m b
_ = forall a. FinList 'N0 a
Nil
(a
a :| FinList n a
as) ** FinList m b
bs = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (a
a,) FinList m b
bs forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ (FinList n a
as forall (n :: N') a (m :: N') b.
FinList n a -> FinList m b -> FinList (n * m) (a, b)
** FinList m b
bs)

--------------------------------------------------------------------------------
-- repeat -

-- | the constant sequence.
repeat :: Any n ->  a -> FinList n a
repeat :: forall (n :: N') a. Any n -> a -> FinList n a
repeat Any n
n a
a = forall (n :: N') a.
Any n
-> FinList 'N0 a
-> (forall (i :: N'). FinList i a -> FinList (i + 1) a)
-> FinList n a
inductionS Any n
n forall a. FinList 'N0 a
Nil (a
aforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|)

--------------------------------------------------------------------------------
-- toArray -

-- | maps a sequnece @as = a0..a(n-1)@ of length @n@ to the corresponding array @a@ with @ai '==' a'$'i@ for @i = 0..(n-1)@.
toArray :: FinList n a -> Array N a
toArray :: forall (n :: N') a. FinList n a -> Array N a
toArray FinList n a
as = forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (N, N)
b (forall a b. [a] -> [b] -> [(a, b)]
L.zip [N
0..] [a]
as') where
  as' :: [a]
as' = forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList FinList n a
as
  n :: N
n   = forall x. LengthN x => x -> N
lengthN [a]
as'
  b :: (N, N)
b   = if N
0 forall a. Ord a => a -> a -> Bool
< N
n then (N
0,N
nN -> N -> N
>-N
1) else (N
1,N
0)

--------------------------------------------------------------------------------
-- iFinList -

-- | indexing finite lists, starting at the given natural number.
iFinList :: N -> FinList n a -> FinList n (a,N)
iFinList :: forall (n :: N') a. N -> FinList n a -> FinList n (a, N)
iFinList N
_ FinList n a
Nil      = forall a. FinList 'N0 a
Nil
iFinList N
n (a
a:|FinList n a
as)  = (a
a,N
n)forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|forall (n :: N') a. N -> FinList n a -> FinList n (a, N)
iFinList (forall a. Enum a => a -> a
succ N
n) FinList n a
as   

-- | adjoins to each element its index, starting from '0'.
iFinList0 :: FinList n a -> FinList n (a,N)
iFinList0 :: forall (n :: N') a. FinList n a -> FinList n (a, N)
iFinList0 = forall (n :: N') a. N -> FinList n a -> FinList n (a, N)
iFinList N
0

-- | the sequence 0,1 .. n-1.
iFinList' :: Any n -> FinList n N
iFinList' :: forall (n :: N'). Any n -> FinList n N
iFinList' Any n
i = forall (n :: N'). N -> W n -> FinList n N
adj N
0 Any n
i where
  adj :: N -> W n -> FinList n N
  adj :: forall (n :: N'). N -> W n -> FinList n N
adj N
_ W n
W0      = forall a. FinList 'N0 a
Nil
  adj N
i (SW W n
i') = N
i forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| forall (n :: N'). N -> W n -> FinList n N
adj (forall a. Enum a => a -> a
succ N
i) W n
i' 

--------------------------------------------------------------------------------
-- SomeFinList -

-- | some finite list.
data SomeFinList a = forall n . SomeFinList (FinList n a)

deriving instance Show a => Show (SomeFinList a)
instance Functor SomeFinList where
  fmap :: forall a b. (a -> b) -> SomeFinList a -> SomeFinList b
fmap a -> b
f (SomeFinList FinList n a
xs) = forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f FinList n a
xs)
  

-- | the associated finite list.
someFinList :: [a] -> SomeFinList a
someFinList :: forall a. [a] -> SomeFinList a
someFinList [] = forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList forall a. FinList 'N0 a
Nil
someFinList (a
a:[a]
as) = case forall a. [a] -> SomeFinList a
someFinList [a]
as of
  SomeFinList FinList n a
as' -> forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (a
aforall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a
as')

--------------------------------------------------------------------------------
-- (<++>) -

infixr 5 <++>
-- | concatenation.
(<++>) :: SomeFinList x -> SomeFinList x -> SomeFinList x
SomeFinList FinList n x
xs <++> :: forall x. SomeFinList x -> SomeFinList x -> SomeFinList x
<++> SomeFinList FinList n x
ys = forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (FinList n x
xs forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ FinList n x
ys)


{-
--------------------------------------------------------------------------------
-- iFoldl -

iFoldl :: (a -> b -> a) -> a -> FinList n b -> a
iFoldl _ a Nil       = a
iFoldl (*) a (b:|bs) = iFoldl (*) (a*b) bs 
-}