public class ProofReplayer
extends java.lang.Object
Constructor and Description |
---|
ProofReplayer() |
Modifier and Type | Method and Description |
---|---|
static void |
run(org.antlr.v4.runtime.CharStream input,
IProofFileParser prl,
int startLine,
java.net.URL source)
Replays the proof behind the given
input . |
static void |
run(org.antlr.v4.runtime.Token token,
org.antlr.v4.runtime.CharStream input,
IProofFileParser prl,
java.net.URL source)
Replays the proof represented by the expression given in the
CharStream after the position of the
token . |
public static void run(@Nonnull org.antlr.v4.runtime.Token token, org.antlr.v4.runtime.CharStream input, IProofFileParser prl, java.net.URL source)
CharStream
after the position of the
token
.token
- the "\proof" with in the input streaminput
- a valid input streamprl
- the proof replayer instancesource
- the source of the stream, used for producing exceptions with locationsrun(CharStream, IProofFileParser, int, URL)
public static void run(org.antlr.v4.runtime.CharStream input, IProofFileParser prl, int startLine, java.net.URL source)
input
.
This method uses the KeYLexer
to lex input stream, and parse them manually
by consuming the tokens. It singals to the given IProofFileParser
at start or end of an expr.
Avoid the usage of a parser, avoids also the construction of an ASTs.input
- a valid input streamprl
- the proof replayer interfacestartLine
- the starting of the sexpr needed for prl
source
- the source of the stream, used for producing exceptions with locationsCopyright © 2003-2019 The KeY-Project.