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

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




Types representing constraints.


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.




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


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.


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.