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

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

Theory.Proof

Contents

Description

Types to represent proofs.

Synopsis

Utilities

data LTree l a Source

Trees with uniquely labelled edges.

Constructors

LNode 

Fields

root :: a
 
children :: Map l (LTree l a)
 

Instances

Functor (LTree l) 
Foldable (LTree l) 
Traversable (LTree l) 
(Eq l, Eq a) => Eq (LTree l a) 
(Ord l, Ord a) => Ord (LTree l a) 
(Show l, Show a) => Show (LTree l a) 
(Ord l, Binary l, Binary a) => Binary (LTree l a) 
(Ord l, NFData l, NFData a) => NFData (LTree l a) 

mergeMapsWith :: Ord k => (a -> c) -> (b -> c) -> (a -> b -> c) -> Map k a -> Map k b -> Map k cSource

O(n+m). A generalized union operator for maps with differing types.

Types

data ProofStep a Source

A proof steps is a proof method together with additional context-dependent information.

Constructors

ProofStep 

Fields

psMethod :: ProofMethod
 
psInfo :: a
 

Instances

Functor ProofStep 
Foldable ProofStep 
Traversable ProofStep 
Eq a => Eq (ProofStep a) 
Ord a => Ord (ProofStep a) 
Show a => Show (ProofStep a) 
Binary a_1627714208 => Binary (ProofStep a_1627714208) 
NFData a_1627714208 => NFData (ProofStep a_1627714208) 
HasFrees a => HasFrees (ProofStep a) 

type Proof a = LTree CaseName (ProofStep a)Source

A proof is a tree of proof steps whose edges are labelled with case names.

Paths inside proofs

type ProofPath = [CaseName]Source

A path to a subproof.

atPath :: Proof a -> ProofPath -> Maybe (Proof a)Source

prf atPath path returns the subproof at the path in prf.

insertPaths :: Proof a -> Proof (a, ProofPath)Source

insertPaths prf inserts the path to every proof node.

Folding/modifying proofs

mapProofInfo :: (a -> b) -> Proof a -> Proof bSource

Apply a function to the information of every proof step.

foldProof :: Monoid m => (ProofStep a -> m) -> Proof a -> mSource

Fold a proof.

annotateProof :: (ProofStep a -> [b] -> b) -> Proof a -> Proof bSource

Annotate a proof in a bottom-up fashion.

data ProofStatus Source

The status of a Proof.

Constructors

UndeterminedProof

All steps are unannotated

CompleteProof

The proof is complete: no annotated sorry, no annotated solved step

IncompleteProof

There is a annotated sorry, but no annotatd solved step.

TraceFound

There is an annotated solved step

Unfinished proofs

sorry :: Maybe String -> a -> Proof aSource

A proof using the sorry proof method.

unproven :: a -> Proof aSource

A proof denoting an unproven part of the proof.

Incremental proof construction

type IncrementalProof = Proof (Maybe System)Source

Incremental proofs are used to represent intermediate results of proof checking/construction.

data Prover Source

Provers whose sequencing is handled via the Monoid instance.

 p1 `mappend` p2

Is a prover that first runs p1 and then p2 on the resulting proof.

Instances

mapProverProof :: (IncrementalProof -> IncrementalProof) -> Prover -> ProverSource

Map the proof generated by the prover.

orelse :: Prover -> Prover -> ProverSource

Resorts to the second prover, if the first one is not successful.

tryProver :: Prover -> ProverSource

Try to apply a prover. If it fails, just return the original proof.

sorryProver :: Maybe String -> ProverSource

Replace the current proof with a sorry step and the given reason.

oneStepProver :: ProofMethod -> ProverSource

Try to execute one proof step using the given proof method.

focus :: ProofPath -> Prover -> ProverSource

Apply a prover only to a sub-proof, fails if the subproof doesn't exist.

checkAndExtendProver :: Prover -> ProverSource

Check the proof and handle new cases using the given prover.

replaceSorryProver :: Prover -> ProverSource

Replace all annotated sorry steps using the given prover.

contradictionProver :: ProverSource

Prover that does one contradiction step.

Explicit representation of a fully automatic prover

Pretty Printing

prettyProofWithSource

Arguments

:: HighlightDocument d 
=> (ProofStep a -> d)

Make proof step pretty

-> (ProofStep a -> d -> d)

Make whole case pretty

-> Proof a

The proof to prettify

-> d 

showProofStatus :: SystemTraceQuantifier -> ProofStatus -> StringSource

Convert a proof status to a redable string.

Parallel Strategy for exploring a proof

parLTreeDFS :: Strategy (LTree l a)Source

A parallel evaluation strategy well-suited for DFS traversal: As soon as a node is forced it sparks off the computation of the number of case-maps of all its children. This way most of the data is already evaulated, when the actual DFS traversal visits it.

NOT used for now. It sometimes required too much memory.

Small-step interface to the constraint solver