module Data.Type.Witness.Specific.List.List where

import Data.PeanoNat
import Data.Type.Witness.General.Representative
import Data.Type.Witness.Specific.FixedList
import Data.Type.Witness.Specific.Pair
import Data.Type.Witness.Specific.PeanoNat
import Data.Type.Witness.Specific.Some
import Import

-- | a witness type for lists of types
-- The @w@ parameter is the witness type of the elements.
type ListType :: (k -> Type) -> ([k] -> Type)
data ListType w lt where
    NilListType :: ListType w '[]
    ConsListType :: w a -> ListType w lt -> ListType w (a : lt)

instance Representative w => Representative (ListType w) where
    getRepWitness :: Subrepresentative (ListType w) (ListType w)
getRepWitness ListType w a
NilListType = forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (ConsListType w a
w ListType w lt
lw) =
        case (forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w a
w, forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness ListType w lt
lw) of
            (Dict (Is w a)
Dict, Dict (Is (ListType w) lt)
Dict) -> forall (a :: Constraint). a => Dict a
Dict

instance Representative w => Is (ListType w) '[] where
    representative :: ListType w '[]
representative = forall {k} (w :: k -> Type). ListType w '[]
NilListType

instance (Is w a, Is (ListType w) lt) => Is (ListType w) (a : lt) where
    representative :: ListType w (a : lt)
representative = forall {k} (w :: k -> Type) (a :: k) (lt :: [k]).
w a -> ListType w lt -> ListType w (a : lt)
ConsListType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative

instance TestEquality w => TestEquality (ListType w) where
    testEquality :: forall (a :: [k]) (b :: [k]).
ListType w a -> ListType w b -> Maybe (a :~: b)
testEquality ListType w a
NilListType ListType w b
NilListType = forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
    testEquality (ConsListType w a
wpa ListType w lt
wpb) (ConsListType w a
wqa ListType w lt
wqb) = do
        a :~: a
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wpa w a
wqa
        lt :~: lt
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ListType w lt
wpb ListType w lt
wqb
        forall (m :: Type -> Type) a. Monad m => a -> m a
return forall {k} (a :: k). a :~: a
Refl
    testEquality ListType w a
_ ListType w b
_ = forall a. Maybe a
Nothing

instance (forall a. Show (w a)) => Show (ListType w lt) where
    show :: ListType w lt -> String
show ListType w lt
s = String
"[" forall a. Semigroup a => a -> a -> a
<> forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall (t :: [k]). ListType w t -> [String]
showAll ListType w lt
s) forall a. Semigroup a => a -> a -> a
<> String
"]"
      where
        showAll :: forall t. ListType w t -> [String]
        showAll :: forall (t :: [k]). ListType w t -> [String]
showAll ListType w t
NilListType = []
        showAll (ConsListType w a
t1 ListType w lt
tr) = forall a. Show a => a -> String
show w a
t1 forall a. a -> [a] -> [a]
: forall (t :: [k]). ListType w t -> [String]
showAll ListType w lt
tr

assembleListType :: [Some w] -> Some (ListType w)
assembleListType :: forall {k} (w :: k -> Type). [Some w] -> Some (ListType w)
assembleListType [] = forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome forall {k} (w :: k -> Type). ListType w '[]
NilListType
assembleListType ((MkSome w a
wa):[Some w]
ww) =
    case forall {k} (w :: k -> Type). [Some w] -> Some (ListType w)
assembleListType [Some w]
ww of
        MkSome ListType w a
wwa -> forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k) (lt :: [k]).
w a -> ListType w lt -> ListType w (a : lt)
ConsListType w a
wa ListType w a
wwa

