Theory.Proof

Types to represent proofs.

Utilities

data LTree l a

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 c

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

Types

data ProofStep a

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)

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

Paths inside proofs

type ProofPath = [CaseName]

A path to a subproof.

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

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

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

insertPaths prf inserts the path to every proof node.

Folding/modifying proofs

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

Apply a function to the information of every proof step.

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

Fold a proof.

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

Annotate a proof in a bottom-up fashion.

data ProofStatus

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

Instances

Monoid ProofStatus

Binary ProofStatus

NFData ProofStatus

proofStepStatus :: ProofStep (Maybe a) -> ProofStatus

The status of a ProofStep.

Unfinished proofs

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

A proof using the sorry proof method.

unproven :: a -> Proof a

A proof denoting an unproven part of the proof.

Incremental proof construction

type IncrementalProof = Proof (Maybe System)

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

data Prover

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

Monoid Prover

runProver :: Prover -> ProofContext -> Int -> System -> IncrementalProof -> Maybe IncrementalProof

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

Map the proof generated by the prover.

orelse :: Prover -> Prover -> Prover

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

tryProver :: Prover -> Prover

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

sorryProver :: Maybe String -> Prover

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

oneStepProver :: ProofMethod -> Prover

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

focus :: ProofPath -> Prover -> Prover

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

checkAndExtendProver :: Prover -> Prover

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

replaceSorryProver :: Prover -> Prover

Replace all annotated sorry steps using the given prover.

contradictionProver :: Prover

Prover that does one contradiction step.

Explicit representation of a fully automatic prover

data SolutionExtractor

Constructors

CutDFS

CutBFS

CutNothing

Instances

Eq SolutionExtractor

Ord SolutionExtractor

Read SolutionExtractor

Show SolutionExtractor

Binary SolutionExtractor

NFData SolutionExtractor

data AutoProver

Constructors

AutoProver

Fields

apHeuristic :: Heuristic

apBound :: Maybe Int

apCut :: SolutionExtractor

Instances

Binary AutoProver

NFData AutoProver

runAutoProver :: AutoProver -> Prover

Pretty Printing

prettyProof :: HighlightDocument d => Proof a -> d

prettyProofWith

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 -> String

Convert a proof status to a redable string.

Parallel Strategy for exploring a proof

parLTreeDFS :: Strategy (LTree l a)

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

module Theory.Constraint.Solver