public abstract class Assrt extends Stmt
Modifier and Type | Field and Description |
---|---|
protected LogHyp[] |
logHypArray
logHypArray contains *exactly* the Assrt's Formula's LogHyp's, in
database sequence.
|
protected ScopeFrame |
mandFrame
The assertion's Mandatory Frame.
|
static java.util.Comparator<Assrt> |
NBR_LOG_HYP_SEQ
NBR_LOG_HYP_SEQ sequences by Stmt.seq
|
protected VarHyp[] |
varHypArray
varHypArray contains *exactly* the Assrt's Formula's VarHyp's, in
database sequence.
|
DESC_NBR_PROOF_REFS, exprParseTree, LABEL, logHypsL1HiLoKey, logHypsMaxDepth, nbrProofRefs
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Constructor and Description |
---|
Assrt(int seq,
java.util.List<ScopeDef> scopeDefList,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Construct using a boatload of parameters.
|
Modifier and Type | Method and Description |
---|---|
static <T extends Hyp> |
accumHypInList(java.util.List<T> hypList,
T hypNew)
Accumulate unique hypotheses (no duplicates), storing them in an array
list in order of their appearance in the database.
|
LogHyp[] |
getLogHypArray()
Return the logHypArray.
|
int |
getLogHypArrayLength()
Return the logHypArray length
|
java.lang.String |
getLogHypsL1HiLoKey()
Dynamically computes, if needed, the Hi and Lo keys of Level 1 (root) of
parse trees of logHypArray, and caches the value for later use.
|
int |
getLogHypsMaxDepth()
Dynamically computes, if needed, the larges maximum depth of parse trees
of logHypArray, and caches the value for later use.
|
ScopeFrame |
getMandFrame()
Get the Assrt's MandFrame.
|
int |
getMandHypArrayLength()
Return the *mandatory* Hyp Array.Length
|
VarHyp[] |
getMandVarHypArray()
Return the *mandatory* varHypArray.
|
int[] |
getReversePermutationForSortedHyp() |
LogHyp[] |
getSortedLogHypArray()
Return the sortedLogHypArray.
|
boolean |
isActive()
Is the Assrt "active".
|
boolean |
isExcluded() |
void |
loadLogHypArray()
Loads the logHypArray using mandFrame.
|
void |
setExcluded(boolean excluded) |
void |
setLogHypArray(LogHyp[] logHypArray)
Set the logHypArray.
|
void |
setMandFrame(ScopeFrame mandFrame)
Set the Assrt's MandFrame.
|
void |
setMandVarHypArray(VarHyp[] varHypArray)
Set the *mandatory* VarHyp Array.
|
static Assrt[] |
sortListIntoArray(java.util.List<Assrt> assrtList,
java.util.Comparator<Assrt> comparator)
Sorts a list of Assrt into an array.
|
equals, getExprParseTree, getExprRPN, getFormula, getLabel, getNbrProofRefs, getTyp, hashCode, incrementNbrProofRefs, initNbrProofRefs, renderParsedSubExpr, resetLogHypsL1HiLoKey, resetLogHypsMaxDepth, setExprParseTree, setExprRPN, setLogHypsL1HiLoKey, setLogHypsMaxDepth, setTyp, toJSONString, toString
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
protected VarHyp[] varHypArray
varHypArray is an array of length zero if the Assrt's Formula contains no variables.
Note: varHypArray is somewhat redundant, but note that MandFrame contains not only VarHyp's used in an Expression's Formula, but the LogHyp's that are in scope, and the VarHyp's used by those LogHyp's!.
protected LogHyp[] logHypArray
logHypArray is an array of length zero if the Assrt has no LogHyp's.
logHypArray is redundant with the data in ScopeFrame, but ProofAsst needs quick access to the LogHyp's as well as the actual number of LogHyp's.
protected ScopeFrame mandFrame
public static final java.util.Comparator<Assrt> NBR_LOG_HYP_SEQ
public Assrt(int seq, java.util.List<ScopeDef> scopeDefList, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws LangException
seq
- MObj.seq numberscopeDefList
- the Scope listsymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)labelS
- Label String identifying the AssrttypS
- Type Code String (first sym of formula)symList
- Formula's Expression (2nd thru nth syms)LangException
- variety of errors :)public VarHyp[] getMandVarHypArray()
Note: the "varHypArray" contains only *mandatory* VarHyp's, hence the name of this function, which is intended to highlight the point. These are the VarHyp's use in the Assrt's Formula.
getMandVarHypArray
in class Stmt
public LogHyp[] getLogHypArray()
public int getLogHypArrayLength()
public void setLogHypArray(LogHyp[] logHypArray)
logHypArray
- for the Assrt.public int getMandHypArrayLength()
getMandHypArrayLength
in class Stmt
public void setMandVarHypArray(VarHyp[] varHypArray)
varHypArray
- VarHyp's used by the Assrt.public ScopeFrame getMandFrame()
public void setMandFrame(ScopeFrame mandFrame)
mandFrame
- Assrt's MandFrame.public boolean isExcluded()
public void setExcluded(boolean excluded)
excluded
- true if this assertion is to be excluded in unification
searchpublic boolean isActive()
Yep. Always. An assertion is always "active" even if it is defined inside a scope level. (Recall that, in practice, "active" simply means that a statement can be referred to by a subsequent statement in a proof or parse RPN.)
That is because Metmath "scope" is designed primarily to limit the visibility of hypotheses so that variables can be reused with different Types and so that logical hypotheses can be applied to just a single assertion. In a sense, Metamath scopes are merely notational shorthand, and as Metamath.pdf explains, every assertion has an "Extended Frame" (look it up for more info.)
public void loadLogHypArray()
This is pretty redundant, but is an add-on for ProofAsst and is designed to be as bombproof as possible -- the output logHypArray is guaranteed to be in database sequence because it is created from MandFrame.hypArray.
public static <T extends Hyp> void accumHypInList(java.util.List<T> hypList, T hypNew)
The input "hypList" is updated with unique variable hypotheses in the expression.
Because hypList is maintained in database statement sequence order, hypList should either be empty (new) before the call, or already be in that order.
T
- the actual type of the listhypList
- List of Hyp's, updated here.hypNew
- Candidate Hyp to be added to hypList if not already there.public int getLogHypsMaxDepth()
public java.lang.String getLogHypsL1HiLoKey()
public static Assrt[] sortListIntoArray(java.util.List<Assrt> assrtList, java.util.Comparator<Assrt> comparator)
assrtList
- List of Assrt to be sorted.comparator
- Comparator to be used for the sort.public LogHyp[] getSortedLogHypArray()
public int[] getReversePermutationForSortedHyp()