Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
A monad for writing constraint reduction steps together with basic steps for inserting nodes, edges, actions, and equations and applying substitutions.
- type Reduction = StateT System (FreshT (DisjT (Reader ProofContext)))
- execReduction :: Reduction a -> ProofContext -> System -> FreshState -> Disj (System, FreshState)
- runReduction :: Reduction a -> ProofContext -> System -> FreshState -> Disj ((a, System), FreshState)
- data ChangeIndicator
- whenChanged :: Monad m => ChangeIndicator -> m () -> m ()
- applyChangeList :: [Reduction ()] -> Reduction ChangeIndicator
- whileChanging :: Reduction ChangeIndicator -> Reduction ChangeIndicator
- getProofContext :: Reduction ProofContext
- getMaudeHandle :: Reduction MaudeHandle
- labelNodeId :: NodeId -> [RuleAC] -> Reduction RuleACInst
- insertFreshNode :: [RuleAC] -> Reduction (NodeId, RuleACInst)
- insertFreshNodeConc :: [RuleAC] -> Reduction (RuleACInst, NodeConc, LNFact)
- insertGoal :: Goal -> Bool -> Reduction ()
- insertAtom :: LNAtom -> Reduction ChangeIndicator
- insertEdges :: [(NodeConc, LNFact, LNFact, NodePrem)] -> Reduction ()
- insertChain :: NodeConc -> NodePrem -> Reduction ()
- insertAction :: NodeId -> LNFact -> Reduction ChangeIndicator
- insertLess :: NodeId -> NodeId -> Reduction ()
- insertFormula :: LNGuarded -> Reduction ()
- reducibleFormula :: LNGuarded -> Bool
- markGoalAsSolved :: String -> Goal -> Reduction ()
- removeSolvedSplitGoals :: Reduction ()
- substSystem :: Reduction ChangeIndicator
- substNodes :: Reduction ChangeIndicator
- substEdges :: Reduction ()
- substLastAtom :: Reduction ()
- substLessAtoms :: Reduction ()
- substFormulas :: Reduction ()
- substSolvedFormulas :: Reduction ()
- data SplitStrategy
- = SplitNow
- | SplitLater
- solveNodeIdEqs :: [Equal NodeId] -> Reduction ChangeIndicator
- solveTermEqs :: SplitStrategy -> [Equal LNTerm] -> Reduction ChangeIndicator
- solveFactEqs :: SplitStrategy -> [Equal LNFact] -> Reduction ChangeIndicator
- solveRuleEqs :: SplitStrategy -> [Equal RuleACInst] -> Reduction ChangeIndicator
- solveSubstEqs :: SplitStrategy -> LNSubst -> Reduction ChangeIndicator
- conjoinSystem :: System -> Reduction ()
- module Logic.Connectives
The constraint Reduction
monad
type Reduction = StateT System (FreshT (DisjT (Reader ProofContext)))Source
A constraint reduction step. Its state is the current constraint system, it can generate fresh names, split over cases, and access the proof context.
execReduction :: Reduction a -> ProofContext -> System -> FreshState -> Disj (System, FreshState)Source
Run a constraint reduction returning only the updated constraint systems and the new freshness states.
runReduction :: Reduction a -> ProofContext -> System -> FreshState -> Disj ((a, System), FreshState)Source
Run a constraint reduction. Returns a list of constraint systems whose
combined solutions are equal to the solutions of the given system. This
property is obviously not enforced, but it must be respected by all
functions of type Reduction
.
Change management
data ChangeIndicator Source
Indicate whether the constraint system was changed or not.
whenChanged :: Monad m => ChangeIndicator -> m () -> m ()Source
Only apply a monadic action, if there has been a change.
applyChangeList :: [Reduction ()] -> Reduction ChangeIndicatorSource
Apply a list of changes to the proof state.
whileChanging :: Reduction ChangeIndicator -> Reduction ChangeIndicatorSource
Execute a Reduction
as long as it results in changes. Indicate whether
at least one change was performed.
Accessing the ProofContext
getProofContext :: Reduction ProofContextSource
Retrieve the ProofContext
.
getMaudeHandle :: Reduction MaudeHandleSource
Retrieve the MaudeHandle
from the ProofContext
.
Inserting nodes, edges, and atoms
labelNodeId :: NodeId -> [RuleAC] -> Reduction RuleACInstSource
Label a node-id with a fresh instance of one of the rules and
solve it's Fr
, In
, and KU
premises immediatly.
PRE: Node must not yet be labelled with a rule.
insertFreshNode :: [RuleAC] -> Reduction (NodeId, RuleACInst)Source
Insert a fresh rule node labelled with a fresh instance of one of the rules
and solve it's Fr
, In
, and KU
premises immediatly.
insertFreshNodeConc :: [RuleAC] -> Reduction (RuleACInst, NodeConc, LNFact)Source
Insert a fresh rule node labelled with a fresh instance of one of the rules and return one of the conclusions.
insertAtom :: LNAtom -> Reduction ChangeIndicatorSource
Insert an atom. Returns Changed
if another part of the constraint
system than the set of actions was changed.
insertEdges :: [(NodeConc, LNFact, LNFact, NodePrem)] -> Reduction ()Source
Insert an edge constraint. CR-rule *DG1_2* is enforced automatically, i.e., the fact equalities are enforced.
insertChain :: NodeConc -> NodePrem -> Reduction ()Source
Insert a chain constrain.
insertAction :: NodeId -> LNFact -> Reduction ChangeIndicatorSource
Insert an Action
atom. Ensures that (almost all) trivial *KU* actions
are solved immediately using rule *S_{at,u,triv}*. We currently avoid
adding intermediate products. Indicates whether nodes other than the given
action have been added to the constraint system.
FIXME: Ensure that intermediate products are also solved before stating that no rule is applicable.
insertLess :: NodeId -> NodeId -> Reduction ()Source
Insert a Less
atom. insertLess i j
means that *i < j* is added.
insertFormula :: LNGuarded -> Reduction ()Source
Insert a Guarded
formula. Ensures that existentials, conjunctions, negated
last atoms, and negated less atoms, are immediately solved using the rules
*S_exists*, *S_and*, *S_not,last*, and *S_not,less*. Only the inserted
formula is marked as solved. Other intermediate formulas are not marked.
reducibleFormula :: LNGuarded -> BoolSource
True
iff the formula can be reduced by one of the rules implemented in
insertFormula
.
Goal management
markGoalAsSolved :: String -> Goal -> Reduction ()Source
Mark the given goal as solved.
Substitution application
substSystem :: Reduction ChangeIndicatorSource
Apply the current substitution of the equation store to the remainder of the sequent.
substNodes :: Reduction ChangeIndicatorSource
Apply the current substitution of the equation store the nodes of the constraint system. Indicates whether additional equalities were added to the equations store.
substEdges :: Reduction ()Source
substLastAtom :: Reduction ()Source
substFormulas :: Reduction ()Source
Solving equalities
data SplitStrategy Source
SplitStrategy
denotes if the equation store should be split into
multiple equation stores.
solveNodeIdEqs :: [Equal NodeId] -> Reduction ChangeIndicatorSource
Add a list of node equalities to the equation store.
solveTermEqs :: SplitStrategy -> [Equal LNTerm] -> Reduction ChangeIndicatorSource
Add a list of term equalities to the equation store. And split resulting disjunction of equations according to given split strategy.
Note that updating the remaining parts of the constraint system with the
substitution has to be performed using a separate call to substSystem
.
solveFactEqs :: SplitStrategy -> [Equal LNFact] -> Reduction ChangeIndicatorSource
Add a list of fact equalities to the equation store, if possible.
solveRuleEqs :: SplitStrategy -> [Equal RuleACInst] -> Reduction ChangeIndicatorSource
Add a list of rule equalities to the equation store, if possible.
solveSubstEqs :: SplitStrategy -> LNSubst -> Reduction ChangeIndicatorSource
Add a list of equalities in substitution form to the equation store
Conjunction with another constraint System
conjoinSystem :: System -> Reduction ()Source
conjoinSystem se
conjoins the logical information in se
to the
constraint system. It assumes that the free variables in se
are shared
with the free variables in the proof state.
Convenience export
module Logic.Connectives