public static class ParseTree.RPNStep
extends java.lang.Object
In packed format, proof steps come in three different flavors: unmarked
(for example syl
) and marked (for example 5:syl
), as well
as backreference steps (just written as numbers i.e. 5
). In
compressed format the same rules apply, except it is harder to read.
Marked steps get a Z
after the number, and backreferences are
numbers larger than the statement list. In our format, which most closely
resembles the packed format, unmarked steps have a valid stmt
and
backRef = 0
. Marked steps have a valid stmt
and
backRef < 0
: the value of -backRef
is the 1-based index
of this marked step in a list of all marked steps (this is not the
RPN index).
For backreference steps, backRef > 0
and stmt
is
null
. In this case, backRef
is the index of the marked
step that is being referenced. (One other special case is ?
steps: in this case stmt
is null
and backRef = 0
.)
Constructor and Description |
---|
RPNStep(java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String str) |
RPNStep(Stmt stmt) |
Modifier and Type | Method and Description |
---|---|
static Serializer<ParseTree.RPNStep> |
serializer(java.util.Map<java.lang.String,Stmt> stmtTbl) |
java.lang.String |
toString() |
public Stmt stmt
public int backRef
public RPNStep(Stmt stmt)
public RPNStep(java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String str)
public java.lang.String toString()
toString
in class java.lang.Object
public static Serializer<ParseTree.RPNStep> serializer(java.util.Map<java.lang.String,Stmt> stmtTbl)