module Data.Type.Witness.Specific.FiniteAllFor where

import Data.Type.Witness.General.Finite
import Data.Type.Witness.Specific.All
import Data.Type.Witness.Specific.Either
import Data.Type.Witness.Specific.Some
import Import

type FiniteAllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
data FiniteAllFor f w = MkFiniteAllFor
    { forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some w]
finiteDomain :: [Some w]
    , forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> forall (t :: k). w t -> f t
finiteGetAllFor :: forall t. w t -> f t
    }

finiteAllFor :: FiniteAllFor f w -> AllFor f w
finiteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> AllFor f w
finiteAllFor (MkFiniteAllFor [Some w]
_ forall (t :: k). w t -> f t
f) = forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall (t :: k). w t -> f t
f

finiteCodomain :: FiniteAllFor f w -> [Some f]
finiteCodomain :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some f]
finiteCodomain FiniteAllFor f w
sw = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkSome w a
st) -> forall {k} (w :: k -> Type) (a :: k). w a -> Some w
MkSome forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> forall (t :: k). w t -> f t
finiteGetAllFor FiniteAllFor f w
sw w a
st) forall a b. (a -> b) -> a -> b
$ forall k (f :: k -> Type) (w :: k -> Type).
FiniteAllFor f w -> [Some w]
finiteDomain FiniteAllFor f w
sw

mapFiniteAllFor :: (forall t. f1 t -> f2 t) -> FiniteAllFor f1 w -> FiniteAllFor f2 w
mapFiniteAllFor :: forall {k} (f1 :: k -> Type) (f2 :: k -> Type) (w :: k -> Type).
(forall (t :: k). f1 t -> f2 t)
-> FiniteAllFor f1 w -> FiniteAllFor f2 w
mapFiniteAllFor forall (t :: k). f1 t -> f2 t
ff (MkFiniteAllFor [Some w]
ai forall (t :: k). w t -> f1 t
i) = forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor [Some w]
ai forall a b. (a -> b) -> a -> b
$ \w t
s -> forall (t :: k). f1 t -> f2 t
ff forall a b. (a -> b) -> a -> b
$ forall (t :: k). w t -> f1 t
i w t
s

eitherFiniteAllFor :: FiniteAllFor t w1 -> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2)
eitherFiniteAllFor :: forall {k} (t :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
FiniteAllFor t w1
-> FiniteAllFor t w2 -> FiniteAllFor t (EitherType w1 w2)
eitherFiniteAllFor (MkFiniteAllFor [Some w1]
a1 forall (t :: k). w1 t -> t t
i1) (MkFiniteAllFor [Some w2]
a2 forall (t :: k). w2 t -> t t
i2) =
    forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor
        ((forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
(forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
mapSome forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w1 t -> EitherType w1 w2 t
LeftType) [Some w1]
a1) forall a. [a] -> [a] -> [a]
++ (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type).
(forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2
mapSome forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k).
w2 t -> EitherType w1 w2 t
RightType) [Some w2]
a2))
        (forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> Type) (sel1 :: k -> Type)
       (sel2 :: k -> Type).
AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2)
eitherAllFor (forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall (t :: k). w1 t -> t t
i1) (forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor forall (t :: k). w2 t -> t t
i2))

mkFiniteAllFor ::
       forall f w. FiniteWitness w
    => (forall t. w t -> f t)
    -> FiniteAllFor f w
mkFiniteAllFor :: forall {k} (f :: k -> Type) (w :: k -> Type).
FiniteWitness w =>
(forall (t :: k). w t -> f t) -> FiniteAllFor f w
mkFiniteAllFor = forall k (f :: k -> Type) (w :: k -> Type).
[Some w] -> (forall (t :: k). w t -> f t) -> FiniteAllFor f w
MkFiniteAllFor forall {k} (w :: k -> Type). FiniteWitness w => [Some w]
allWitnesses