| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | None |
Tct.Proof
Description
This module defines proof objects.
- data Answer
- yesAnswer :: Answer
- certificate :: ComplexityProof p => p -> Certificate
- succeeded :: ComplexityProof p => p -> Bool
- failed :: ComplexityProof p => p -> Bool
- isTimeout :: ComplexityProof p => p -> Bool
- data PPMode
- type XmlContent = Content ()
- class ComplexityProof proof where
- answer :: proof -> Answer
- pprintProof :: proof -> PPMode -> Doc
- toXml :: proof -> XmlContent
Documentation
data Answer
The datatype Answer reflects the answer type
from the complexity competition.
Constructors
| CertAnswer Certificate | |
| MaybeAnswer | |
| NoAnswer | |
| TimeoutAnswer |
certificate :: ComplexityProof p => p -> Certificate
returns the Certificate associated
with the proof.
succeeded :: ComplexityProof p => p -> Bool
failed :: ComplexityProof p => p -> Bool
Negation of succeeded.
isTimeout :: ComplexityProof p => p -> Bool
data PPMode
Constructors
| ProofOutput | standard proof output |
| StrategyOutput | also output of extended strategy information |
| OverviewOutput | Only present an overview |
type XmlContent = Content ()
class ComplexityProof proof where
Complexity proofs should be instance of the ComplexityProof class.
Methods
Construct an Answer from the proof.
pprintProof :: proof -> PPMode -> Doc
Pretty printer of proof.
toXml :: proof -> XmlContent
Instances
| ComplexityProof Answer | |
| ComplexityProof SomeProof | |
| ComplexityProof OpenProof | |
| ComplexityProof TrivialProof | |
| ComplexityProof PopStarOrder | |
| ComplexityProof MpoOrder | |
| ComplexityProof MatrixOrder | |
| ComplexityProof ArcticOrder | |
| ComplexityProof PolynomialOrder | |
| ComplexityProof BoundsProof | |
| ComplexityProof PredicateProof | |
| ComplexityProof proof => ComplexityProof (PartialProof proof) | |
| Processor proc => ComplexityProof (Proof proc) | |
| ComplexityProof (ProofOf p) => ComplexityProof (TOProof p) | |
| ComplexityProof o => ComplexityProof (OrientationProof o) | |
| ComplexityProof proof => ComplexityProof (MaybeSubsumed proof) | |
| Processor p => ComplexityProof (OneOfProof p) | |
| Processor p => ComplexityProof (TimedProof p) | |
| (Transformer t, Processor sub) => ComplexityProof (Proof t sub) | |
| (Transformer g, Processor t, Processor e) => ComplexityProof (IteProgressProof g t e) | |
| (Processor g, Processor t, Processor e, ComplexityProof (ProofOf g), ComplexityProof (ProofOf t), ComplexityProof (ProofOf e)) => ComplexityProof (IteProof g t e) |