- 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
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