compdata-0.7.0.2: Compositional Data Types

Copyright (c) 2010-2011 Patrick Bahr, Tom Hvitved BSD3 Patrick Bahr experimental non-portable (GHC Extensions) None Haskell98

Data.Comp.Sum

Description

This module provides the infrastructure to extend signatures.

Synopsis

# Documentation

class sub :<: sup where Source

Signature containment relation for automatic injections. The left-hand must be an atomic signature, where as the right-hand side must have a list-like structure. Examples include `f :<: f :+: g` and `g :<: f :+: (g :+: h)`, non-examples include `f :+: g :<: f :+: (g :+: h)` and `f :<: (f :+: g) :+: h`.

Methods

inj :: sub a -> sup a Source

proj :: sup a -> Maybe (sub a) Source

Instances

 f :<: f (:<:) f g => f :<: ((:+:) h g) f :<: ((:+:) f g)

data (f :+: g) e infixr 6 Source

Formal sum of signatures (functors).

Instances

 (:<:) f g => f :<: ((:+:) h g) f :<: ((:+:) f g) (Functor f, Functor g) => Functor ((:+:) f g) (Foldable f, Foldable g) => Foldable ((:+:) f g) (Traversable f, Traversable g) => Traversable ((:+:) f g) (ShowF f, ShowF g) => ShowF ((:+:) f g) (ArbitraryF f, ArbitraryF g) => ArbitraryF ((:+:) f g) Instances of `ArbitraryF` are closed under forming sums. (NFDataF f, NFDataF g) => NFDataF ((:+:) f g) (EqF f, EqF g) => EqF ((:+:) f g) `EqF` is propagated through sums. (OrdF f, OrdF g) => OrdF ((:+:) f g) `OrdF` is propagated through sums. (HasVars f v0, HasVars g v0) => HasVars ((:+:) f g) v (Desugar f h, Desugar g h) => Desugar ((:+:) f g) h DistAnn s p s' => DistAnn ((:+:) f s) p ((:+:) ((:&:) f p) s') RemA s s' => RemA ((:+:) ((:&:) f p) s) ((:+:) f s') (Eq (f a), Eq (g a)) => Eq ((:+:) f g a) (Ord (f a), Ord (g a)) => Ord ((:+:) f g a) (Show (f a), Show (g a)) => Show ((:+:) f g a)

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

proj2 :: forall f a g1 g2. ((:<:) g1 f, (:<:) g2 f) => f a -> Maybe ((:+:) g2 g1 a) Source

proj3 :: forall f a g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => f a -> Maybe ((:+:) g3 ((:+:) g2 g1) a) Source

proj4 :: forall f a g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => f a -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) a) Source

proj5 :: forall f a g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => f a -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) a) Source

proj6 :: forall f a g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => f a -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) a) Source

proj7 :: forall f a g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => f a -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) a) Source

proj8 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => f a -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) a) Source

proj9 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => f a -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) a) Source

proj10 :: forall f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => f a -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) a) Source

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.

project2 :: forall h f a g1 g2. ((:<:) g1 f, (:<:) g2 f) => Cxt h f a -> Maybe ((:+:) g2 g1 (Cxt h f a)) Source

project3 :: forall h f a g1 g2 g3. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => Cxt h f a -> Maybe ((:+:) g3 ((:+:) g2 g1) (Cxt h f a)) Source

project4 :: forall h f a g1 g2 g3 g4. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => Cxt h f a -> Maybe ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)) (Cxt h f a)) Source

project5 :: forall h f a g1 g2 g3 g4 g5. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => Cxt h f a -> Maybe ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) (Cxt h f a)) Source

project6 :: forall h f a g1 g2 g3 g4 g5 g6. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => Cxt h f a -> Maybe ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) (Cxt h f a)) Source

project7 :: forall h f a g1 g2 g3 g4 g5 g6 g7. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => Cxt h f a -> Maybe ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) (Cxt h f a)) Source

project8 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => Cxt h f a -> Maybe ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) (Cxt h f a)) Source

project9 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => Cxt h f a -> Maybe ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) (Cxt h f a)) Source

project10 :: forall h f a g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. ((:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => Cxt h f a -> Maybe ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) (Cxt h f a)) Source

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.

deepProject2 :: forall f g1 g2. (Traversable ((:+:) g2 g1), (:<:) g1 f, (:<:) g2 f) => CxtFunM Maybe f ((:+:) g2 g1) Source

deepProject3 :: forall f g1 g2 g3. (Traversable ((:+:) g3 ((:+:) g2 g1)), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f) => CxtFunM Maybe f ((:+:) g3 ((:+:) g2 g1)) Source

deepProject4 :: forall f g1 g2 g3 g4. (Traversable ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f) => CxtFunM Maybe f ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))) Source

deepProject5 :: forall f g1 g2 g3 g4 g5. (Traversable ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f) => CxtFunM Maybe f ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))) Source

deepProject6 :: forall f g1 g2 g3 g4 g5 g6. (Traversable ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f) => CxtFunM Maybe f ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))) Source

