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()
.
Modifier and Type | Class and Description |
---|---|
private static class |
IntermediatePresentationProofFileParser.BuiltinRuleInformation
Information about built-in rule applications.
|
(package private) static class |
IntermediatePresentationProofFileParser.Result
Simple structure comprising the results of the parser.
|
private static class |
IntermediatePresentationProofFileParser.RuleInformation
General information about taclet and built-in rule applications.
|
private static class |
IntermediatePresentationProofFileParser.TacletInformation
Information about taclet applications.
|
IProofFileParser.ProofElementID
Modifier and Type | Field and Description |
---|---|
private NodeIntermediate |
currNode |
private java.util.LinkedList<java.lang.Throwable> |
errors |
private Proof |
proof |
private BranchNodeIntermediate |
root |
private IntermediatePresentationProofFileParser.RuleInformation |
ruleInfo |
private java.util.Stack<NodeIntermediate> |
stack |
Constructor and Description |
---|
IntermediatePresentationProofFileParser(Proof proof) |
Modifier and Type | Method and Description |
---|---|
void |
beginExpr(IProofFileParser.ProofElementID eid,
java.lang.String str) |
private BuiltInAppIntermediate |
constructBuiltInApp() |
private TacletAppIntermediate |
constructTacletApp() |
void |
endExpr(IProofFileParser.ProofElementID eid,
int lineNr) |
java.util.List<java.lang.Throwable> |
getErrors() |
BranchNodeIntermediate |
getParsedResult() |
IntermediatePresentationProofFileParser.Result |
getResult() |
java.lang.String |
getStatus() |
private boolean |
insideBuiltinIfInsts() |
private void |
loadPreferences(java.lang.String preferences)
Loads proof settings.
|
private Proof proof
private java.util.Stack<NodeIntermediate> stack
private IntermediatePresentationProofFileParser.RuleInformation ruleInfo
private BranchNodeIntermediate root
private NodeIntermediate currNode
private java.util.LinkedList<java.lang.Throwable> errors
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 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()
private TacletAppIntermediate constructTacletApp()
private BuiltInAppIntermediate constructBuiltInApp()
private void loadPreferences(java.lang.String preferences)
preferences
- The preferences to load.private boolean insideBuiltinIfInsts()