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

import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.List.Element
import Data.Type.Witness.Specific.List.List
import Import
import Unsafe.Coerce

type ListProduct :: [Type] -> Type
type family ListProduct w = r | r -> w where
    ListProduct '[] = ()
    ListProduct (t : tt) = (t, ListProduct tt)

-- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833
injectiveListProduct ::
       forall (a :: [Type]) (b :: [Type]). ListProduct a ~ ListProduct b
    => a :~: b
injectiveListProduct :: forall (a :: [Type]) (b :: [Type]).
(ListProduct a ~ ListProduct b) =>
a :~: b
injectiveListProduct = forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl

listProductEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (ListProduct t))
listProductEq :: forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListProduct t))
listProductEq forall a. w a -> Dict (Eq a)
_ ListType w t
NilListType = forall (a :: Constraint). a => Dict a
Dict
listProductEq forall a. w a -> Dict (Eq a)
f (ConsListType w a
t ListType w lt1
tt) =
    case (forall a. w a -> Dict (Eq a)
f w a
t, forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListProduct t))
listProductEq forall a. w a -> Dict (Eq a)
f ListType w lt1
tt) of
        (Dict (Eq a)
Dict, Dict (Eq (ListProduct lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

listProductShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (ListProduct t))
listProductShow :: forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Show a))
-> ListType w t -> Dict (Show (ListProduct t))
listProductShow forall a. w a -> Dict (Show a)
_ ListType w t
NilListType = forall (a :: Constraint). a => Dict a
Dict
listProductShow forall a. w a -> Dict (Show a)
f (ConsListType w a
t ListType w lt1
tt) =
    case (forall a. w a -> Dict (Show a)
f w a
t, forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Show a))
-> ListType w t -> Dict (Show (ListProduct t))
listProductShow forall a. w a -> Dict (Show a)
f ListType w lt1
tt) of
        (Dict (Show a)
Dict, Dict (Show (ListProduct lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

fillListProduct :: ListType w t -> (forall a. w a -> a) -> ListProduct t
fillListProduct :: forall (w :: Type -> Type) (t :: [Type]).
ListType w t -> (forall a. w a -> a) -> ListProduct t
fillListProduct ListType w t
NilListType forall a. w a -> a
_f = ()
fillListProduct (ConsListType w a
wa ListType w lt1
wr) forall a. w a -> a
f = (forall a. w a -> a
f w a
wa, forall (w :: Type -> Type) (t :: [Type]).
ListType w t -> (forall a. w a -> a) -> ListProduct t
fillListProduct ListType w lt1
wr forall a. w a -> a
f)

mapListProduct :: ListType w t -> (forall a. w a -> a -> a) -> ListProduct t -> ListProduct t
mapListProduct :: forall (w :: Type -> Type) (t :: [Type]).
ListType w t
-> (forall a. w a -> a -> a) -> ListProduct t -> ListProduct t
mapListProduct ListType w t
NilListType forall a. w a -> a -> a
_f () = ()
mapListProduct (ConsListType w a
wa ListType w lt1
wr) forall a. w a -> a -> a
f (a
a, ListProduct lt1
rest) = (forall a. w a -> a -> a
f w a
wa a
a, forall (w :: Type -> Type) (t :: [Type]).
ListType w t
-> (forall a. w a -> a -> a) -> ListProduct t -> ListProduct t
mapListProduct ListType w lt1
wr forall a. w a -> a -> a
f ListProduct lt1
rest)

lift2ListProduct :: ListType w t -> (forall a. w a -> a -> a -> a) -> ListProduct t -> ListProduct t -> ListProduct t
lift2ListProduct :: forall (w :: Type -> Type) (t :: [Type]).
ListType w t
-> (forall a. w a -> a -> a -> a)
-> ListProduct t
-> ListProduct t
-> ListProduct t
lift2ListProduct ListType w t
NilListType forall a. w a -> a -> a -> a
_f () () = ()
lift2ListProduct (ConsListType w a
wa ListType w lt1
wr) forall a. w a -> a -> a -> a
f (a
a, ListProduct lt1
resta) (a
b, ListProduct lt1
restb) = (forall a. w a -> a -> a -> a
f w a
wa a
a a
b, forall (w :: Type -> Type) (t :: [Type]).
ListType w t
-> (forall a. w a -> a -> a -> a)
-> ListProduct t
-> ListProduct t
-> ListProduct t
lift2ListProduct ListType w lt1
wr forall a. w a -> a -> a -> a
f ListProduct lt1
resta ListProduct lt1
restb)

identityListProduct :: ListType Identity lt -> ListProduct lt
identityListProduct :: forall (lt :: [Type]). ListType Identity lt -> ListProduct lt
identityListProduct ListType Identity lt
NilListType = ()
identityListProduct (ConsListType (Identity a
a) ListType Identity lt1
rest) = (a
a, forall (lt :: [Type]). ListType Identity lt -> ListProduct lt
identityListProduct ListType Identity lt1
rest)

sequenceListProduct :: Applicative f => ListType f lt -> f (ListProduct lt)
sequenceListProduct :: forall (f :: Type -> Type) (lt :: [Type]).
Applicative f =>
ListType f lt -> f (ListProduct lt)
sequenceListProduct ListType f lt
NilListType = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
sequenceListProduct (ConsListType f a
fa ListType f lt1
rest) = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) f a
fa (forall (f :: Type -> Type) (lt :: [Type]).
Applicative f =>
ListType f lt -> f (ListProduct lt)
sequenceListProduct ListType f lt1
rest)

listProductGetElement :: ListElementType list t -> ListProduct list -> t
listProductGetElement :: forall (list :: [Type]) t.
ListElementType list t -> ListProduct list -> t
listProductGetElement ListElementType list t
FirstElementType = forall a b. (a, b) -> a
fst -- using fst and snd for irrefutable matching
listProductGetElement (RestElementType ListElementType aa t
lw) = forall (list :: [Type]) t.
ListElementType list t -> ListProduct list -> t
listProductGetElement ListElementType aa t
lw forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall a b. (a, b) -> b
snd

listProductPutElement :: ListElementType list t -> t -> ListProduct list -> ListProduct list
listProductPutElement :: forall (list :: [Type]) t.
ListElementType list t -> t -> ListProduct list -> ListProduct list
listProductPutElement ListElementType list t
FirstElementType t
t (t
_, ListProduct tt
r) = (t
t, ListProduct tt
r)
listProductPutElement (RestElementType ListElementType aa t
lw) t
t (a
a, ListProduct aa
r) = (a
a, forall (list :: [Type]) t.
ListElementType list t -> t -> ListProduct list -> ListProduct list
listProductPutElement ListElementType aa t
lw t
t ListProduct aa
r)

listProductModifyElement :: ListElementType list t -> (t -> t) -> ListProduct list -> ListProduct list
listProductModifyElement :: forall (list :: [Type]) t.
ListElementType list t
-> (t -> t) -> ListProduct list -> ListProduct list
listProductModifyElement ListElementType list t
n t -> t
aa ListProduct list
t = forall (list :: [Type]) t.
ListElementType list t -> t -> ListProduct list -> ListProduct list
listProductPutElement ListElementType list t
n (t -> t
aa (forall (list :: [Type]) t.
ListElementType list t -> ListProduct list -> t
listProductGetElement ListElementType list t
n ListProduct list
t)) ListProduct list
t

type ListProductType :: (Type -> Type) -> (Type -> Type)
data ListProductType wit t where
    MkListProductType
        :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListProductType wit (ListProduct lt)

instance TestEquality wit => TestEquality (ListProductType wit) where
    testEquality :: forall a b.
ListProductType wit a -> ListProductType wit b -> Maybe (a :~: b)
testEquality (MkListProductType ListType wit lt
lt1) (MkListProductType ListType wit lt
lt2) =
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ListType wit lt
lt1 ListType wit lt
lt2 of
            Just lt :~: lt
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
            Maybe (lt :~: lt)
Nothing -> forall a. Maybe a
Nothing

instance WitnessConstraint Eq w => WitnessConstraint Eq (ListProductType w) where
    witnessConstraint :: forall t. ListProductType w t -> Dict (Eq t)
witnessConstraint (MkListProductType ListType w lt
lt) = forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListProduct t))
listProductEq forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint ListType w lt
lt

instance Representative w => Representative (ListProductType w) where
    getRepWitness :: Subrepresentative (ListProductType w) (ListProductType w)
getRepWitness (MkListProductType ListType w lt
NilListType) = forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (MkListProductType (ConsListType w a
a ListType w lt1
ar)) =
        case (forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w a
a, forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness forall a b. (a -> b) -> a -> b
$ forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListProductType wit (ListProduct lt)
MkListProductType ListType w lt1
ar) of
            (Dict (Is w a)
Dict, Dict (Is (ListProductType w) (ListProduct lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

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

instance (Is w a, Is (ListProductType w) ar) => Is (ListProductType w) (a, ar) where
    representative :: ListProductType w (a, ar)
representative =
        case forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListProductType w) @ar of
            MkListProductType ListType w lt
r -> forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListProductType wit (ListProduct lt)
MkListProductType forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative ListType w lt
r