public class IntermediatePresentationProofFileParser extends java.lang.Object implements IProofFileParser
IntermediateProofReplayer
.
This approach is more flexible than direct parsing; for instance, it is
capable of dealing with merge rule applications.
The returned intermediate proof closely resembles the structure of the parsed proof file. Specifically, branch nodes are explicitly stored and, as in the proof file, have exactly one child (or zero in the case of an empty proof). The first node, that is also the main returned result, is a branch node with the identifier "dummy ID" that is present in every proof.
Example for parsed intermediate proof:
BranchNodeIntermediate "dummy ID" - AppNodeIntermediate - AppNodeIntermediate - ... - AppNodeIntermediate + BranchNodeIntermediate "x > 0" > AppNodeIntermediate > ... + BranchNodeIntermediate "x <= 0" > AppNodeIntermediate > ...
Note that the last open goal in an unfinished proof is not represented by a node in the intermediate representation (since no rule has been applied on the goal yet).
The results of the parser may be obtained by calling getResult()
.
IProofFileParser.ProofElementID
Constructor and Description |
---|
IntermediatePresentationProofFileParser(Proof proof) |
Modifier and Type | Method and Description |
---|---|
void |
beginExpr(IProofFileParser.ProofElementID eid,
java.lang.String str) |
void |
endExpr(IProofFileParser.ProofElementID eid,
int lineNr) |
java.util.List<java.lang.Throwable> |
getErrors() |
BranchNodeIntermediate |
getParsedResult() |
de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser.Result |
getResult() |
java.lang.String |
getStatus() |
public IntermediatePresentationProofFileParser(Proof proof)
proof
- Proof object for storing meta information about the parsed
proof.public void beginExpr(IProofFileParser.ProofElementID eid, java.lang.String str)
beginExpr
in interface IProofFileParser
public void endExpr(IProofFileParser.ProofElementID eid, int lineNr)
endExpr
in interface IProofFileParser
public de.uka.ilkd.key.proof.io.IntermediatePresentationProofFileParser.Result getResult()
public java.lang.String getStatus()
getStatus
in interface IProofFileParser
public java.util.List<java.lang.Throwable> getErrors()
getErrors
in interface IProofFileParser
public BranchNodeIntermediate getParsedResult()
Copyright © 2003-2019 The KeY-Project.