Zsyntax.Labelled.Rule.Interface

Documentation

type UCtxt a l = Set (LAxiom a l)

Type of labelled unrestricted contexts, i.e. sets of labelled axioms.

type LCtxt a l = MultiSet (Neutral a l)

Type of labelled neutral contexts, i.e. multisets of neutral labelled formulas.

data LSequent a l

Type of labelled sequents.

Constructors

LS

Fields

• lsUCtxt :: UCtxt a l
• lsLCtxt :: LCtxt a l
• lsCty :: ReactionList a
• lsConcl :: Opaque a l

Instances

(Ord a, Ord l) => Subsumable (LSequent a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

subsumes :: LSequent a l -> LSequent a l -> Bool

data SubCtxt a

Constructors

SC

Fields

• _scOnOnlyFirst :: [a]
• _scRestFirst :: [a]

subCtxtOf :: Ord a => Set a -> Set a -> SubCtxt a

class NeutralKind (k :: FKind) where

Predicate identifying those formula kinds corresponding to neutral formulas.

Methods

decideNeutral :: Either (Dict (k ~ KAtom)) (Dict (k ~ KImpl))

Instances

NeutralKind KAtom

Defined in Zsyntax.Labelled.Rule.Interface

Methods

decideNeutral :: Either (Dict (KAtom ~ KAtom)) (Dict (KAtom ~ KImpl))

NeutralKind KImpl

Defined in Zsyntax.Labelled.Rule.Interface

Methods

decideNeutral :: Either (Dict (KImpl ~ KAtom)) (Dict (KImpl ~ KImpl))

data Neutral a l

Type of neutral formulas, i.e. all formulas whose formula kind is classified as neutral by NeutralKind.

Constructors

NeutralKind k => N (LFormula k a l)

Instances

(Eq l, Eq a) => Eq (Neutral a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

(==) :: Neutral a l -> Neutral a l -> Bool

(/=) :: Neutral a l -> Neutral a l -> Bool

(Ord l, Ord a) => Ord (Neutral a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

compare :: Neutral a l -> Neutral a l -> Ordering

(<) :: Neutral a l -> Neutral a l -> Bool

(<=) :: Neutral a l -> Neutral a l -> Bool

(>) :: Neutral a l -> Neutral a l -> Bool

(>=) :: Neutral a l -> Neutral a l -> Bool

max :: Neutral a l -> Neutral a l -> Neutral a l

min :: Neutral a l -> Neutral a l -> Neutral a l

(Show a, Show l) => Show (Neutral a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

showsPrec :: Int -> Neutral a l -> ShowS

show :: Neutral a l -> String

showList :: [Neutral a l] -> ShowS

withMaybeNeutral :: LFormula k a l -> (NeutralKind k => b) -> (LFormula KConj a l -> b) -> b

withNeutral :: (forall k. NeutralKind k => LFormula k a l -> b) -> Neutral a l -> b

switchN :: (LFormula KAtom a l -> b) -> (LFormula KImpl a l -> b) -> Neutral a l -> b

newtype SchemaLCtxt a l

Linear contexts that appear in sequent schemas.

Constructors

SLC (LCtxt a l)

Instances

(Ord l, Ord a) => Semigroup (SchemaLCtxt a l)

Defined in Zsyntax.Labelled.Rule.Interface

Methods

(<>) :: SchemaLCtxt a l -> SchemaLCtxt a l -> SchemaLCtxt a l

sconcat :: NonEmpty (SchemaLCtxt a l) -> SchemaLCtxt a l

stimes :: Integral b => b -> SchemaLCtxt a l -> SchemaLCtxt a l

data ActCase

Type indicating the possible shapes of an active relation. An active relation has the form

act(delta ; omega ==>_zeta xi)[...] -> gamma' ; delta' -->> res

where either 1. xi is a formula, zeta is a control set, and res is empty, or 2. xi is empty, zeta is empty, and res is a formula.

Constructors

FullXiEmptyResult

EmptyXiFullResult

data SSchema :: * -> * -> ActCase -> * where

Sequent schemas.

Constructors

SSEmptyGoal :: SchemaLCtxt a l -> SSchema a l EmptyXiFullResult

SSFullGoal :: SchemaLCtxt a l -> ReactionList a -> Opaque a l -> SSchema a l FullXiEmptyResult

data MatchRes :: * -> * -> ActCase -> * where

Pre-sequents to be used as match results.

Constructors

MREmptyGoal :: UCtxt a l -> LCtxt a l -> MatchRes a l FullXiEmptyResult

MRFullGoal :: UCtxt a l -> LCtxt a l -> ReactionList a -> Opaque a l -> MatchRes a l EmptyXiFullResult

data ZetaXi :: * -> * -> ActCase -> * where

Constructors

FullZetaXi :: ReactionList a -> Opaque a l -> ZetaXi a l FullXiEmptyResult

EmptyZetaXi :: ZetaXi a l EmptyXiFullResult

elemBaseAll :: (Foldable f, Ord a) => f (Opaque a l) -> ElemBase a

lcBase :: Ord a => LCtxt a l -> ElemBase a