public abstract class Stmt extends MObj implements org.json.JSONString
Hyp
s (hypotheses) and
Assrt
s.
Every Stmt has a label, which uniquely identifies it within the Stmt namespace (no rule against have a Stmt with a label equal to a Sym's id though.)
Every Stmt has a Formula, even VarHyp
s.
Every Stmt also has a Type Code -- which is the first symbol of the Formula, and must be a Cnst. (This is a key point!) Everything following the Type Code in the Stmt's Formula is referred to in mmj as the "Expression" or the "Formula's Expression". (Make a note -- the nomenclature can be confusing, but Metamath requires every "formula" to have a Type Code, and what other books/works refer to as the "formula" equates to mmj's Expression.)
Metamath statements and their correspondence to mmj "Stmt":
The only goofball Metamath statements that do not form mmj Stmt's, (other than Cnst ("$c") and Var ($v) which inherit from Sym), are:
Modifier and Type | Field and Description |
---|---|
static java.util.Comparator<Stmt> |
DESC_NBR_PROOF_REFS |
protected ParseTree |
exprParseTree
exprRPN is the Reverse Polish Notation parse of the expression portion of
a statement's formula (the 2nd through nth symbols).
|
static java.util.Comparator<Stmt> |
LABEL
LABEL sequences by Stmt.label
|
protected java.lang.String |
logHypsL1HiLoKey
This contains the labels of the root node Syntax Axiom for the
Assrt.logHypArray with lowest and greates sequence numbers.
|
protected int |
logHypsMaxDepth
This contains the greatest maximum depth among Parse Trees in the
Assrt.logHypArray.
|
protected int |
nbrProofRefs |
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Modifier | Constructor and Description |
---|---|
|
Stmt(int seq,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String labelS)
Construct using sequence number and id string.
|
protected |
Stmt(int tempSeq,
java.lang.String tempLabel,
Formula tempFormula,
ParseTree tempParseTree)
Construct temp Stmt using precomputed values and doing no validation.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj)
Compare for equality with another MObj.
|
ParseTree |
getExprParseTree()
Get exprParseTree, the statement's parse tree.
|
ParseTree.RPNStep[] |
getExprRPN()
Return exprRPN, the statement's parse RPN.
|
Formula |
getFormula()
Return Stmt Formula.
|
java.lang.String |
getLabel()
Return Stmt label.
|
abstract int |
getMandHypArrayLength()
Return mandatory Hyp Array length Note: the Hyp array is different from
the VarHyp array because the Hyp array can also include LogHyp's.
|
abstract VarHyp[] |
getMandVarHypArray()
Return mandatory VarHyp Array
|
int |
getNbrProofRefs() |
Cnst |
getTyp()
Return Stmt Type Code.
|
int |
hashCode()
Computes hashcode for this MObj
|
int |
incrementNbrProofRefs() |
void |
initNbrProofRefs() |
abstract boolean |
isActive()
Is Stmt active?
|
abstract int |
renderParsedSubExpr(java.lang.StringBuilder sb,
int maxDepth,
int maxLength,
ParseNode[] child)
Converts a parse sub-tree into a sub-expression which is output into a
String Buffer.
|
void |
resetLogHypsL1HiLoKey()
Reset the computed Hi/Lo key for an Assertions LogHyps to the default
value.
|
void |
resetLogHypsMaxDepth()
Reset the computed max depth value for the LogHyps in an Assrt to the
default value.
|
void |
setExprParseTree(ParseTree parseTree)
Set exprParseTree, the statement's parse tree.
|
void |
setExprRPN(ParseTree.RPNStep[] exprRPN)
Set exprRPN, the statement's parse RPN.
|
void |
setLogHypsL1HiLoKey(java.lang.String logHypsL1HiLoKey)
Set the computed Hi/Lo key for an Assertions LogHyps.
|
void |
setLogHypsMaxDepth(int logHypsMaxDepth)
Set the computed max depth value for the LogHyps in an Assrt.
|
void |
setTyp(Cnst typ)
Set Stmt Type Code.
|
java.lang.String |
toJSONString()
Needed for JSONification of Stmts.
|
java.lang.String |
toString()
Converts to String.
|
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
protected ParseTree exprParseTree
protected int logHypsMaxDepth
protected java.lang.String logHypsL1HiLoKey
protected int nbrProofRefs
public static final java.util.Comparator<Stmt> LABEL
public static final java.util.Comparator<Stmt> DESC_NBR_PROOF_REFS
public Stmt(int seq, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String labelS) throws LangException
seq
- MObj.seq numbersymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)labelS
- Stmt label stringLangException
- if label is empty string, or is a duplicate of
another label in stmtTbl or an id in the symTbl.public abstract boolean isActive()
A Stmt defined at the global level -- outside of any scope -- is always active.
A statement defined inside a non-global scope level can only be referred to within that scope level or another scope level nested within the first.
Note: Stmt
s refer to other Stmt
s only within proofs and
exprRPN (grammatical parses), but since Syntax Axioms must be defined at
the global level, the question of a Stmt being "active" is only relevant
to proofs.
public abstract VarHyp[] getMandVarHypArray()
public abstract int getMandHypArrayLength()
public abstract int renderParsedSubExpr(java.lang.StringBuilder sb, int maxDepth, int maxLength, ParseNode[] child)
Note: this will not work for a proof node! The ParseNode's stmt must be a VarHyp or a Syntax Axiom.
The output sub-expression is generated into text not to exceed the given maxLength. If the number of output characters exceeds maxLength output terminates, possibly leaving a dirty StringBuilder.
The depth of the sub-tree is checked against the input maxDepth parameter, and if the depth exceeds this number, output terminates,, possibly leaving a dirty StringBuilder.
Depth is computed as 1 for each Notation Syntax Axiom Node. VarHyp nodes and Nulls Permitted, Type Conversion and NamedTypedConstant Syntax Axiom nodes are assigned depth = 0 for purposes of depth checking.
sb
- StringBuilder already initialized for appending characters.maxDepth
- maximum depth of Notation Syntax axioms in sub-tree to be
printed. Set to Integer.MAX_VALUE to turn off depth checking.maxLength
- maximum length of output sub-expression. Set to
Integer.MAX_VALUE to turn off depth checking.child
- array of ParseNode, corresponding to VarHyp nodes to be
substituted into the Stmt.public java.lang.String getLabel()
public Formula getFormula()
public Cnst getTyp()
public void setTyp(Cnst typ)
typ
- Stmt Type Code.public ParseTree.RPNStep[] getExprRPN()
public void setExprRPN(ParseTree.RPNStep[] exprRPN)
exprRPN
- array of Stmt!public void setLogHypsMaxDepth(int logHypsMaxDepth)
logHypsMaxDepth
- the new max depth valuepublic void resetLogHypsMaxDepth()
public void setLogHypsL1HiLoKey(java.lang.String logHypsL1HiLoKey)
logHypsL1HiLoKey
- computed value.public void resetLogHypsL1HiLoKey()
public ParseTree getExprParseTree()
public void setExprParseTree(ParseTree parseTree)
parseTree
- Parse Tree from Grammarpublic int getNbrProofRefs()
public void initNbrProofRefs()
public int incrementNbrProofRefs()
public java.lang.String toString()
Output is simply Stmt.label.
public java.lang.String toJSONString()
toJSONString
in interface org.json.JSONString
public int hashCode()
MObj
public boolean equals(java.lang.Object obj)
MObj
Equal if and only if the MObj sequence numbers are equal. and the obj to be compared to this object is not null and is a MObj as well.