- class DomainMap phi phi' supIxT where
- class DomainMap phi phi' supIxT => DomainEmbedding phi phi' supIxT where
- data SubVal supIxT v ix = MkSubVal {
- unSubVal :: v (supIxT ix)
- data IxMapId
- data IxMapBase m
- data IxMapSeq l1 l2
- type family ApplyIxMap m ix
- class MemoFam phi where
- memoFamily :: MemoFam phi => (forall ix. phi ix -> v ix) -> forall ix. phi ix -> v ix
- class FoldFam phi where
- foldFam :: (forall ix. phi ix -> b -> b) -> b -> b
- class EqFam phi where
- eqIdx :: forall ix1 ix2. phi ix1 -> phi ix2 -> Bool
- overrideIdx :: (forall ix'. phi ix' -> r ix') -> phi oix -> r oix -> phi ix -> r ix
- overrideIdxK :: EqFam phi => (forall ix'. phi ix' -> v) -> phi oix -> v -> phi ix -> v
- class ShowFam phi where
- class (FoldFam phi, ShowFam phi, EqFam phi, MemoFam phi) => Domain phi
- memoFamilyK :: MemoFam phi => (forall ix. phi ix -> v) -> forall ix. phi ix -> v
- toMemoK :: MemoFam phi => (forall ix. phi ix -> v) -> Memo phi (K0 v)
- fromMemoK :: MemoFam phi => Memo phi (K0 v) -> phi ix -> v
- class LiftFam phi where
- data LeftIx ix
- data RightIx ix
- data MergeDomain phiL phiR ix where
- LeftIdx :: phiL ix -> MergeDomain phiL phiR (LeftIx ix)
- RightIdx :: phiR ix -> MergeDomain phiL phiR (RightIx ix)
- data EitherFunctor rL rR ix where
- LeftR :: rL ix -> EitherFunctor rL rR (LeftIx ix)
- RightR :: rR ix -> EitherFunctor rL rR (RightIx ix)
- unLeftR :: EitherFunctor rL rR (LeftIx ix) -> rL ix
- unRightR :: EitherFunctor rL rR (RightIx ix) -> rR ix
Documentation
class DomainMap phi phi' supIxT => DomainEmbedding phi phi' supIxT whereSource
data SubVal supIxT v ix Source
A generic wrapper type that restricts a semantic value family over a bigger domain to a smaller domain.
type family ApplyIxMap m ix Source
memoFamily :: MemoFam phi => (forall ix. phi ix -> v ix) -> forall ix. phi ix -> v ixSource
A domain phi
that is an instance of the FoldFam
type class supports
folding over all non-terminals in the domain using the foldFam
function.
A domain phi
that is an instance of the EqFam
type class supports
overriding a function over the full domain at a single non-terminal using
the |overrideIdx| function.
eqIdx :: forall ix1 ix2. phi ix1 -> phi ix2 -> BoolSource
Test equality of two given non-terminal proof terms.
overrideIdx :: (forall ix'. phi ix' -> r ix') -> phi oix -> r oix -> phi ix -> r ixSource
Override a function over the full domain at a single non-terminal.
overrideIdxK :: EqFam phi => (forall ix'. phi ix' -> v) -> phi oix -> v -> phi ix -> vSource
Similar to the overrideIdx
function, but limited to functions whose result type is
the same for all non-terminals.
A domain phi
that is an instance of the ShowFam
type class supports
conversion of non-terminal proof terms to Strings using the showIdx
function.
class (FoldFam phi, ShowFam phi, EqFam phi, MemoFam phi) => Domain phi Source
A decent Domain phi
should instantiate the FoldFam
, ShowFam
, EqFam
and MemoFam
. Avoid
using this type class in constraints, use more specific type classes whenever possible.
Note: instances for this type class are not automatically derived, and you have to manually instantiate it with an empty implementation block.
memoFamilyK :: MemoFam phi => (forall ix. phi ix -> v) -> forall ix. phi ix -> vSource
data MergeDomain phiL phiR ix whereSource
LeftIdx :: phiL ix -> MergeDomain phiL phiR (LeftIx ix) | |
RightIdx :: phiR ix -> MergeDomain phiL phiR (RightIx ix) |
(MemoFam phiL, MemoFam phiR) => MemoFam (MergeDomain phiL phiR) | |
(FoldFam phiL, FoldFam phiR) => FoldFam (MergeDomain phiL phiR) | |
(ShowFam phiL, ShowFam phiR) => ShowFam (MergeDomain phiL phiR) | |
(EqFam phiL, EqFam phiR) => EqFam (MergeDomain phiL phiR) | |
(Domain phiL, Domain phiR) => Domain (MergeDomain phiL phiR) | |
(EpsProductionRule p, ProductionRule p, LoopProductionRule p (MergeDomain phiL phiR) (EitherFunctor rL rR)) => LoopProductionRule (IGW p phiL phiR rL rR t) (MergeDomain phiR phiL) (EitherFunctor rR rL) | |
(EpsProductionRule p, ProductionRule p, RecProductionRule p (MergeDomain phiL phiR) (EitherFunctor rL rR)) => RecProductionRule (IGW p phiL phiR rL rR t) (MergeDomain phiR phiL) (EitherFunctor rR rL) |
data EitherFunctor rL rR ix whereSource
LeftR :: rL ix -> EitherFunctor rL rR (LeftIx ix) | |
RightR :: rR ix -> EitherFunctor rL rR (RightIx ix) |
Show (rR ix) => Show (EitherFunctor rL rR (RightIx ix)) | |
Show (rL ix) => Show (EitherFunctor rL rR (LeftIx ix)) | |
(EpsProductionRule p, ProductionRule p, LoopProductionRule p (MergeDomain phiL phiR) (EitherFunctor rL rR)) => LoopProductionRule (IGW p phiL phiR rL rR t) (MergeDomain phiR phiL) (EitherFunctor rR rL) | |
(EpsProductionRule p, ProductionRule p, RecProductionRule p (MergeDomain phiL phiR) (EitherFunctor rL rR)) => RecProductionRule (IGW p phiL phiR rL rR t) (MergeDomain phiR phiL) (EitherFunctor rR rL) |
unLeftR :: EitherFunctor rL rR (LeftIx ix) -> rL ixSource
unRightR :: EitherFunctor rL rR (RightIx ix) -> rR ixSource