public class VarHyp extends Hyp
The VarHyp is truly a hypothesis (Hyp) in Metamath, and it is also a statement (Stmt), complete with its own label and Formula.
The Formula of a VarHyp consists of a Cnst followed by a Var. For example, "wph $f wff ph $." is the famous Metamath declaration of phi, stating that variable "ph" is a wff.
On a Tangent Concerning Type Codes and Conversions
By the way, Metamath's base language is strongly typed. Every statement must have a Type Code (every Formula is at least one Sym long and the first Sym must be a Cnst.) In addition, subsitution of an expression for a variable is permitted in Proof Verification (or parsing) only if the two statements have the same Type Code.
Apparently a less strict regime was overthrown after an inconsistency was "proved". The people of Metamathland quickly discovered the lie and revised their system to require their laws and terminology to be well-defined and impartially judged by incorruptible automatons.
Fortunately for the expressiveness of Metamath, Type Conversions can be defined. The most famous example is Syntax Axiom "cv" in set.mm:
$( All sets are classes (but not vice-versa!). $)
cv $a class x $.
Modifier and Type | Field and Description |
---|---|
ParseNode |
paSubst
paSubst is used in Proof Assistant unification and holds the root node of
a subtree which is the assigned substitution value for the VarHyp in a
single ProofStep.
|
DESC_NBR_PROOF_REFS, exprParseTree, LABEL, logHypsL1HiLoKey, logHypsMaxDepth, nbrProofRefs
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Modifier | Constructor and Description |
---|---|
|
VarHyp(int seq,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String varS,
java.lang.String labelS,
java.lang.String typS)
Construct VarHyp using sequence number plus label, Type Code and Var
Strings.
|
protected |
VarHyp(int tempVarHypSeq,
java.lang.String tempVarHypLabel,
Formula tempVarHypFormula)
Construct VarHyp using precomputed values and doing no validation.
|
Modifier and Type | Method and Description |
---|---|
void |
accumVarHypListBySeq(java.util.List<? super VarHyp> optionalVarHypList)
Accumulate VarHyp(no duplicates), storing it in an array list in order of
appearance in the database.
|
boolean |
containedInVarHypListBySeq(java.util.List<? super VarHyp> mandHypList)
Searches for this Var Hyp in an ArrayList maintained in database input
sequence.
|
int |
getMandHypArrayLength()
Return the mandatory Hyp array length for this VarHyp.
|
VarHyp[] |
getMandVarHypArray()
Return the mandatory VarHyp array for this VarHyp.
|
Var |
getVar()
Gets the Var for this VarHyp.
|
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 |
setActive(boolean active)
Sets VarHyp "active", either true or false.
|
equals, getExprParseTree, getExprRPN, getFormula, getLabel, getNbrProofRefs, getTyp, hashCode, incrementNbrProofRefs, initNbrProofRefs, resetLogHypsL1HiLoKey, resetLogHypsMaxDepth, setExprParseTree, setExprRPN, setLogHypsL1HiLoKey, setLogHypsMaxDepth, setTyp, toJSONString, toString
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
public ParseNode paSubst
Yes, this is a hokey scratchpad. In theory an array of paSubst could be devised, with one entry for each thread :-) Or not.
public VarHyp(int seq, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String varS, java.lang.String labelS, java.lang.String typS) throws LangException
seq
- MObj.seq numbersymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)varS
- Var id String.labelS
- Statement label String.typS
- Type Code id String.LangException
- if duplicate, etc.protected VarHyp(int tempVarHypSeq, java.lang.String tempVarHypLabel, Formula tempVarHypFormula)
tempVarHypSeq
- MObj.seqtempVarHypLabel
- Stmt.labeltempVarHypFormula
- Stmt.formulapublic void setActive(boolean active)
Sets "active" to true or false. Also, if the new setting is "inactive", then the associated var.activeVarHyp is set to null (which happens at the end of a scope definition -- see LogicalSystem.)
public Var getVar()
"De-embeds" the var from the VarHyp's VarHypFormula.
A "var" occurrence was stored redundantly here in VarHyp at one time, but it was not much used and was later eliminated as being "a waste of code".
public VarHyp[] getMandVarHypArray()
I'd rather not explain this one, but at the time I coded it, I must have been thinking something... It appears useless, but ...
getMandVarHypArray
in class Stmt
public int getMandHypArrayLength()
getMandHypArrayLength
in class Stmt
public 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.
renderParsedSubExpr
in class Stmt
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 void accumVarHypListBySeq(java.util.List<? super VarHyp> optionalVarHypList)
Because varHypList is maintained in database statement sequence order, varHypList should either be empty (new) before the call, or already be in that order.
optionalVarHypList
- List of Var Hyps, updated here.public boolean containedInVarHypListBySeq(java.util.List<? super VarHyp> mandHypList)
mandHypList
- List of Var Hyps