module Data.Type.Witness.Specific.All where

import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.Some
import Import

type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type
type role AllFor representational representational
newtype AllFor f w = MkAllFor
    { forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor :: forall t. w t -> f t
    }

mapAllFor :: (forall a. f1 a -> f2 a) -> AllFor f1 w -> AllFor f2 w
mapAllFor :: forall {k} (f1 :: k -> Type) (f2 :: k -> Type) (w :: k -> Type).
(forall (a :: k). f1 a -> f2 a) -> AllFor f1 w -> AllFor f2 w
mapAllFor forall (a :: k). f1 a -> f2 a
ff (MkAllFor forall (t :: k). w t -> f1 t
wtft) = (forall (t :: k). w t -> f2 t) -> AllFor f2 w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall (t :: k). w t -> f2 t) -> AllFor f2 w)
-> (forall (t :: k). w t -> f2 t) -> AllFor f2 w
forall a b. (a -> b) -> a -> b
$ f1 t -> f2 t
forall (a :: k). f1 a -> f2 a
ff (f1 t -> f2 t) -> (w t -> f1 t) -> w t -> f2 t
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. w t -> f1 t
forall (t :: k). w t -> f1 t
wtft

type AllOf :: (Type -> Type) -> Type
type role AllOf representational
newtype AllOf w = MkAllOf
    { forall (w :: Type -> Type). AllOf w -> forall t. w t -> t
unAllOf :: forall t. w t -> t
    }

setAllOf ::
       forall (w :: Type -> Type) (a :: Type). TestEquality w
    => w a
    -> a
    -> AllOf w
    -> AllOf w
setAllOf :: forall (w :: Type -> Type) a.
TestEquality w =>
w a -> a -> AllOf w -> AllOf w
setAllOf w a
wa a
a (MkAllOf forall t. w t -> t
wtt) =
    (forall t. w t -> t) -> AllOf w
forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf ((forall t. w t -> t) -> AllOf w)
-> (forall t. w t -> t) -> AllOf w
forall a b. (a -> b) -> a -> b
$ \w t
wa' ->
        case w a -> w t -> Maybe (a :~: t)
forall a b. w a -> w b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wa w t
wa' of
            Just a :~: t
Refl -> a
t
a
            Maybe (a :~: t)
Nothing -> w t -> t
forall t. w t -> t
wtt w t
wa'

allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w
allForToAllOf (MkAllFor forall t. w t -> Identity t
wtit) = (forall t. w t -> t) -> AllOf w
forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf ((forall t. w t -> t) -> AllOf w)
-> (forall t. w t -> t) -> AllOf w
forall a b. (a -> b) -> a -> b
$ \w t
wt -> Identity t -> t
forall a. Identity a -> a
runIdentity (Identity t -> t) -> Identity t -> t
forall a b. (a -> b) -> a -> b
$ w t -> Identity t
forall t. w t -> Identity t
wtit w t
wt

allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w
allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w
allOfToAllFor (MkAllOf forall t. w t -> t
wtt) = (forall t. w t -> Identity t) -> AllFor Identity w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall t. w t -> Identity t) -> AllFor Identity w)
-> (forall t. w t -> Identity t) -> AllFor Identity w
forall a b. (a -> b) -> a -> b
$ \w t
wt -> t -> Identity t
forall a. a -> Identity a
Identity (t -> Identity t) -> t -> Identity t
forall a b. (a -> b) -> a -> b
$ w t -> t
forall t. w t -> t
wtt w t
wt

allMapSome :: AllFor f w -> SomeFor g w -> SomeFor g f
allMapSome :: forall {k} (f :: k -> Type) (w :: k -> Type) (g :: k -> Type).
AllFor f w -> SomeFor g w -> SomeFor g f
allMapSome (MkAllFor forall (t :: k). w t -> f t
f) = (forall (t :: k). w t -> f t) -> SomeFor g w -> SomeFor g f
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 w t -> f t
forall (t :: k). w t -> f t
f

type UnAllOf :: Type -> Type -> Type
type family UnAllOf aw where
    UnAllOf (AllOf w) = w

splitSomeOfList ::
       forall (w :: Type -> Type). TestEquality w
    => [SomeOf w]
    -> AllFor [] w
splitSomeOfList :: forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [] = (forall t. w t -> [t]) -> AllFor [] w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall t. w t -> [t]) -> AllFor [] w)
-> (forall t. w t -> [t]) -> AllFor [] w
forall a b. (a -> b) -> a -> b
$ \w t
_ -> []
splitSomeOfList ((MkSomeOf w a
wt a
t):[SomeOf w]
rr) =
    (forall t. w t -> [t]) -> AllFor [] w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall t. w t -> [t]) -> AllFor [] w)
-> (forall t. w t -> [t]) -> AllFor [] w
forall a b. (a -> b) -> a -> b
$ \w t
wt' ->
        case w a -> w t -> Maybe (a :~: t)
forall a b. w a -> w b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality w a
wt w t
wt' of
            Just a :~: t
Refl -> a
t
t t -> [t] -> [t]
forall a. a -> [a] -> [a]
: (AllFor [] w -> forall t. w t -> [t]
forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor ([SomeOf w] -> AllFor [] w
forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [SomeOf w]
rr) w t
wt')
            Maybe (a :~: t)
Nothing -> AllFor [] w -> forall t. w t -> [t]
forall k (f :: k -> Type) (w :: k -> Type).
AllFor f w -> forall (t :: k). w t -> f t
unAllFor ([SomeOf w] -> AllFor [] w
forall (w :: Type -> Type).
TestEquality w =>
[SomeOf w] -> AllFor [] w
splitSomeOfList [SomeOf w]
rr) w t
wt'

allForWitnessConstraint ::
       forall k (c :: k -> Constraint) (w :: k -> Type). WitnessConstraint c w
    => AllFor (Compose Dict c) w
allForWitnessConstraint :: forall k (c :: k -> Constraint) (w :: k -> Type).
WitnessConstraint c w =>
AllFor (Compose Dict c) w
allForWitnessConstraint = (forall (t :: k). w t -> Compose Dict c t)
-> AllFor (Compose Dict c) w
forall k (f :: k -> Type) (w :: k -> Type).
(forall (t :: k). w t -> f t) -> AllFor f w
MkAllFor ((forall (t :: k). w t -> Compose Dict c t)
 -> AllFor (Compose Dict c) w)
-> (forall (t :: k). w t -> Compose Dict c t)
-> AllFor (Compose Dict c) w
forall a b. (a -> b) -> a -> b
$ \w t
wt -> Dict (c t) -> Compose Dict c t
forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Dict (c t) -> Compose Dict c t) -> Dict (c t) -> Compose Dict c t
forall a b. (a -> b) -> a -> b
$ w t -> Dict (c t)
forall (t :: k). w t -> Dict (c t)
forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint w t
wt