Data.Comp.Sum

This module provides the infrastructure to extend signatures.

Documentation

type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g infixl 5

A constraint f :<: g expresses that the signature f is subsumed by g, i.e. f can be used to construct elements in g.

type (:=:) f g = (f :<: g, g :<: f) infixl 5

data (f :+: g) e infixr 6

Formal sum of signatures (functors).

Instances

DistAnn s p s' => DistAnn (f :+: s :: k -> *) p ((f :&: p) :+: s' :: k -> *)

Defined in Data.Comp.Ops

Methods

injectA :: p -> (f :+: s) a -> ((f :&: p) :+: s') a

projectA :: ((f :&: p) :+: s') a -> ((f :+: s) a, p)

RemA s s' => RemA ((f :&: p) :+: s :: k -> *) (f :+: s' :: k -> *)

Defined in Data.Comp.Ops

Methods

remA :: ((f :&: p) :+: s) a -> (f :+: s') a

(Functor f, Functor g) => Functor (f :+: g)

Defined in Data.Comp.Ops

Methods

fmap :: (a -> b) -> (f :+: g) a -> (f :+: g) b

(<$) :: a -> (f :+: g) b -> (f :+: g) a

(Foldable f, Foldable g) => Foldable (f :+: g)

Defined in Data.Comp.Ops

Methods

fold :: Monoid m => (f :+: g) m -> m

foldMap :: Monoid m => (a -> m) -> (f :+: g) a -> m

foldr :: (a -> b -> b) -> b -> (f :+: g) a -> b

foldr' :: (a -> b -> b) -> b -> (f :+: g) a -> b

foldl :: (b -> a -> b) -> b -> (f :+: g) a -> b

foldl' :: (b -> a -> b) -> b -> (f :+: g) a -> b

foldr1 :: (a -> a -> a) -> (f :+: g) a -> a

foldl1 :: (a -> a -> a) -> (f :+: g) a -> a

toList :: (f :+: g) a -> [a]

null :: (f :+: g) a -> Bool

length :: (f :+: g) a -> Int

elem :: Eq a => a -> (f :+: g) a -> Bool

maximum :: Ord a => (f :+: g) a -> a

minimum :: Ord a => (f :+: g) a -> a

sum :: Num a => (f :+: g) a -> a

product :: Num a => (f :+: g) a -> a

(Traversable f, Traversable g) => Traversable (f :+: g)

Defined in Data.Comp.Ops

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :+: g) a -> f0 ((f :+: g) b)

sequenceA :: Applicative f0 => (f :+: g) (f0 a) -> f0 ((f :+: g) a)

mapM :: Monad m => (a -> m b) -> (f :+: g) a -> m ((f :+: g) b)

sequence :: Monad m => (f :+: g) (m a) -> m ((f :+: g) a)

(ShowConstr f, ShowConstr g) => ShowConstr (f :+: g)

Defined in Data.Comp.Show

Methods

showConstr :: (f :+: g) a -> String

(ShowF f, ShowF g) => ShowF (f :+: g)

Defined in Data.Comp.Show

Methods

showF :: (f :+: g) String -> String

(EqF f, EqF g) => EqF (f :+: g)

EqF is propagated through sums.

Defined in Data.Comp.Equality

Methods

eqF :: Eq a => (f :+: g) a -> (f :+: g) a -> Bool

(OrdF f, OrdF g) => OrdF (f :+: g)

OrdF is propagated through sums.

Defined in Data.Comp.Ordering

Methods

compareF :: Ord a => (f :+: g) a -> (f :+: g) a -> Ordering

(NFDataF f, NFDataF g) => NFDataF (f :+: g)

Defined in Data.Comp.DeepSeq

Methods

rnfF :: NFData a => (f :+: g) a -> ()

(ArbitraryF f, ArbitraryF g) => ArbitraryF (f :+: g)

Instances of ArbitraryF are closed under forming sums.

Defined in Data.Comp.Arbitrary

Methods

arbitraryF' :: Arbitrary v => [(Int, Gen ((f :+: g) v))]

arbitraryF :: Arbitrary v => Gen ((f :+: g) v)

shrinkF :: Arbitrary v => (f :+: g) v -> [(f :+: g) v]

(Render f, Render g) => Render (f :+: g)

Defined in Data.Comp.Render

Methods

stringTreeAlg :: Alg (f :+: g) (Tree String)

(Desugar f h, Desugar g h) => Desugar (f :+: g) h

Defined in Data.Comp.Desugar

Methods

desugHom :: Hom (f :+: g) h

desugHom' :: Alg (f :+: g) (Context h a)

(HasVars f v, HasVars g v) => HasVars (f :+: g) v

Defined in Data.Comp.Variables

Methods

isVar :: (f :+: g) a -> Maybe v

bindsVars :: Mapping m a => (f :+: g) a -> m (Set v)

(Eq (f a), Eq (g a)) => Eq ((f :+: g) a)

Defined in Data.Comp.Sum

Methods

(==) :: (f :+: g) a -> (f :+: g) a -> Bool

(/=) :: (f :+: g) a -> (f :+: g) a -> Bool

(Ord (f a), Ord (g a)) => Ord ((f :+: g) a)

Defined in Data.Comp.Sum

Methods

compare :: (f :+: g) a -> (f :+: g) a -> Ordering

(<) :: (f :+: g) a -> (f :+: g) a -> Bool

(<=) :: (f :+: g) a -> (f :+: g) a -> Bool

(>) :: (f :+: g) a -> (f :+: g) a -> Bool

(>=) :: (f :+: g) a -> (f :+: g) a -> Bool

max :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

min :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

(Show (f a), Show (g a)) => Show ((f :+: g) a)

Defined in Data.Comp.Sum

Methods

showsPrec :: Int -> (f :+: g) a -> ShowS

show :: (f :+: g) a -> String

showList :: [(f :+: g) a] -> ShowS

caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b

Utility function to case on a functor sum, without exposing the internal representation of sums.

Projections for Signatures and Terms

proj :: forall f g a. f :<: g => g a -> Maybe (f a)

project :: g :<: f => Cxt h f a -> Maybe (g (Cxt h f a))

Project the outermost layer of a term to a sub signature. If the signature g is compound of n atomic signatures, use projectn instead.

deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g

Tries to coerce a termcontext to a termcontext over a sub-signature. If the signature g is compound of n atomic signatures, use deepProjectn instead.

project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))

