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.System

Contents

Description

This is the public interface for constructing and deconstructing constraint systems. The interface for performing constraint solving provided by Theory.Constraint.Solver.

Synopsis

Constraints

Constraint systems

data System Source

A constraint system.

Construction

emptySystem :: CaseDistKind -> SystemSource

The empty constraint system, which is logically equivalent to true.

data SystemTraceQuantifier Source

Whether we are checking for the existence of a trace satisfiying a the current constraint system or whether we're checking that no traces satisfies the current constraint system.

formulaToSystemSource

Arguments

:: [LNGuarded]

Axioms to add

-> CaseDistKind

Case distinction kind

-> SystemTraceQuantifier

Trace quantifier

-> LNFormula 
-> System 

Returns the constraint system that has to be proven to show that given formula holds in the context of the given theory.

Node constraints

sNodes :: forall arr. Arrow arr => Lens arr System (Map NodeId RuleACInst)Source

allKDConcs :: System -> [(NodeId, RuleACInst, LNTerm)]Source

A list of all KD-conclusions in the System.

nodeRule :: NodeId -> System -> RuleACInstSource

nodeRule v accesses the rule label of node v under the assumption that it is present in the sequent.

nodeConcNode :: NodeConc -> NodeIdSource

nodeConcNode c compute the node-id of the node conclusion c.

nodePremNode :: NodePrem -> NodeIdSource

nodePremNode prem is the node that this premise is referring to.

nodePremFact :: NodePrem -> System -> LNFactSource

nodePremFact prem se computes the fact associated to premise prem in sequent se under the assumption that premise prem is a a premise in se.

nodeConcFact :: NodeConc -> System -> LNFactSource

nodeConcFact (NodeConc (v, i)) accesses the i-th conclusion of the rule associated with node v under the assumption that v is labeled with a rule that has an i-th conclusion.

resolveNodePremFact :: NodePrem -> System -> Maybe LNFactSource

All facts associated to this node premise.

resolveNodeConcFact :: NodeConc -> System -> Maybe LNFactSource

The fact associated with this node conclusion, if there is one.

Actions

allActions :: System -> [(NodeId, LNFact)]Source

All actions that hold in a sequent.

allKUActions :: System -> [(NodeId, LNFact, LNTerm)]Source

All actions that hold in a sequent.

unsolvedActionAtoms :: System -> [(NodeId, LNFact)]Source

All actions that hold in a sequent.

kuActionAtoms :: System -> [(NodeId, LNFact, LNTerm)]Source

All KU-actions.

standardActionAtoms :: System -> [(NodeId, LNFact)]Source

The standard actions, i.e., non-KU-actions.

Edge and chain constraints

sEdges :: forall arr. Arrow arr => Lens arr System (Set Edge)Source

unsolvedChains :: System -> [(NodeConc, NodePrem)]Source

All unsolved destruction chains in the constraint system.

Temporal ordering

sLessAtoms :: forall arr. Arrow arr => Lens arr System (Set (NodeId, NodeId))Source

rawLessRel :: System -> [(NodeId, NodeId)]Source

(from,to) is in rawLessRel se iff we can prove that there is a path (possibly using the Less relation) from from to to in se without appealing to transitivity.

rawEdgeRel :: System -> [(NodeId, NodeId)]Source

(from,to) is in rawEdgeRel se iff we can prove that there is an edge-path from from to to in se without appealing to transitivity.

alwaysBefore :: System -> NodeId -> NodeId -> BoolSource

Returns a predicate that is True iff the first argument happens before the second argument in all models of the sequent.

isInTrace :: System -> NodeId -> BoolSource

True iff the given node id is guaranteed to be instantiated to an index in the trace.

The last node

sLastAtom :: forall arr. Arrow arr => Lens arr System (Maybe NodeId)Source

isLast :: System -> NodeId -> BoolSource

True iff the given node id is guaranteed to be instantiated to the last index of the trace.

Equations

sEqStore :: forall arr. Arrow arr => Lens arr System EqStoreSource

sSubst :: System :-> LNSubstSource

Label to access the free substitution of the equation store.

sConjDisjEqs :: System :-> Conj (SplitId, Set LNSubstVFresh)Source

Label to access the conjunction of disjunctions of fresh substutitution in the equation store.

Formulas

sFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

sSolvedFormulas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

Lemmas

sLemmas :: forall arr. Arrow arr => Lens arr System (Set LNGuarded)Source

insertLemmas :: [LNGuarded] -> System -> SystemSource

Add lemmas / additional assumptions to a constraint system.

Keeping track of typing assumptions

data CaseDistKind Source

Case dinstinction kind that are allowed. The order of the kinds corresponds to the subkinding relation: untyped < typed.

Goals

data GoalStatus Source

The status of a Goal. Use its Semigroup instance to combine the status info of goals that collapse.

Constructors

GoalStatus 

gsSolved :: forall arr. Arrow arr => Lens arr GoalStatus BoolSource

gsLoopBreaker :: forall arr. Arrow arr => Lens arr GoalStatus BoolSource

gsNr :: forall arr. Arrow arr => Lens arr GoalStatus IntegerSource

sGoals :: forall arr. Arrow arr => Lens arr System (Map Goal GoalStatus)Source

sNextGoalNr :: forall arr. Arrow arr => Lens arr System IntegerSource

Pretty-printing

prettySystem :: HighlightDocument d => System -> dSource

Pretty print a sequent

prettyNonGraphSystem :: HighlightDocument d => System -> dSource

Pretty print the non-graph part of the sequent; i.e. equation store and clauses.