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

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

    -- ** Induction

  , inductionS, FinList'(..)

    -- * X

  , xListF
  )

  where

import Control.Monad as M

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 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 Show a => Show (FinList n a) where
  show :: FinList n a -> String
show FinList n a
xs = String
"[|" String -> ShowS
forall a. [a] -> [a] -> [a]
L.++ ([String] -> String
forall (m :: Type -> Type) a. Monad m => m (m a) -> m a
join ([String] -> String) -> [String] -> String
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
tween String
"," ([String] -> [String]) -> [String] -> [String]
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ (a -> String) -> [a] -> [String]
forall (h :: Type -> Type -> Type) (f :: Type -> Type) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> String
forall a. Show a => a -> String
show ([a] -> [String]) -> [a] -> [String]
forall (h :: Type -> Type -> Type) x y.
Applicative h =>
h x y -> x -> y
$ FinList n a -> [a]
forall a. FinList n a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList FinList n a
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
L.++ String
"|]"

instance ApplicativeG (FinList n) (->) (->) where
  amapG :: forall x y. (x -> y) -> FinList n x -> FinList n y
amapG x -> y
_ FinList n x
Nil     = FinList n y
FinList 'N0 y
forall a. FinList 'N0 a
Nil
  amapG x -> y
f (x
a:|FinList n x
as) = x -> y
f x
a y -> FinList n y -> FinList (n + 1) y
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| (x -> y) -> FinList n x -> FinList n y
forall x y. (x -> y) -> FinList n x -> FinList n y
forall (t :: Type -> Type) (a :: Type -> Type -> Type)
       (b :: Type -> Type -> Type) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG x -> y
f FinList n x
as

instance Validable a => Validable (FinList n a) where
  valid :: FinList n a -> Statement
valid FinList n a
as = N -> FinList n a -> Statement
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 (N -> String
forall a. Show a => a -> String
show N
i) Label -> Statement -> Statement
:<=>: a -> Statement
forall a. Validable a => a -> Statement
valid a
a) Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> FinList n a -> Statement
forall a (n :: N'). Validable a => N -> FinList n a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) FinList n a
as

--------------------------------------------------------------------------------

-- 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 n
W 'N0
W0
toW (a
_:|FinList n a
as) = W n -> W (n + 1)
forall (n1 :: N'). W n1 -> W (n1 + 1)
SW (FinList n a -> W n
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
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) = FinList ('S i) a -> FinList' a ('S i)
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 = Any n
-> FinList' a 'N0
-> (forall (i :: N'). FinList' a i -> FinList' a (i + 1))
-> FinList' a n
forall (n :: N') (f :: N' -> Type).
Any n -> f 'N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
induction Any n
w (FinList 'N0 a -> FinList' a 'N0
forall a (n :: N'). FinList n a -> FinList' a n
FinList' FinList 'N0 a
s0) ((FinList i a -> FinList (i + 1) a)
-> FinList' a i -> FinList' a (i + 1)
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
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 = FinList n (a, b)
FinList 'N0 (a, b)
forall a. FinList 'N0 a
Nil
zip (a
a:|FinList n a
as) (b
b:|FinList n b
bs) = (a
a,b
b)(a, b) -> FinList n (a, b) -> FinList (n + 1) (a, b)
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a -> FinList n b -> FinList n (a, b)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
zip FinList n a
as FinList n b
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 = (((a, b), c) -> (a, b, c))
-> FinList n ((a, b), c) -> FinList n (a, b, c)
forall (h :: Type -> Type -> Type) (f :: Type -> Type) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\((a
a,b
b),c
c) -> (a
a,b
b,c
c)) ((FinList n a
as FinList n a -> FinList n b -> FinList n (a, b)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n b
bs) FinList n (a, b) -> FinList n c -> FinList n ((a, b), c)
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 a -> FinList 'N0 a -> FinList ('N0 + 1) a
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| FinList 'N0 a
forall a. FinList 'N0 a
Nil
(a
a:|FinList n a
as) |: a
b = a
a a -> FinList ('S n) a -> FinList ('S n + 1) a
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| (FinList n a
asFinList n a -> a -> FinList (n + 1) a
forall (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
FinList (n + m) a
bs
(a
a:|FinList n a
as) ++ FinList m a
bs = a
a a -> FinList (n + m) a -> FinList ((n + m) + 1) a
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| (FinList n a
as FinList n a -> FinList m a -> FinList (n + m) a
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
_ = FinList (n * m) (a, b)
FinList 'N0 (a, b)
forall a. FinList 'N0 a
Nil
(a
a :| FinList n a
as) ** FinList m b
bs = (b -> (a, b)) -> FinList m b -> FinList m (a, b)
forall (h :: Type -> Type -> Type) (f :: Type -> Type) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (a
a,) FinList m b
bs FinList m (a, b)
-> FinList (n * m) (a, b) -> FinList (m + (n * m)) (a, b)
forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ (FinList n a
as FinList n a -> FinList m b -> FinList (n * m) (a, b)
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 = Any n
-> FinList 'N0 a
-> (forall (i :: N'). FinList i a -> FinList (i + 1) a)
-> FinList n 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 FinList 'N0 a
forall a. FinList 'N0 a
Nil (a
aa -> FinList i a -> FinList (i + 1) a
forall 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 = (N, N) -> [(N, a)] -> Array N a
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (N, N)
b ([N] -> [a] -> [(N, a)]
forall a b. [a] -> [b] -> [(a, b)]
L.zip [N
0..] [a]
as') where
  as' :: [a]
as' = FinList n a -> [a]
forall a. FinList n a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList FinList n a
as
  n :: N
n   = [a] -> N
forall x. LengthN x => x -> N
lengthN [a]
as'
  b :: (N, N)
b   = if N
0 N -> N -> Bool
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      = FinList n (a, N)
FinList 'N0 (a, N)
forall a. FinList 'N0 a
Nil
iFinList N
n (a
a:|FinList n a
as)  = (a
a,N
n)(a, N) -> FinList n (a, N) -> FinList (n + 1) (a, N)
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|N -> FinList n a -> FinList n (a, N)
forall (n :: N') a. N -> FinList n a -> FinList n (a, N)
iFinList (N -> N
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 = N -> FinList n a -> FinList n (a, N)
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 = N -> Any n -> FinList n N
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      = FinList n N
FinList 'N0 N
forall a. FinList 'N0 a
Nil
  adj N
i (SW W n1
i') = N
i N -> FinList n1 N -> FinList (n1 + 1) N
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:| N -> W n1 -> FinList n1 N
forall (n :: N'). N -> W n -> FinList n N
adj (N -> N
forall a. Enum a => a -> a
succ N
i) W n1
i' 

--------------------------------------------------------------------------------

-- SomeFinList -


-- | some finite list.

data SomeFinList a = forall n . SomeFinList (FinList n a)

deriving instance Show a => Show (SomeFinList a)

instance Validable a => Validable (SomeFinList a) where
  valid :: SomeFinList a -> Statement
valid (SomeFinList FinList n a
xs) = FinList n a -> Statement
forall a. Validable a => a -> Statement
valid FinList n a
xs

instance ApplicativeG SomeFinList (->) (->)  where
  amapG :: forall x y. (x -> y) -> SomeFinList x -> SomeFinList y
amapG x -> y
f (SomeFinList FinList n x
xs) = FinList n y -> SomeFinList y
forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList ((x -> y) -> FinList n x -> FinList n y
forall x y. (x -> y) -> FinList n x -> FinList n y
forall (t :: Type -> Type) (a :: Type -> Type -> Type)
       (b :: Type -> Type -> Type) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG x -> y
f FinList n x
xs)
  

--------------------------------------------------------------------------------

-- someFinList -


-- | the associated finite list.

--

-- __Note__ If the input list is infinite then 'someFinList' dose not terminate.

someFinList :: [a] -> SomeFinList a
someFinList :: forall a. [a] -> SomeFinList a
someFinList [] = FinList 'N0 a -> SomeFinList a
forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList FinList 'N0 a
forall a. FinList 'N0 a
Nil
someFinList (a
a:[a]
as) = case [a] -> SomeFinList a
forall a. [a] -> SomeFinList a
someFinList [a]
as of
  SomeFinList FinList n a
as' -> FinList ('S n) a -> SomeFinList a
forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (a
aa -> FinList n a -> FinList (n + 1) a
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|FinList n a
as')

--------------------------------------------------------------------------------

-- maybeFinList -


-- | list as a finite list according to @__n__@.

--

-- __Property__ Let @xs@ be in @[__a__]@ and @n@ in @'Any' __n__@, then holds:

--

-- (1) If @'lengthN' n '<=' 'length' xs@ then @'maybeFinList' n xs@ matches @'Just' xs'@ with

-- @'toList' xs' '==' xs@.

maybeFinList :: Any n -> [a] -> Maybe (FinList n a)
maybeFinList :: forall (n :: N') a. Any n -> [a] -> Maybe (FinList n a)
maybeFinList W n
W0 [a]
_          = FinList n a -> Maybe (FinList n a)
forall a. a -> Maybe a
Just (FinList n a
FinList 'N0 a
forall a. FinList 'N0 a
Nil)
maybeFinList W n
_ []          = Maybe (FinList n a)
forall a. Maybe a
Nothing
maybeFinList (SW W n1
n) (a
a:[a]
as) = W n1 -> [a] -> Maybe (FinList n1 a)
forall (n :: N') a. Any n -> [a] -> Maybe (FinList n a)
maybeFinList W n1
n [a]
as Maybe (FinList n1 a)
-> (FinList n1 a -> Maybe (FinList n a)) -> Maybe (FinList n a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= FinList ('S n1) a -> Maybe (FinList ('S n1) a)
forall a. a -> Maybe a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FinList ('S n1) a -> Maybe (FinList ('S n1) a))
-> (FinList n1 a -> FinList ('S n1) a)
-> FinList n1 a
-> Maybe (FinList ('S n1) a)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. (a
aa -> FinList n1 a -> FinList (n1 + 1) a
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|)

--------------------------------------------------------------------------------

-- (<++>) -


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 = FinList (n + n) x -> SomeFinList x
forall a (n :: N'). FinList n a -> SomeFinList a
SomeFinList (FinList n x
xs FinList n x -> FinList n x -> FinList (n + n) x
forall (n :: N') a (m :: N').
FinList n a -> FinList m a -> FinList (n + m) a
++ FinList n x
ys)

--------------------------------------------------------------------------------

-- xListF -


-- | random variable for a finite list of random variables.

xListF :: FinList n (X x) -> X (FinList n x)
xListF :: forall (n :: N') x. FinList n (X x) -> X (FinList n x)
xListF FinList n (X x)
Nil = FinList n x -> X (FinList n x)
forall a. a -> X a
forall (m :: Type -> Type) a. Monad m => a -> m a
return FinList n x
FinList 'N0 x
forall a. FinList 'N0 a
Nil
xListF (X x
xx:|FinList n (X x)
xxs) = do
  x
x  <- X x
xx
  FinList n (X x) -> X (FinList n x)
forall (n :: N') x. FinList n (X x) -> X (FinList n x)
xListF FinList n (X x)
xxs X (FinList n x)
-> (FinList n x -> X (FinList n x)) -> X (FinList n x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= FinList ('S n) x -> X (FinList ('S n) x)
forall a. a -> X a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (FinList ('S n) x -> X (FinList ('S n) x))
-> (FinList n x -> FinList ('S n) x)
-> FinList n x
-> X (FinList ('S n) x)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: Type -> Type -> Type) y z x.
Category c =>
c y z -> c x y -> c x z
. (x
xx -> FinList n x -> FinList (n + 1) x
forall a (n :: N'). a -> FinList n a -> FinList (n + 1) a
:|)



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

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