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