public class Axiom extends Assrt
There are actually several different kinds of Axioms: Syntax Axioms, Definitions and Logical Axioms. mmj does not distinguish (presently) between Definitions and Logical Axioms, but mmj.verify.Grammar is *very* interested in Syntax Axioms :)
Some Syntax Axiom specific information is stored here. The Syntax related information is stored by mmj.verify.Grammar and is generally unavailable until the grammar has been successfully initialized.
A few more words are in order...to save space later...
int[] syntaxAxiomVarHypReseq
Array of indexes for
resequencing a Syntax Axiom's VarHyp's from order of appearance in the
Axiom's Formula to database sequence.
Stmt VarHypArray's are stored in .seq order -- appearance in database. Counter-intuitively, RPN's must adhere to the same sequence for variables -- i.e. "wph wps wi" is correct because wph appears before wps in the database, not because ph appears before ps in wi.
For each Notation Syntax Axiom whose formula's variables appear in a different order than their variable hypotheses database sequence -- that is, for Notation Syntax Axioms whose variables must be resequenced -- this array is present; for all others, it is null (that means that we will not store arrays such as [ 0, 1, 2] because no resequencing need be done.
Example: wsbc
Notation=wsbc, Typ wff: [ class ___ / set ___ ] wff ___
Axiom seq= 27140 label=wsbc formula=wff [ A / x ] ph
VarHyp seq= 120 label=wph formula=wff ph
VarHyp seq= 12840 label=vx formula=set x
VarHyp seq= 19860 label=cA formula=class A
syntaxAxiomVarHypReseq = {2, 1, 0}
Therefore...Stmt.exprRPN would be displayed as "wph vx cA wsbc" AND when wsbc is used to create a more complex formula, the RPN for that formula will reflect the resequenced VarHyp's.
NOTE: The reason for all of this is the way the Proof Verifier works: hypotheses are pushed onto the referenced assertion's hypothesis stack in database sequence, and substitutions from the Proof Work stack are made positionally. The RPN's *must* reflect this or else they would substitute expressions for the wrong variables.
NOTE2: A "hidden" requirement for axioms we deem "Notation Syntax Axioms" is that no variable can appear more than once in the formula. This is seemingly paradoxical because Notation Axiom variables are positional -- the variable type matters, not the name -- except for the problem of .seq on the hypothesis stack. Think about it: if "wi" were coded as "wi $a wff ( ph -> ph ) $." would it be saying that there is one variable or two? And if two, what would be their sequence on the hypothesis stack. Thus, we'll have to have a validation error message for this scenario!
logHypArray, mandFrame, NBR_LOG_HYP_SEQ, varHypArray
DESC_NBR_PROOF_REFS, exprParseTree, LABEL, logHypsL1HiLoKey, logHypsMaxDepth, nbrProofRefs
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Constructor and Description |
---|
Axiom(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 the whole enchilada of parameters!
|
Modifier and Type | Method and Description |
---|---|
boolean |
getIsSyntaxAxiom()
Answer, Is Axiom a Syntax Axiom?
|
boolean |
getSyntaxAxiomHasUniqueCnst()
Return syntaxAxiomHasUniqueCnst, true or false.
|
int[] |
getSyntaxAxiomVarHypReseq()
Return Axiom's syntaxAxiomVarHypReseq.
|
int[] |
getSyntaxAxiomVarHypReseqInv()
Return Axiom's syntaxAxiomVarHypReseqInv.
|
int |
getWidthOfWidestExprCnst()
Gets the width in characters of the widest constant in the Axiom's
Formula's Expression.
|
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 |
setIsSyntaxAxiom(boolean isSyntaxAxiom)
Set isSyntaxAxiom, true or false.
|
void |
setSyntaxAxiomHasUniqueCnst(boolean syntaxAxiomHasUniqueCnst)
Set syntaxAxiomHasUniqueCnst, true or false.
|
void |
setSyntaxAxiomVarHypReseq(int[] syntaxAxiomVarHypReseq)
Set Axiom's syntaxAxiomVarHypReseq (may be null).
|
accumHypInList, getLogHypArray, getLogHypArrayLength, getLogHypsL1HiLoKey, getLogHypsMaxDepth, getMandFrame, getMandHypArrayLength, getMandVarHypArray, getReversePermutationForSortedHyp, getSortedLogHypArray, isActive, isExcluded, loadLogHypArray, setExcluded, setLogHypArray, setMandFrame, setMandVarHypArray, sortListIntoArray
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 Axiom(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 sequence numberscopeDefList
- Scope info in effect at the timesymTbl
- Symbol Table (Map)stmtTbl
- Statement Table (Map)labelS
- Axiom label StringtypS
- Axiom Formula Type Code StringsymList
- Axiom Expression Sym String List.LangException
- if an error occurredpublic int[] getSyntaxAxiomVarHypReseq()
Array of indexes for resequencing a Syntax Axiom's VarHyp's from order of appearance in the Axiom's Formula to database sequence.
public int[] getSyntaxAxiomVarHypReseqInv()
Array of indexes for resequencing a Syntax Axiom's VarHyp's from database sequence to order of appearance in the Axiom's Formula.
public void setSyntaxAxiomVarHypReseq(int[] syntaxAxiomVarHypReseq)
Array of indexes for resequencing a Syntax Axiom's VarHyp's from order of appearance in the Axiom's Formula to database sequence.
syntaxAxiomVarHypReseq
- array of int.public boolean getIsSyntaxAxiom()
An Axiom is a "Syntax Axiom" if its Type Code is not equal to a mmj.verify.Grammar "provableLogicStmtTyp" (i.e. "|-", the default -- see mmj.verify.Grammar).
This answer is unavailable until Grammar has been initialized successfully.
public void setIsSyntaxAxiom(boolean isSyntaxAxiom)
isSyntaxAxiom
- true or false.public boolean getSyntaxAxiomHasUniqueCnst()
True for Syntax Axiom whose Formula Expression contains a Sym such that ((Cnst)sym[i])).getNbrOccInSyntaxAxioms == 1.
public void setSyntaxAxiomHasUniqueCnst(boolean syntaxAxiomHasUniqueCnst)
True for Syntax Axiom whose Formula Expression contains a Sym such that ((Cnst)sym[i])).getNbrOccInSyntaxAxioms == 1.
syntaxAxiomHasUniqueCnst
- true or false.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 int getWidthOfWidestExprCnst()
Used for the TMFF project, and used only with Syntax Axioms.