mapMListType :: Applicative m => (forall t'. wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)
mapMListType :: forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> m (witb t'))
-> ListType wita t -> m (ListType witb t)
mapMListType forall (t' :: k). wita t' -> m (witb t')
_ff ListType wita t
NilListType = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall {k} (w :: k -> Type). ListType w '[]
NilListType
mapMListType forall (t' :: k). wita t' -> m (witb t')
ff (ConsListType wita a
t ListType wita lt
tt) = forall {k} (w :: k -> Type) (a :: k) (lt :: [k]).
w a -> ListType w lt -> ListType w (a : lt)
ConsListType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t' :: k). wita t' -> m (witb t')
ff wita a
t forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> m (witb t'))
-> ListType wita t -> m (ListType witb t)
mapMListType forall (t' :: k). wita t' -> m (witb t')
ff ListType wita lt
tt

joinMListType ::
       Applicative m
    => (forall t'. wita t' -> witb t' -> m (witc t'))
    -> ListType wita t
    -> ListType witb t
    -> m (ListType witc t)
joinMListType :: forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (witc :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> witb t' -> m (witc t'))
-> ListType wita t -> ListType witb t -> m (ListType witc t)
joinMListType forall (t' :: k). wita t' -> witb t' -> m (witc t')
_ff ListType wita t
NilListType ListType witb t
NilListType = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall {k} (w :: k -> Type). ListType w '[]
NilListType
joinMListType forall (t' :: k). wita t' -> witb t' -> m (witc t')
ff (ConsListType wita a
t1 ListType wita lt
t1t) (ConsListType witb a
t2 ListType witb lt
t2t) = forall {k} (w :: k -> Type) (a :: k) (lt :: [k]).
w a -> ListType w lt -> ListType w (a : lt)
ConsListType forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t' :: k). wita t' -> witb t' -> m (witc t')
ff wita a
t1 witb a
t2 forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (witc :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> witb t' -> m (witc t'))
-> ListType wita t -> ListType witb t -> m (ListType witc t)
joinMListType forall (t' :: k). wita t' -> witb t' -> m (witc t')
ff ListType wita lt
t1t ListType witb lt
t2t

mapListType :: (forall t'. wita t' -> witb t') -> ListType wita t -> ListType witb t
mapListType :: forall {k} (wita :: k -> Type) (witb :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t')
-> ListType wita t -> ListType witb t
mapListType forall (t' :: k). wita t' -> witb t'
ff ListType wita t
l = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> m (witb t'))
-> ListType wita t -> m (ListType witb t)
mapMListType (\wita t'
wt -> forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall (t' :: k). wita t' -> witb t'
ff wita t'
wt) ListType wita t
l

joinListType :: (forall t'. wita t' -> witb t' -> witc t') -> ListType wita t -> ListType witb t -> ListType witc t
joinListType :: forall {k} (wita :: k -> Type) (witb :: k -> Type)
       (witc :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t' -> witc t')
-> ListType wita t -> ListType witb t -> ListType witc t
joinListType forall (t' :: k). wita t' -> witb t' -> witc t'
ff ListType wita t
la ListType witb t
lb = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall {k} (m :: Type -> Type) (wita :: k -> Type)
       (witb :: k -> Type) (witc :: k -> Type) (t :: [k]).
Applicative m =>
(forall (t' :: k). wita t' -> witb t' -> m (witc t'))
-> ListType wita t -> ListType witb t -> m (ListType witc t)
joinMListType (\wita t'
wta witb t'
wtb -> forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ forall (t' :: k). wita t' -> witb t' -> witc t'
ff wita t'
wta witb t'
wtb) ListType wita t
la ListType witb t
lb

pairListType :: ListType wita t -> ListType witb t -> ListType (PairType wita witb) t
pairListType :: forall {k} (wita :: k -> Type) (t :: [k]) (witb :: k -> Type).
ListType wita t
-> ListType witb t -> ListType (PairType wita witb) t
pairListType = forall {k} (wita :: k -> Type) (witb :: k -> Type)
       (witc :: k -> Type) (t :: [k]).
(forall (t' :: k). wita t' -> witb t' -> witc t')
-> ListType wita t -> ListType witb t -> ListType witc t
joinListType forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> w2 t -> PairType w1 w2 t
MkPairType

listTypeLength :: ListType w lt -> Int
listTypeLength :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> Int
listTypeLength ListType w lt
NilListType = Int
0
listTypeLength (ConsListType w a
_ ListType w lt
lt) = forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> Int
listTypeLength ListType w lt
lt

listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r]
listTypeToList :: forall {k} (w :: k -> Type) r (t :: [k]).
(forall (a :: k). w a -> r) -> ListType w t -> [r]
listTypeToList forall (a :: k). w a -> r
_wr ListType w t
NilListType = []
listTypeToList forall (a :: k). w a -> r
wr (ConsListType w a
wa ListType w lt
rest) = (forall (a :: k). w a -> r
wr w a
wa) forall a. a -> [a] -> [a]
: (forall {k} (w :: k -> Type) r (t :: [k]).
(forall (a :: k). w a -> r) -> ListType w t -> [r]
listTypeToList forall (a :: k). w a -> r
wr ListType w lt
rest)

listTypeFor :: Applicative m => ListType w t -> (forall a. w a -> m r) -> m [r]
listTypeFor :: forall {k} (m :: Type -> Type) (w :: k -> Type) (t :: [k]) r.
Applicative m =>
ListType w t -> (forall (a :: k). w a -> m r) -> m [r]
listTypeFor ListType w t
NilListType forall (a :: k). w a -> m r
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure []
listTypeFor (ConsListType w a
t ListType w lt
tt) forall (a :: k). w a -> m r
f = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (:) (forall (a :: k). w a -> m r
f w a
t) forall a b. (a -> b) -> a -> b
$ forall {k} (m :: Type -> Type) (w :: k -> Type) (t :: [k]) r.
Applicative m =>
ListType w t -> (forall (a :: k). w a -> m r) -> m [r]
listTypeFor ListType w lt
tt forall (a :: k). w a -> m r
f

listTypeFor_ :: Applicative m => ListType w t -> (forall a. w a -> m ()) -> m ()
listTypeFor_ :: forall {k} (m :: Type -> Type) (w :: k -> Type) (t :: [k]).
Applicative m =>
ListType w t -> (forall (a :: k). w a -> m ()) -> m ()
listTypeFor_ ListType w t
NilListType forall (a :: k). w a -> m ()
_ = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
listTypeFor_ (ConsListType w a
t ListType w lt
tt) forall (a :: k). w a -> m ()
f = forall (a :: k). w a -> m ()
f w a
t forall (f :: Type -> Type) a b. Applicative f => f a -> f b -> f b
*> forall {k} (m :: Type -> Type) (w :: k -> Type) (t :: [k]).
Applicative m =>
ListType w t -> (forall (a :: k). w a -> m ()) -> m ()
listTypeFor_ ListType w lt
tt forall (a :: k). w a -> m ()
f

listTypeLengthType :: ListType w lt -> PeanoNatType (ListLength lt)
listTypeLengthType :: forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt -> PeanoNatType (ListLength lt)
listTypeLengthType ListType w lt
NilListType = PeanoNatType 'Zero
ZeroType
listTypeLengthType (ConsListType w a
_ ListType w lt
rest) = forall (t1 :: PeanoNat). PeanoNatType t1 -> PeanoNatType ('Succ t1)
SuccType forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (lt :: [k]).
ListType w lt -> PeanoNatType (ListLength lt)
listTypeLengthType ListType w lt
rest

listTypeToFixedList :: (forall a. w a -> r) -> ListType w t -> FixedList (ListLength t) r
listTypeToFixedList :: forall {k} (w :: k -> Type) r (t :: [k]).
(forall (a :: k). w a -> r)
-> ListType w t -> FixedList (ListLength t) r
listTypeToFixedList forall (a :: k). w a -> r
_wr ListType w t
NilListType = forall a. FixedList 'Zero a
NilFixedList
listTypeToFixedList forall (a :: k). w a -> r
wr (ConsListType w a
wa ListType w lt
rest) = forall a (n1 :: PeanoNat).
a -> FixedList n1 a -> FixedList ('Succ n1) a
ConsFixedList (forall (a :: k). w a -> r
wr w a
wa) forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) r (t :: [k]).
(forall (a :: k). w a -> r)
-> ListType w t -> FixedList (ListLength t) r
listTypeToFixedList forall (a :: k). w a -> r
wr ListType w lt
rest

listTypeFromFixedList :: FixedList n (Some w) -> (forall t. n ~ ListLength t => ListType w t -> r) -> r
listTypeFromFixedList :: forall {k} (n :: PeanoNat) (w :: k -> Type) r.
FixedList n (Some w)
-> (forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r)
-> r
listTypeFromFixedList FixedList n (Some w)
NilFixedList forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r
call = forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r
call forall {k} (w :: k -> Type). ListType w '[]
NilListType
listTypeFromFixedList (ConsFixedList (MkSome w a
wa) FixedList n1 (Some w)
l) forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r
call =
    forall {k} (n :: PeanoNat) (w :: k -> Type) r.
FixedList n (Some w)
-> (forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r)
-> r
listTypeFromFixedList FixedList n1 (Some w)
l forall a b. (a -> b) -> a -> b
$ \ListType w t
rest -> forall (t :: [k]). (n ~ ListLength t) => ListType w t -> r
call forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k) (lt :: [k]).
w a -> ListType w lt -> ListType w (a : lt)
ConsListType w a
wa ListType w t
rest