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

Contents

Description

Types representing constraints.

Synopsis

Guarded formulas

Graph constraints

type NodePrem = (NodeId, PremIdx)Source

A premise of a node.

type NodeConc = (NodeId, ConcIdx)Source

A conclusion of a node.

data Edge Source

A labeled edge in a derivation graph.

Constructors

Edge 

Fields

eSrc :: NodeConc
 
eTgt :: NodePrem
 

type Less = (NodeId, NodeId)Source

A *⋖* constraint between NodeIds.

Goal constraints

data Goal Source

A Goal denotes that a constraint reduction rule is applicable, which might result in case splits. We either use a heuristic to decide what goal to solve next or leave the choice to user (in case of the interactive UI).

Constructors

ActionG LVar LNFact

An action that must exist in the trace.

ChainG NodeConc NodePrem 
PremiseG NodePrem LNFact

A premise that must have an incoming direct edge.

SplitG SplitId

A case split over equalities.

DisjG (Disj LNGuarded)

A case split over a disjunction.

Pretty-printing

prettyNode :: HighlightDocument d => (NodeId, RuleACInst) -> dSource

Pretty print a node.

prettyNodePrem :: HighlightDocument d => NodePrem -> dSource

Pretty print a node premise.

prettyNodeConc :: HighlightDocument d => NodeConc -> dSource

Pretty print a node conclusion.

prettyEdge :: HighlightDocument d => Edge -> dSource

Pretty print a edge as src >-i--j-> tgt.

prettyLess :: HighlightDocument d => Less -> dSource

Pretty print a less-atom as src < tgt.

prettyGoal :: HighlightDocument d => Goal -> dSource

Pretty print a goal.