Copyright | (c) 2010-2011 Patrick Bahr Tom Hvitved |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module provides the infrastructure to extend signatures.
Synopsis
- type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g
- type (:=:) f g = (f :<: g, g :<: f)
- data (f :+: g) e
- caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b
- 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))
- deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g
- project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a))
- deepProject_ :: Traversable g => SigFunM Maybe f g -> CxtFunM Maybe f g
- inj :: forall f g a. f :<: g => f a -> g a
- inject :: g :<: f => g (Cxt h f a) -> Cxt h f a
- deepInject :: (Functor g, g :<: f) => CxtFun g f
- inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a
- deepInject_ :: Functor g => SigFun g f -> CxtFun g f
- split :: f :=: (f1 :+: f2) => (f1 (Term f) -> a) -> (f2 (Term f) -> a) -> Term f -> a
- 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
- liftCxt :: (Functor f, g :<: f) => g a -> Context f a
- substHoles :: (Functor f, Functor g, f :<: g) => Cxt h' f v -> (v -> Cxt h g a) -> Cxt h g a
- substHoles' :: (Functor f, Functor g, f :<: g, Ord v) => Cxt h' f v -> Map v (Cxt h g a) -> Cxt h g a
Documentation
type (:<:) f g = Subsume (ComprEmb (Elem f g)) f g infixl 5 Source #
A constraint f :<: g
expresses that the signature f
is
subsumed by g
, i.e. f
can be used to construct elements in g
.
data (f :+: g) e infixr 6 Source #
Formal sum of signatures (functors).
Instances
DistAnn s p s' => DistAnn (f :+: s :: k -> Type) p ((f :&: p) :+: s' :: k -> Type) Source # | |
RemA s s' => RemA ((f :&: p) :+: s :: k -> Type) (f :+: s' :: k -> Type) Source # | |
(Foldable f, Foldable g) => Foldable (f :+: g) Source # | |
Defined in Data.Comp.Ops fold :: Monoid m => (f :+: g) m -> m # foldMap :: Monoid m => (a -> m) -> (f :+: g) a -> 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] # 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 # | |
(Traversable f, Traversable g) => Traversable (f :+: g) Source # | |
(Functor f, Functor g) => Functor (f :+: g) Source # | |
(ArbitraryF f, ArbitraryF g) => ArbitraryF (f :+: g) Source # | Instances of |
(NFDataF f, NFDataF g) => NFDataF (f :+: g) Source # | |
(EqF f, EqF g) => EqF (f :+: g) Source # |
|
(OrdF f, OrdF g) => OrdF (f :+: g) Source # |
|
(ShowConstr f, ShowConstr g) => ShowConstr (f :+: g) Source # | |
Defined in Data.Comp.Show showConstr :: (f :+: g) a -> String Source # | |
(ShowF f, ShowF g) => ShowF (f :+: g) Source # | |
(Render f, Render g) => Render (f :+: g) Source # | |
Defined in Data.Comp.Render | |
(Desugar f h, Desugar g h) => Desugar (f :+: g) h Source # | |
(HasVars f v, HasVars g v) => HasVars (f :+: g) v Source # | |
(Show (f a), Show (g a)) => Show ((f :+: g) a) Source # | |
(Eq (f a), Eq (g a)) => Eq ((f :+: g) a) Source # | |
(Ord (f a), Ord (g a)) => Ord ((f :+: g) a) Source # | |
Defined in Data.Comp.Sum |
caseF :: (f a -> b) -> (g a -> b) -> (f :+: g) a -> b Source #
Utility function to case on a functor sum, without exposing the internal representation of sums.
Projections for Signatures and Terms
project :: g :<: f => Cxt h f a -> Maybe (g (Cxt h f a)) Source #
Project the outermost layer of a term to a sub signature. If the signature
g
is compound of n atomic signatures, use project
n instead.
deepProject :: (Traversable g, g :<: f) => CxtFunM Maybe f g Source #
Tries to coerce a termcontext to a termcontext over a sub-signature. If
the signature g
is compound of n atomic signatures, use
deepProject
n instead.
project_ :: SigFunM Maybe f g -> Cxt h f a -> Maybe (g (Cxt h f a)) Source #
Project the outermost layer of a term to a sub signature. If the signature
g
is compound of n atomic signatures, use project
n instead.
deepProject_ :: Traversable g => SigFunM Maybe f g -> CxtFunM Maybe f g Source #
Tries to coerce a termcontext to a termcontext over a sub-signature. If
the signature g
is compound of n atomic signatures, use
deepProject
n instead.
Injections for Signatures and Terms
inject :: g :<: f => g (Cxt h f a) -> Cxt h f a Source #
Inject a term where the outermost layer is a sub signature. If the signature
g
is compound of n atomic signatures, use inject
n instead.
deepInject :: (Functor g, g :<: f) => CxtFun g f Source #
Inject a term over a sub signature to a term over larger signature. If the
signature g
is compound of n atomic signatures, use deepInject
n
instead.
inject_ :: SigFun g f -> g (Cxt h f a) -> Cxt h f a Source #
Inject a term where the outermost layer is a sub signature. If the signature
g
is compound of n atomic signatures, use inject
n instead.
deepInject_ :: Functor g => SigFun g f -> CxtFun g f Source #
Inject a term over a sub signature to a term over larger signature. If the
signature g
is compound of n atomic signatures, use deepInject
n
instead.
Injections and Projections for Constants
injectCxt :: (Functor g, g :<: f) => Cxt h' g (Cxt h f a) -> Cxt h f a Source #
This function injects a whole context into another context.
liftCxt :: (Functor f, g :<: f) => g a -> Context f a Source #
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 Source #
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 Source #
Orphan instances
(Show (f a), Show (g a)) => Show ((f :+: g) a) Source # | |
(Eq (f a), Eq (g a)) => Eq ((f :+: g) a) Source # | |
(Ord (f a), Ord (g a)) => Ord ((f :+: g) a) Source # | |