Safe Haskell | None |
---|---|
Language | Haskell2010 |
Module of derived rule relations.
Synopsis
- respects :: Ord a => ElemBase a -> RList (ElemBase a) (CtrlSet a) -> Bool
- data tm ::: pl = (:::) {}
- type AnnLSequent a l = DerivationTerm a l ::: LSequent a l
- type BipoleRel a l = Rule (AnnLSequent a l)
- type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l)
- class IsFocusable (k :: FKind)
- type FocMatchRes a l = MatchRes a l FullXiEmptyResult
- type DTFocMatchRes a l = DerivationTerm a l ::: FocMatchRes a l
- type DTMatchRes a l actcase = DerivationTerm a l ::: MatchRes a l actcase
- matchMultiSet :: Ord a => MultiSet a -> MultiSet a -> Maybe (MultiSet a)
- matchLinearCtxt :: (Ord a, Ord l) => SchemaLCtxt a l -> LCtxt a l -> Maybe (LCtxt a l)
- matchSchema :: (Ord a, Ord l) => SSchema a l act -> AnnLSequent a l -> Maybe (DTMatchRes a l act)
- matchRel :: (Ord a, Ord l) => LCtxt a l -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)
- positiveFocalDispatch :: (Ord l, Ord a) => LFormula k a l -> BipoleRel a l (DTFocMatchRes a l)
- leftActive :: (Ord l, Ord a) => LCtxt a l -> [Opaque a l] -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)
- focus :: (Ord l, Ord a, IsFocusable k) => LFormula k a l -> BipoleRule a l
- implLeft :: (Ord l, Ord a) => LFormula KImpl a l -> BipoleRule a l
- copyRule :: (Ord a, Ord l) => LAxiom a l -> BipoleRule a l
- implRight :: (Ord a, Ord l) => LFormula KImpl a l -> BipoleRule a l
Documentation
Type of derivation terms-decorated data.
Instances
Bifunctor (:::) Source # | |
(Eq tm, Eq pl) => Eq (tm ::: pl) Source # | |
(Ord tm, Ord pl) => Ord (tm ::: pl) Source # | |
Defined in Zsyntax.Labelled.Rule.BipoleRelation | |
(Show tm, Show pl) => Show (tm ::: pl) Source # | |
Subsumable s => Subsumable (tm ::: s) Source # | |
type AnnLSequent a l = DerivationTerm a l ::: LSequent a l Source #
Type of labelled sequents that are annotated with a derivation term.
type BipoleRel a l = Rule (AnnLSequent a l) Source #
A relation is an unbounded curried function with an annotated sequents as input.
type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l) Source #
A rule of the derived rule calculus is a relation that has derivation term-decorated sequents as both input and output.
class IsFocusable (k :: FKind) Source #
Predicate identifying those formula kinds that correspond to focusable formulas.
Instances
IsFocusable KAtom Source # | |
Defined in Zsyntax.Labelled.Rule.BipoleRelation | |
IsFocusable KConj Source # | |
Defined in Zsyntax.Labelled.Rule.BipoleRelation |
type FocMatchRes a l = MatchRes a l FullXiEmptyResult Source #
type DTFocMatchRes a l = DerivationTerm a l ::: FocMatchRes a l Source #
type DTMatchRes a l actcase = DerivationTerm a l ::: MatchRes a l actcase Source #
matchMultiSet :: Ord a => MultiSet a -> MultiSet a -> Maybe (MultiSet a) Source #
Given two multisets m1 and m2, it checks whether m1 is contained in m2, and returns the rest of m2 if it is the case.
matchLinearCtxt :: (Ord a, Ord l) => SchemaLCtxt a l -> LCtxt a l -> Maybe (LCtxt a l) Source #
matchSchema :: (Ord a, Ord l) => SSchema a l act -> AnnLSequent a l -> Maybe (DTMatchRes a l act) Source #
matchRel :: (Ord a, Ord l) => LCtxt a l -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act) Source #
positiveFocalDispatch :: (Ord l, Ord a) => LFormula k a l -> BipoleRel a l (DTFocMatchRes a l) Source #
leftActive :: (Ord l, Ord a) => LCtxt a l -> [Opaque a l] -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act) Source #
focus :: (Ord l, Ord a, IsFocusable k) => LFormula k a l -> BipoleRule a l Source #