module Data.Comp.MultiParam.Sum
(
(:<:),
(:+:),
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,
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.MultiParam.Term
import Data.Comp.MultiParam.Algebra
import Data.Comp.MultiParam.Ops
import Data.Comp.MultiParam.Derive.Projections
import Data.Comp.MultiParam.Derive.Injections
import Data.Comp.MultiParam.HDifunctor
import Data.Comp.MultiParam.HDitraversable
$(liftM concat $ mapM projn [2..10])
project :: (g :<: f) => NatM Maybe (Cxt h f a b) (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 :: (HDitraversable g, g :<: f) => Term f i -> Maybe (Term g i)
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
$(liftM concat $ mapM injectn [2..10])
deepInject :: (HDifunctor g, g :<: f) => CxtFun g f
deepInject = appSigFun inj
$(liftM concat $ mapM deepInjectn [2..10])
injectCxt :: (HDifunctor g, g :<: f) => Cxt h g a (Cxt h f a b) :-> Cxt h f a b
injectCxt (In t) = inject $ hfmap injectCxt t
injectCxt (Hole x) = x
injectCxt (Var p) = Var p
liftCxt :: (HDifunctor f, g :<: f) => g a b :-> Cxt Hole f a b
liftCxt g = simpCxt $ inj g
instance (Show (f a b i), Show (g a b i)) => Show ((f :+: g) a b i) where
show (Inl v) = show v
show (Inr v) = show v
instance (Ord (f a b i), Ord (g a b i)) => Ord ((f :+: g) a b i) 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 i), Eq (g a b i)) => Eq ((f :+: g) a b i) where
(Inl x) == (Inl y) = x == y
(Inr x) == (Inr y) = x == y
_ == _ = False