module Data.Comp.Multi.Sum
(
(:<:)(..),
(:+:)(..),
proj2,
proj3,
project,
project2,
project3,
deepProject,
deepProject2,
deepProject3,
inj2,
inj3,
inject,
inject2,
inject3,
deepInject,
deepInject2,
deepInject3,
injectConst,
injectConst2,
injectConst3,
projectConst,
injectCxt,
liftCxt,
substHoles,
) where
import Data.Comp.Multi.Functor
import Data.Comp.Multi.Traversable
import Data.Comp.Multi.Ops
import Data.Comp.Multi.Term
import Data.Comp.Multi.Algebra
import Control.Monad (liftM)
proj2 :: forall f g1 g2 a i. (g1 :<: f, g2 :<: f) =>
f a i -> Maybe (((g1 :+: g2) a) i)
proj2 x = case proj x of
Just (y :: g1 a i) -> Just $ inj y
_ -> liftM inj (proj x :: Maybe (g2 a i))
proj3 :: forall f g1 g2 g3 a i. (g1 :<: f, g2 :<: f, g3 :<: f) =>
f a i -> Maybe (((g1 :+: g2 :+: g3) a) i)
proj3 x = case proj x of
Just (y :: g1 a i) -> Just $ inj y
_ -> case proj x of
Just (y :: g2 a i) -> Just $ inj y
_ -> liftM inj (proj x :: Maybe (g3 a i))
project :: (g :<: f) => NatM Maybe (Cxt h f a) (g (Cxt h f a))
project (Hole _) = Nothing
project (Term t) = proj t
project2 :: (g1 :<: f, g2 :<: f) =>
NatM Maybe (Cxt h f a) ((g1 :+: g2) (Cxt h f a))
project2 (Hole _) = Nothing
project2 (Term t) = proj2 t
project3 :: (g1 :<: f, g2 :<: f, g3 :<: f) =>
NatM Maybe (Cxt h f a) ((g1 :+: g2 :+: g3) (Cxt h f a))
project3 (Hole _) = Nothing
project3 (Term t) = proj3 t
deepProject :: (HTraversable f, HFunctor g, g :<: f)
=> NatM Maybe (Cxt h f a) (Cxt h g a)
deepProject = appSigFunM proj
deepProject2 :: (HTraversable f, HFunctor g1, HFunctor g2,
g1 :<: f, g2 :<: f)
=> NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2) a)
deepProject2 = appSigFunM proj2
deepProject3 :: (HTraversable f, HFunctor g1, HFunctor g2, HFunctor g3,
g1 :<: f, g2 :<: f, g3 :<: f)
=> NatM Maybe (Cxt h f a) (Cxt h (g1 :+: g2 :+: g3) a)
deepProject3 = appSigFunM proj3
inj2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) a :-> g a
inj2 (Inl x) = inj x
inj2 (Inr y) = inj y
inj3 :: (f1 :<: g, f2 :<: g, f3 :<: g) => (f1 :+: f2 :+: f3) a :-> g a
inj3 (Inl x) = inj x
inj3 (Inr y) = inj2 y
inject :: (g :<: f) => g (Cxt h f a) :-> Cxt h f a
inject = Term . inj
inject2 :: (f1 :<: g, f2 :<: g) => (f1 :+: f2) (Cxt h g a) :-> Cxt h g a
inject2 = Term . inj2
inject3 :: (f1 :<: g, f2 :<: g, f3 :<: g)
=> (f1 :+: f2 :+: f3) (Cxt h g a) :-> Cxt h g a
inject3 = Term . inj3
deepInject :: (HFunctor g, HFunctor f, g :<: f) => Cxt h g a :-> Cxt h f a
deepInject = appSigFun inj
deepInject2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)
=> Cxt h (f1 :+: f2) a :-> Cxt h g a
deepInject2 = appSigFun inj2
deepInject3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
f1 :<: g, f2 :<: g, f3 :<: g)
=> Cxt h (f1 :+: f2 :+: f3) a :-> Cxt h g a
deepInject3 = appSigFun inj3
injectCxt :: (HFunctor g, g :<: f) => Cxt h' g (Cxt h f a) :-> Cxt h f a
injectCxt = cata' inject
liftCxt :: (HFunctor f, g :<: f) => g a :-> Context f a
liftCxt g = simpCxt $ inj g
substHoles :: (HFunctor f, HFunctor g, f :<: g)
=> (v :-> Cxt h g a) -> Cxt h' f v :-> Cxt h g a
substHoles f c = injectCxt $ hfmap f c
injectConst :: (HFunctor g, g :<: f) => Const g :-> Cxt h f a
injectConst = inject . hfmap (const undefined)
injectConst2 :: (HFunctor f1, HFunctor f2, HFunctor g, f1 :<: g, f2 :<: g)
=> Const (f1 :+: f2) :-> Cxt h g a
injectConst2 = inject2 . hfmap (const undefined)
injectConst3 :: (HFunctor f1, HFunctor f2, HFunctor f3, HFunctor g,
f1 :<: g, f2 :<: g, f3 :<: g)
=> Const (f1 :+: f2 :+: f3) :-> Cxt h g a
injectConst3 = inject3 . hfmap (const undefined)
projectConst :: (HFunctor g, g :<: f) => NatM Maybe (Cxt h f a) (Const g)
projectConst = fmap (hfmap (const (K ()))) . project