Project the outermost layer of a term to a sub signature. If the signature g is compound of n atomic signatures, use projectn instead.

deepProject_ :: Traversable g => SigFunM Maybe f g -> CxtFunM Maybe f g

Tries to coerce a termcontext to a termcontext over a sub-signature. If the signature g is compound of n atomic signatures, use deepProjectn instead.

Injections for Signatures and Terms

inj :: forall f g a. f :<: g => f a -> g a

inject :: g :<: f => g (Cxt h f a) -> Cxt h f a

Inject a term where the outermost layer is a sub signature. If the signature g is compound of n atomic signatures, use injectn instead.

deepInject :: (Functor g, g :<: f) => CxtFun g f

Inject a term over a sub signature to a term over larger signature. If the signature g is compound of n atomic signatures, use deepInjectn instead.

inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a

Inject a term where the outermost layer is a sub signature. If the signature g is compound of n atomic signatures, use injectn instead.

deepInject_ :: Functor g => SigFun g f -> CxtFun g f

Inject a term over a sub signature to a term over larger signature. If the signature g is compound of n atomic signatures, use deepInjectn instead.

split :: f :=: (f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a

Injections and Projections for Constants

injectConst :: (Functor g, g :<: f) => Const g -> Cxt h f a

projectConst :: (Functor g, g :<: f) => Cxt h f a -> Maybe (Const g)

injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a

This function injects a whole context into another context.

liftCxt :: (Functor f, g :<: f) => g a -> Context f a

This function lifts the given functor to a context.

substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a

This function applies the given context with hole type a to a family f of contexts (possibly terms) indexed by a. That is, each hole h is replaced by the context f h.

substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a

Orphan instances

(Eq (f a), Eq (g a)) => Eq ((f :+: g) a)

Methods

(==) :: (f :+: g) a -> (f :+: g) a -> Bool

(/=) :: (f :+: g) a -> (f :+: g) a -> Bool

(Ord (f a), Ord (g a)) => Ord ((f :+: g) a)

Methods

compare :: (f :+: g) a -> (f :+: g) a -> Ordering

(<) :: (f :+: g) a -> (f :+: g) a -> Bool

(<=) :: (f :+: g) a -> (f :+: g) a -> Bool

(>) :: (f :+: g) a -> (f :+: g) a -> Bool

(>=) :: (f :+: g) a -> (f :+: g) a -> Bool

max :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

min :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

(Show (f a), Show (g a)) => Show ((f :+: g) a)

Methods

showsPrec :: Int -> (f :+: g) a -> ShowS

show :: (f :+: g) a -> String

showList :: [(f :+: g) a] -> ShowS