Data.Expression.Utils.Indexed.Sum

Documentation

data (f :+: g) a i infixr 8

Sum of two indexed functors

Constructors

InL (f a i)

InR (g a i)

Instances

(IShow f, IShow g) => IShow (f :+: g :: (k1 -> Type) -> k2 -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

ishow :: (f :+: g) (Const String) i -> Const String i

(IFunctor f, IFunctor g, IFunctor h, f :<<: g) => (f :: (k -> Type) -> k -> Type) :<<: (h :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

emb :: f a i -> (h :+: g) a i

res :: (h :+: g) a i -> Maybe (f a i)

(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<<: (g :+: f :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

emb :: f a i -> (g :+: f) a i

res :: (g :+: f) a i -> Maybe (f a i)

(IFunctor f, IFunctor g, IFunctor h, f :<: g) => (f :: (k -> Type) -> k -> Type) :<: (h :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

inj :: f a i -> (h :+: g) a i

prj :: (h :+: g) a i -> Maybe (f a i)

(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<: (f :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

inj :: f a i -> (f :+: g) a i

prj :: (f :+: g) a i -> Maybe (f a i)

(IEq1 f, IEq1 g) => IEq1 (f :+: g :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

ieq1 :: IEq a => (f :+: g) a j -> (f :+: g) a j -> Bool

(IFoldable f, IFoldable g) => IFoldable (f :+: g :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

ifold :: Monoid m => (f :+: g) (Const m) i' -> Const m i'

(IFunctor f, IFunctor g) => IFunctor (f :+: g :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

imap :: (forall (i' :: i0). a i' -> b i') -> forall (i' :: i0). (f :+: g) a i' -> (f :+: g) b i'

index :: (f :+: g) a i' -> Sing i'

(ITraversable f, ITraversable g) => ITraversable (f :+: g :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

itraverse :: Applicative f0 => (forall (i' :: i0). a i' -> f0 (b i')) -> forall (i' :: i0). (f :+: g) a i' -> f0 ((f :+: g) b i')

(MaybeQuantified f, MaybeQuantified g) => MaybeQuantified (f :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression

Methods

isQuantified' :: MaybeQuantified g0 => (f :+: g) (IFix g0) s -> Const Any s

freevars' :: (f :+: g) (Const [DynamicallySorted Var]) s -> Const [DynamicallySorted Var] s

Heyting (ALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

neg :: ALia BooleanSort -> ALia BooleanSort

(<=>) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Heyting (QFALia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

neg :: QFALia BooleanSort -> QFALia BooleanSort

(<=>) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Heyting (Lia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

neg :: Lia BooleanSort -> Lia BooleanSort

(<=>) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Heyting (QFLia BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

neg :: QFLia BooleanSort -> QFLia BooleanSort

(<=>) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Heyting (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(==>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

neg :: QFLogic BooleanSort -> QFLogic BooleanSort

(<=>) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

Lattice (ALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

(/\) :: ALia BooleanSort -> ALia BooleanSort -> ALia BooleanSort

Lattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

(/\) :: QFALia BooleanSort -> QFALia BooleanSort -> QFALia BooleanSort

Lattice (Lia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

(/\) :: Lia BooleanSort -> Lia BooleanSort -> Lia BooleanSort

Lattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

(/\) :: QFLia BooleanSort -> QFLia BooleanSort -> QFLia BooleanSort

Lattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

(\/) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

(/\) :: QFLogic BooleanSort -> QFLogic BooleanSort -> QFLogic BooleanSort

BoundedJoinSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: ALia BooleanSort

BoundedJoinSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFALia BooleanSort

BoundedJoinSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

bottom :: Lia BooleanSort

BoundedJoinSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLia BooleanSort

BoundedJoinSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

bottom :: QFLogic BooleanSort

BoundedMeetSemiLattice (ALia BooleanSort)

Defined in Data.Expression

Methods

top :: ALia BooleanSort

BoundedMeetSemiLattice (QFALia BooleanSort)

Defined in Data.Expression

Methods

top :: QFALia BooleanSort

BoundedMeetSemiLattice (Lia BooleanSort)

Defined in Data.Expression

Methods

top :: Lia BooleanSort

BoundedMeetSemiLattice (QFLia BooleanSort)

Defined in Data.Expression

Methods

top :: QFLia BooleanSort

BoundedMeetSemiLattice (QFLogic BooleanSort)

Defined in Data.Expression

Methods

top :: QFLogic BooleanSort

(Parseable f h, Parseable g h) => Parseable (f :+: g :: k1 -> k2 -> Type) h

Defined in Data.Expression.Parser

Methods

parser :: Proxy (f :+: g) -> Parser (DynamicallySortedFix h) -> Parser (DynamicallySortedFix h)

class (IFunctor f, IFunctor g) => f :<: g where

Inclusion relation for indexed sum functors

Methods

inj :: f a i -> g a i

prj :: g a i -> Maybe (f a i)

Instances

IFunctor f => (f :: (i -> Type) -> i -> Type) :<: (f :: (i -> Type) -> i -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

inj :: f a i0 -> f a i0

prj :: f a i0 -> Maybe (f a i0)

(IFunctor f, IFunctor g, IFunctor h, f :<: g) => (f :: (k -> Type) -> k -> Type) :<: (h :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

inj :: f a i -> (h :+: g) a i

prj :: (h :+: g) a i -> Maybe (f a i)

(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<: (f :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

inj :: f a i -> (f :+: g) a i

prj :: (f :+: g) a i -> Maybe (f a i)

class (IFunctor f, IFunctor g) => f :<<: g

Minimal complete definition

emb, res

Instances

(IFunctor f, IFunctor g, IFunctor h, f :<<: g) => (f :: (k -> Type) -> k -> Type) :<<: (h :+: g :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

emb :: f a i -> (h :+: g) a i

res :: (h :+: g) a i -> Maybe (f a i)

(IFunctor f, IFunctor g) => (f :: (k -> Type) -> k -> Type) :<<: (g :+: f :: (k -> Type) -> k -> Type)

Defined in Data.Expression.Utils.Indexed.Sum

Methods

emb :: f a i -> (g :+: f) a i

res :: (g :+: f) a i -> Maybe (f a i)

inject :: g :<: f => forall i. g (IFix f) i -> IFix f i

Inject a component into a sum.

match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i)

Try to unpack a sum into a component.

embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i

Embed a subset in a superset.

restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)

Try to restrict a superset to a subset.