deepProject7 :: forall f g1 g2 g3 g4 g5 g6 g7. (Traversable ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f) => CxtFunM Maybe f ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))) Source

deepProject8 :: forall f g1 g2 g3 g4 g5 g6 g7 g8. (Traversable ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f) => CxtFunM Maybe f ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))) Source

deepProject9 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9. (Traversable ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f) => CxtFunM Maybe f ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1)))))))) Source

deepProject10 :: forall f g1 g2 g3 g4 g5 g6 g7 g8 g9 g10. (Traversable ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))), (:<:) g1 f, (:<:) g2 f, (:<:) g3 f, (:<:) g4 f, (:<:) g5 f, (:<:) g6 f, (:<:) g7 f, (:<:) g8 f, (:<:) g9 f, (:<:) g10 f) => CxtFunM Maybe f ((:+:) g10 ((:+:) g9 ((:+:) g8 ((:+:) g7 ((:+:) g6 ((:+:) g5 ((:+:) g4 ((:+:) g3 ((:+:) g2 g1))))))))) Source

# Injections for Signatures and Terms

inj2 :: forall g a f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 a -> g a Source

inj3 :: forall g a f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) a -> g a Source

inj4 :: forall g a f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) a -> g a Source

inj5 :: forall g a f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) a -> g a Source

inj6 :: forall g a f1 f2 f3 f4 f5 f6. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => (:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) a -> g a Source

inj7 :: forall g a f1 f2 f3 f4 f5 f6 f7. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => (:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) a -> g a Source

inj8 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => (:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) a -> g a Source

inj9 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => (:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) a -> g a Source

inj10 :: forall g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => (:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) a -> g a Source

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.

inject2 :: forall h g a f1 f2. ((:<:) f1 g, (:<:) f2 g) => (:+:) f2 f1 (Cxt h g a) -> Cxt h g a Source

inject3 :: forall h g a f1 f2 f3. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => (:+:) f3 ((:+:) f2 f1) (Cxt h g a) -> Cxt h g a Source

inject4 :: forall h g a f1 f2 f3 f4. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => (:+:) f4 ((:+:) f3 ((:+:) f2 f1)) (Cxt h g a) -> Cxt h g a Source

inject5 :: forall h g a f1 f2 f3 f4 f5. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => (:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) (Cxt h g a) -> Cxt h g a Source

inject6 :: forall h g a f1 f2 f3 f4 f5 f6. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => (:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) (Cxt h g a) -> Cxt h g a Source

inject7 :: forall h g a f1 f2 f3 f4 f5 f6 f7. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => (:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) (Cxt h g a) -> Cxt h g a Source

inject8 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => (:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) (Cxt h g a) -> Cxt h g a Source

inject9 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => (:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) (Cxt h g a) -> Cxt h g a Source

inject10 :: forall h g a f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. ((:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => (:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) (Cxt h g a) -> Cxt h g a Source

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.

deepInject2 :: forall g f1 f2. (Functor ((:+:) f2 f1), (:<:) f1 g, (:<:) f2 g) => CxtFun ((:+:) f2 f1) g Source

deepInject3 :: forall g f1 f2 f3. (Functor ((:+:) f3 ((:+:) f2 f1)), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g) => CxtFun ((:+:) f3 ((:+:) f2 f1)) g Source

deepInject4 :: forall g f1 f2 f3 f4. (Functor ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g) => CxtFun ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))) g Source

deepInject5 :: forall g f1 f2 f3 f4 f5. (Functor ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g) => CxtFun ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))) g Source

deepInject6 :: forall g f1 f2 f3 f4 f5 f6. (Functor ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g) => CxtFun ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))) g Source

deepInject7 :: forall g f1 f2 f3 f4 f5 f6 f7. (Functor ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g) => CxtFun ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))) g Source

deepInject8 :: forall g f1 f2 f3 f4 f5 f6 f7 f8. (Functor ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g) => CxtFun ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))) g Source

deepInject9 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9. (Functor ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g) => CxtFun ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1)))))))) g Source

deepInject10 :: forall g f1 f2 f3 f4 f5 f6 f7 f8 f9 f10. (Functor ((:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))))), (:<:) f1 g, (:<:) f2 g, (:<:) f3 g, (:<:) f4 g, (:<:) f5 g, (:<:) f6 g, (:<:) f7 g, (:<:) f8 g, (:<:) f9 g, (:<:) f10 g) => CxtFun ((:+:) f10 ((:+:) f9 ((:+:) f8 ((:+:) f7 ((:+:) f6 ((:+:) f5 ((:+:) f4 ((:+:) f3 ((:+:) f2 f1))))))))) g Source

# Injections and Projections for Constants

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

injectConst2 :: (Functor f1, Functor f2, Functor g, f1 :<: g, f2 :<: g) => Const (f1 :+: f2) -> Cxt h g a Source

injectConst3 :: (Functor f1, Functor f2, Functor f3, Functor g, f1 :<: g, f2 :<: g, f3 :<: g) => Const (f1 :+: (f2 :+: f3)) -> Cxt h g a Source

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

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