| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Zsyntax.Labelled.Rule.Frontier
Synopsis
- data DecoratedFormula :: * -> * -> * where
- Unrestr :: LAxiom a l -> DecoratedFormula a l
- LinNeg :: LFormula KImpl a l -> DecoratedFormula a l
- LinPos :: Opaque a l -> DecoratedFormula a l
- dfLabel :: DecoratedFormula a l -> Label a l
- data GoalNSequent a l = GNS {}
- toGoalSequent :: LSequent a l -> GoalNSequent a l
- filterImpl :: [Neutral a l] -> [LFormula KImpl a l]
- frNeg :: (Ord l, Ord a) => Neutral a l -> Set (DecoratedFormula a l)
- frPos :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
- foc :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
- act :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
- frontier :: (Ord l, Ord a) => GoalNSequent a l -> Set (DecoratedFormula a l)
- generateRule :: (Ord a, Ord l) => DecoratedFormula a l -> BipoleRule a l
- type ProperRule a l = AnnLSequent a l -> BipoleRule a l
- initialRules :: (Ord a, Ord l) => GoalNSequent a l -> [BipoleRule a l]
- mayProperRule :: BipoleRule a l -> Maybe (ProperRule a l)
- maySequent :: BipoleRule a l -> Maybe (AnnLSequent a l)
Documentation
data DecoratedFormula :: * -> * -> * where Source #
Constructors
| Unrestr :: LAxiom a l -> DecoratedFormula a l | |
| LinNeg :: LFormula KImpl a l -> DecoratedFormula a l | |
| LinPos :: Opaque a l -> DecoratedFormula a l |
Instances
| (Eq l, Eq a) => Eq (DecoratedFormula a l) Source # | |
Defined in Zsyntax.Labelled.Rule.Frontier Methods (==) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # (/=) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # | |
| (Ord l, Ord a) => Ord (DecoratedFormula a l) Source # | |
Defined in Zsyntax.Labelled.Rule.Frontier Methods compare :: DecoratedFormula a l -> DecoratedFormula a l -> Ordering # (<) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # (<=) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # (>) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # (>=) :: DecoratedFormula a l -> DecoratedFormula a l -> Bool # max :: DecoratedFormula a l -> DecoratedFormula a l -> DecoratedFormula a l # min :: DecoratedFormula a l -> DecoratedFormula a l -> DecoratedFormula a l # | |
dfLabel :: DecoratedFormula a l -> Label a l Source #
data GoalNSequent a l Source #
Type of goal sequents.
A goal sequent is characterized by an unrestricted context of axioms, a (non-empty) neutral context, and a consequent formula of unspecified formula kind (i.e., an opaque formula).
Constructors
| GNS | |
Instances
| (Show a, Show l) => Show (GoalNSequent a l) Source # | |
Defined in Zsyntax.Labelled.Rule.Frontier Methods showsPrec :: Int -> GoalNSequent a l -> ShowS # show :: GoalNSequent a l -> String # showList :: [GoalNSequent a l] -> ShowS # | |
| (Ord a, Ord l) => Subsumable (GoalNSequent a l) Source # | |
Defined in Zsyntax.Labelled.Rule.Frontier Methods subsumes :: GoalNSequent a l -> GoalNSequent a l -> Bool Source # | |
toGoalSequent :: LSequent a l -> GoalNSequent a l Source #
frontier :: (Ord l, Ord a) => GoalNSequent a l -> Set (DecoratedFormula a l) Source #
Computes the frontier of a sequent.
generateRule :: (Ord a, Ord l) => DecoratedFormula a l -> BipoleRule a l Source #
type ProperRule a l = AnnLSequent a l -> BipoleRule a l Source #
Type of proper rules of the formal system, i.e. BipoleRules that take at
least one premise.
initialRules :: (Ord a, Ord l) => GoalNSequent a l -> [BipoleRule a l] Source #
Computes the set of initial rules from the frontier of a specified goal sequent.
mayProperRule :: BipoleRule a l -> Maybe (ProperRule a l) Source #
maySequent :: BipoleRule a l -> Maybe (AnnLSequent a l) Source #