Zsyntax.Labelled.Rule.BipoleRelation

Module of derived rule relations.

Documentation

respects :: Ord a => ElemBase a -> RList (ElemBase a) (CtrlSet a) -> Bool

data tm ::: pl

Type of derivation terms-decorated data.

Constructors

(:::)

Fields

• _term :: tm
• _payload :: pl

Instances

Bifunctor (:::)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

bimap :: (a -> b) -> (c -> d) -> (a ::: c) -> b ::: d

first :: (a -> b) -> (a ::: c) -> b ::: c

second :: (b -> c) -> (a ::: b) -> a ::: c

(Eq tm, Eq pl) => Eq (tm ::: pl)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

(==) :: (tm ::: pl) -> (tm ::: pl) -> Bool

(/=) :: (tm ::: pl) -> (tm ::: pl) -> Bool

(Ord tm, Ord pl) => Ord (tm ::: pl)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

compare :: (tm ::: pl) -> (tm ::: pl) -> Ordering

(<) :: (tm ::: pl) -> (tm ::: pl) -> Bool

(<=) :: (tm ::: pl) -> (tm ::: pl) -> Bool

(>) :: (tm ::: pl) -> (tm ::: pl) -> Bool

(>=) :: (tm ::: pl) -> (tm ::: pl) -> Bool

max :: (tm ::: pl) -> (tm ::: pl) -> tm ::: pl

min :: (tm ::: pl) -> (tm ::: pl) -> tm ::: pl

(Show tm, Show pl) => Show (tm ::: pl)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

showsPrec :: Int -> (tm ::: pl) -> ShowS

show :: (tm ::: pl) -> String

showList :: [tm ::: pl] -> ShowS

Subsumable s => Subsumable (tm ::: s)

Defined in Zsyntax.Labelled.Rule.BipoleRelation

Methods

subsumes :: (tm ::: s) -> (tm ::: s) -> Bool

type AnnLSequent a l = DerivationTerm a l ::: LSequent a l

Type of labelled sequents that are annotated with a derivation term.

type BipoleRel a l = Rule (AnnLSequent a l)

A relation is an unbounded curried function with an annotated sequents as input.

type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l)

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)

Predicate identifying those formula kinds that correspond to focusable formulas.

Instances

IsFocusable KAtom

Defined in Zsyntax.Labelled.Rule.BipoleRelation

IsFocusable KConj

Defined in Zsyntax.Labelled.Rule.BipoleRelation

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)

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)

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