module Data.Yoko.Reflect
(module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.ReflectBase hiding (DCU)
type instance Tag (N dc) = Tag dc
type instance Recurs (D a) = V
type instance Recurs (F f c) = Recurs c
type instance Recurs (FF ff c d) =
NormW (Recurs c) (Recurs d)
type instance Recurs (M i c) = Recurs c
type instance Recurs (N t) = Recurs (Rep t)
type instance Recurs (R t) = N t
type instance Recurs U = V
type instance Recurs V = V
type SiblingsU t = Uni (Siblings t)
type OnlyDC t = UnN (DCs t)
type family UnN a
type instance UnN (N dc) = dc
uniqueDC :: (DT t, N (OnlyDC t) ~ DCs t, t ~ Range (OnlyDC t)) => t -> RMNI (OnlyDC t)
uniqueDC = uniqueRMN . disband
uniqueRMN :: (Finite u, N (UnN (Inhabitants u)) ~ Inhabitants u
) => AnRMN m u -> RMN m (UnN (Inhabitants u))
uniqueRMN x = case finiteNP x of NP (Uni (Here Refl)) x -> x
uniqueRMN' :: (Finite (DCOf (Range dc)), N dc ~ DCs (Range dc)
) => AnRMN m (DCOf (Range dc)) -> RMN m dc
uniqueRMN' = uniqueRMN
data IsDC dc where IsDC :: DC dc => IsDC dc
type instance Pred IsDC t = True
instance DC dc => dc ::: IsDC where inhabits = IsDC
newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b}
type instance Unwrap (RMNTo m b) dc = RMN m dc -> b
instance Wrapper (RMNTo m b) where wrap = RMNTo; unwrap = rmnTo
dcDispatch :: DT t => NT (DCOf t) (RMNTo IdM b) -> t -> b
dcDispatch = (. disband) . dcDispatch'
dcDispatch' :: DT t => NT (DCOf t) (RMNTo IdM b) -> Disbanded IdM t -> b
dcDispatch' nt (NP tag fds) = appNT nt tag fds
data TagRepIs tag c dc where
TagRepIs :: (Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc
instance (Tag dc ~ tag, c ~ Rep dc) => dc ::: TagRepIs tag c where
inhabits = TagRepIs
type instance Pred (TagRepIs tag c) dc =
And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))
bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band
fr_DCOf :: DCOf t dc -> RMNI dc -> t; fr_DCOf (DCOf _) = fr