tamarin-prover-theory-0.8.5.0: Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone

Theory.Constraint.Solver.Reduction

Contents

Description

A monad for writing constraint reduction steps together with basic steps for inserting nodes, edges, actions, and equations and applying substitutions.

Synopsis

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.

Constructors

Unchanged 
Changed 

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

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.

insertGoal :: Goal -> Bool -> Reduction ()Source

Insert a Goal and store its age.

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.

Solving equalities

data SplitStrategy Source

SplitStrategy denotes if the equation store should be split into multiple equation stores.

Constructors

SplitNow 
SplitLater 

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