module Data.Yoko.HCompos where
import Data.Yoko.TypeBasics
import Data.Yoko.W
import Data.Yoko
import Control.Applicative
import Data.Traversable (Traversable, traverse)
import Data.Bitraversable (Bitraversable, bitraverse)
import Type.Digits (Digit)
type family Idiom (cnv :: *) :: * -> *
class Applicative (Idiom cnv) => Convert0 cnv a b where
convert0 :: cnv -> a -> Idiom cnv b
class Applicative (Idiom cnv) => HCompos0 cnv a t where
hcompos0 :: cnv -> a p1 p0 -> Idiom cnv t
type instance Idiom (a -> i b) = i
instance (Applicative i, a ~ x, b ~ y) => Convert0 (a -> i b) x y where convert0 = ($)
data FoundDC (k :: *) (l :: *) = NoCorrespondingConstructorFor_In_ k k | Match l
type family WithMessage (dcA :: k) (b :: k) (dcB :: Maybe l) :: FoundDC k l
type instance WithMessage dcA b (Just x) = Match x
type instance WithMessage dcA b Nothing = NoCorrespondingConstructorFor_In_ dcA b
type family FindDCs (s :: Digit) (dcBs :: * -> * -> *) :: Maybe (* -> * -> *)
type instance FindDCs s (N dc) =
If (Equal s (Tag dc)) (Just (N dc)) Nothing
type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)
instance (HCompos0 cnv a t, HCompos0 cnv b t
) => HCompos0 cnv (a :+: b) t where
hcompos0 cnv = foldPlus (hcompos0 cnv) (hcompos0 cnv)
instance (Generic dcA, Match (N dcB) ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),
MapRs0 cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB),
DC dcB, Codomain dcB ~ b, DT b
) => HCompos0 cnv (N dcA) b where
hcompos0 cnv =
foldN0 $ liftA (unSym0 rejoin . (id :: dcB -> dcB) . unW'0 obj) . mapRs0 cnv msgp p1 p2 . unW0 rep
where p1 :: Proxy dcA; p1 = Proxy; p2 :: Proxy dcB; p2 = Proxy
msgp = ResultsInIncompatibleFields :: ResultsInIncompatibleFields dcA dcB
data ResultsInIncompatibleFields (dcA :: k) (dcB :: k) = ResultsInIncompatibleFields
class Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' prod prod' where
mapRs0 :: cnv -> msg -> Proxy dc -> Proxy dc' -> prod p1 p0 -> Idiom cnv (prod' p1 p0)
instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' U U where
mapRs0 _ _ _ _ = pure
instance (MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'
) => MapRs0 cnv msg dc dc' (a :*: b) (a' :*: b') where
mapRs0 cnv msgp p1 p2 (a :*: b) = (:*:) <$> mapRs0 cnv msgp p1 p2 a <*> mapRs0 cnv msgp p1 p2 b
instance MapRs0 cnv msg dc dc' a a' => MapRs0 cnv msg dc dc' (C dcA a) (C dcB a') where
mapRs0 cnv msgp p1 p2 (C x) = C <$> mapRs0 cnv msgp p1 p2 x
instance Convert0 cnv a b => MapRs0 cnv msg dc dc' (T0 (Rec lbl) a) (T0 (Rec lbl') b) where
mapRs0 cnv _ _ _ (T0 x) = T0 <$> convert0 cnv x
instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' (T0 Dep a) (T0 Dep a) where
mapRs0 _ _ _ _ = pure
instance (Traversable f, MapRs0 cnv msg dc dc' a a'
) => MapRs0 cnv msg dc dc' (T1 Dep f a) (T1 Dep f a') where
mapRs0 cnv msgp p1 p2 (T1 x) = T1 <$> traverse (mapRs0 cnv msgp p1 p2) x
instance (Bitraversable f, MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'
) => MapRs0 cnv msg dc dc' (T2 Dep f a b) (T2 Dep f a' b') where
mapRs0 cnv msgp p1 p2 (T2 x) = T2 <$> bitraverse (mapRs0 cnv msgp p1 p2) (mapRs0 cnv msgp p1 p2) x