module Data.Comp.Param.Sum
(
(:<:),
(:+:),
caseD,
proj,
proj2,
proj3,
proj4,
proj5,
proj6,
proj7,
proj8,
proj9,
proj10,
project,
project2,
project3,
project4,
project5,
project6,
project7,
project8,
project9,
project10,
deepProject,
deepProject2,
deepProject3,
deepProject4,
deepProject5,
deepProject6,
deepProject7,
deepProject8,
deepProject9,
deepProject10,
inj,
inj2,
inj3,
inj4,
inj5,
inj6,
inj7,
inj8,
inj9,
inj10,
inject,
inject',
inject2,
inject3,
inject4,
inject5,
inject6,
inject7,
inject8,
inject9,
inject10,
deepInject,
deepInject2,
deepInject3,
deepInject4,
deepInject5,
deepInject6,
deepInject7,
deepInject8,
deepInject9,
deepInject10,
injectCxt,
liftCxt
) where
import Prelude hiding (sequence)
import Control.Monad hiding (sequence)
import Data.Comp.Param.Term
import Data.Comp.Param.Algebra
import Data.Comp.Param.Ops
import Data.Comp.Param.Derive.Projections
import Data.Comp.Param.Derive.Injections
import Data.Comp.Param.Difunctor
import Data.Comp.Param.Ditraversable
$(liftM concat $ mapM projn [2..10])
project :: (g :<: f) => Cxt h f a b -> Maybe (g a (Cxt h f a b))
project (In t) = proj t
project (Hole _) = Nothing
project (Var _) = Nothing
$(liftM concat $ mapM projectn [2..10])
deepProject :: (Ditraversable g, g :<: f) => Term f -> Maybe (Term g)
deepProject = appTSigFunM' proj
$(liftM concat $ mapM deepProjectn [2..10])
$(liftM concat $ mapM injn [2..10])
inject :: (g :<: f) => g a (Cxt h f a b) -> Cxt h f a b
inject = In . inj
inject' :: (Difunctor g, g :<: f) => g (Cxt h f a b) (Cxt h f a b) -> Cxt h f a b
inject' = inject . dimap Var id
$(liftM concat $ mapM injectn [2..10])
deepInject :: (Difunctor g, g :<: f) => Term g -> Term f
deepInject (Term t) = Term (appSigFun inj t)
$(liftM concat $ mapM deepInjectn [2..10])
injectCxt :: (Difunctor g, g :<: f) => Cxt h g a (Cxt h f a b) -> Cxt h f a b
injectCxt (In t) = inject $ difmap injectCxt t
injectCxt (Hole x) = x
injectCxt (Var p) = Var p
liftCxt :: (Difunctor f, g :<: f) => g a b -> Cxt Hole f a b
liftCxt g = simpCxt $ inj g
instance (Show (f a b), Show (g a b)) => Show ((f :+: g) a b) where
show (Inl v) = show v
show (Inr v) = show v
instance (Ord (f a b), Ord (g a b)) => Ord ((f :+: g) a b) where
compare (Inl _) (Inr _) = LT
compare (Inr _) (Inl _) = GT
compare (Inl x) (Inl y) = compare x y
compare (Inr x) (Inr y) = compare x y
instance (Eq (f a b), Eq (g a b)) => Eq ((f :+: g) a b) where
(Inl x) == (Inl y) = x == y
(Inr x) == (Inr y) = x == y
_ == _ = False