module Data.Yoko.InDT where
import Type.Yoko
import Data.Yoko.Generic
import Data.Yoko.Reflect
data HasTagRepDCD tag c t where
HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
HasTagRepDCD tag c t
instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits
hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t
hasTagRepDCD (HasTagRepDCD d) = w d where
w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t
w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj
w (OnLeft u) = w u; w (OnRight u) = w u
type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))
data ImageInDTD t fn dc where
ImageInDTD :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc
instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
) => dc ::: ImageInDTD t fn where
inhabits = ImageInDTD inhabits
imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t
imageInDTD fn (ImageInDTD d) = hasTagRepDCD d . apply (CMap fn) . rep
data ImageInDTDA t fn dc where
ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)
) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc
instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
) => dc ::: ImageInDTDA t fn where
inhabits = ImageInDTDA inhabits
imageInDTAD :: Functor (Idiom (fn IdM)) =>
(forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
imageInDTAD fn (ImageInDTDA d) = fmap (hasTagRepDCD d) . applyA (CMap fn) . rep