Portability  GHC only 

Maintainer  Simon Meier <iridcode@gmail.com> 
Safe Haskell  None 
Types to represent proofs.
 data LTree l a = LNode {}
 mergeMapsWith :: Ord k => (a > c) > (b > c) > (a > b > c) > Map k a > Map k b > Map k c
 data ProofStep a = ProofStep {
 psMethod :: ProofMethod
 psInfo :: a
 type Proof a = LTree CaseName (ProofStep a)
 type ProofPath = [CaseName]
 atPath :: Proof a > ProofPath > Maybe (Proof a)
 insertPaths :: Proof a > Proof (a, ProofPath)
 mapProofInfo :: (a > b) > Proof a > Proof b
 foldProof :: Monoid m => (ProofStep a > m) > Proof a > m
 annotateProof :: (ProofStep a > [b] > b) > Proof a > Proof b
 data ProofStatus
 proofStepStatus :: ProofStep (Maybe a) > ProofStatus
 sorry :: Maybe String > a > Proof a
 unproven :: a > Proof a
 type IncrementalProof = Proof (Maybe System)
 data Prover
 runProver :: Prover > ProofContext > Int > System > IncrementalProof > Maybe IncrementalProof
 mapProverProof :: (IncrementalProof > IncrementalProof) > Prover > Prover
 orelse :: Prover > Prover > Prover
 tryProver :: Prover > Prover
 sorryProver :: Maybe String > Prover
 oneStepProver :: ProofMethod > Prover
 focus :: ProofPath > Prover > Prover
 checkAndExtendProver :: Prover > Prover
 replaceSorryProver :: Prover > Prover
 contradictionProver :: Prover
 data SolutionExtractor
 = CutDFS
  CutBFS
  CutNothing
 data AutoProver = AutoProver {}
 runAutoProver :: AutoProver > Prover
 prettyProof :: HighlightDocument d => Proof a > d
 prettyProofWith :: HighlightDocument d => (ProofStep a > d) > (ProofStep a > d > d) > Proof a > d
 showProofStatus :: SystemTraceQuantifier > ProofStatus > String
 parLTreeDFS :: Strategy (LTree l a)
 module Theory.Constraint.Solver
Utilities
Trees with uniquely labelled edges.
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
A proof steps is a proof method together with additional contextdependent information.
ProofStep  

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
atPath :: Proof a > ProofPath > Maybe (Proof a)Source
prf
returns the subproof at the atPath
pathpath
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.
annotateProof :: (ProofStep a > [b] > b) > Proof a > Proof bSource
Annotate a proof in a bottomup fashion.
data ProofStatus Source
The status of a Proof
.
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 
proofStepStatus :: ProofStep (Maybe a) > ProofStatusSource
The status of a ProofStep
.
Unfinished proofs
Incremental proof construction
type IncrementalProof = Proof (Maybe System)Source
Incremental proofs are used to represent intermediate results of proof checking/construction.
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.
runProver :: Prover > ProofContext > Int > System > IncrementalProof > Maybe IncrementalProofSource
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 subproof, 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
data SolutionExtractor Source
data AutoProver Source
Pretty Printing
prettyProof :: HighlightDocument d => Proof a > dSource
:: 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 wellsuited for DFS traversal: As soon as a node is forced it sparks off the computation of the number of casemaps 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.
Smallstep interface to the constraint solver
module Theory.Constraint.Solver