public class ParseNode
extends java.lang.Object
ParseNode is dual use, and provides the tree node structure for grammatical/syntax parses -- these parse trees can be readily converted to Reverse Polish Notation (see Stmt.exprRPN) -- and for proof trees, which are normally stored in Metamath .mm files in RPN format but can easily be converted to ParseTrees.
The difference between proof and grammatical parse trees is content and purpose, there is no structural difference.
Proof step Stmt references are not restricted to Syntax Axiom and Variable Hypotheses, and can contain references to Logical Hypotheses, Logical Axioms and other Theorems. Logical Axioms and Theorems have Frames (see ScopeFrame and OptFrame) whose hypArrays contain Variable Hypotheses AND Logical Hypotheses, therefore there may be more children nodes under an Assertion's ParseNode than there are under a Syntax Axiom's ParseNode. Both proof parse trees and grammatical parse trees are required to reproduce/generate the original Statement's Formula's Expression (the 2nd through nth Symbols of the Formula), but a Proof is, in addition required to produce the entire Formula, which includes the Type Code and the Expression.
Thus, the difference between a proof and a grammatical parse is that a proof derives a theorem's Formula from Axioms with the same Type Code as the statement being proved; a grammatical parse is not under this obligation (it must generate some Type Code however!)
Also:
Modifier and Type | Class and Description |
---|---|
class |
ParseNode.SubTreeIterator |
Modifier and Type | Field and Description |
---|---|
ParseNode[] |
child
Child node array of length 0 to n.
|
int |
firstAppearance
This temporary variable is 0 if the node has one parent, -1 if the node
has multiple parents, and a positive integer when the RPN index of the
first parent is known.
|
Stmt |
stmt
Stmt object reference, either a Hyp or an Assrt.
|
Constructor and Description |
---|
ParseNode()
Default constructor.
|
ParseNode(Stmt stmt,
ParseNode... child)
Construct with a Stmt and children.
|
ParseNode(VarHyp varHyp)
Construct using a VarHyp.
|
Modifier and Type | Method and Description |
---|---|
void |
accumListVarHypUsedListBySeq(java.util.List<VarHyp> optionalVarHypList,
java.util.List<VarHyp> optionalVarHypsInUseList)
Accumulate Var Hyps used in the subtree which are also in an input list
of Var Hyps.
|
void |
accumSetOfWorkVarsUsed(java.util.List<WorkVar> workVarList)
Updates an ArrayList to maintain a set of Work Vars used in a subtree.
|
int |
accumVarHypArray(ParseNode[] varHypList,
int index)
Updates an array to maintain a set of parse trees correponding to the Var
Hyps used in a subtree.
|
void |
accumVarHypUsedListBySeq(java.util.List<? super VarHyp> varHypList)
Updates an ArrayList to maintain a set of Var Hyps used in a subtree.
|
java.lang.String |
asLisp() |
int |
calcMaxDepth()
Calculates the maximum depth of a parse sub-tree.
|
int |
checkWorkVarHasOccursIn(WorkVarHyp searchWorkVarHyp)
Check to see if or how the input searchWorkVarHyp occurs within the
current ParseNode stmt and its subtree and any substitutions made to
VarHyps via paSubst.
|
ParseNode |
cloneResolvingUpdatedWorkVars()
Clone subtree replacing any updated Work Vars with clones of their
updating subtrees.
|
ParseNode |
cloneTargetToSourceVars()
Deep clone of a ParseNode sub-tree converting Target Variables to Source
Variables.
|
Formula |
convertToFormula()
Converts a sub-tree expression to a Formula object.
|
int |
convertToFormula(Sym[] array,
int index)
Accumulate a Sym array for creating formulas.
|
ParseTree.RPNStep[] |
convertToRPN(boolean pressLeaf)
Converts a sub-tree expression to Reverse Polish Notation.
|
void |
convertToRPN(boolean pressLeaf,
ParseTree.RPNStep[] list,
int[] dat) |
int |
convertToRPNExpanded(ParseTree.RPNStep[] outRPN,
int dest)
Converts a sub-tree to Reverse Polish Notation.
|
int |
countFormulaLength() |
int |
countParseNodes(boolean expanded)
Counts nodes in a ParseNode sub-tree, and initializes the
firstAppearance field. |
ParseNode |
deepClone()
Deep clone of a ParseNode sub-tree.
|
ParseNode |
deepCloneApplyingAssrtSubst(Hyp[] assrtHypArray,
ParseNode[] assrtSubst,
java.util.List<WorkVar> workVarList)
(Deep) Clone a ParseNode while substituting a set of VarHyp substitutions
specified by a parallel Hyp array and keeping track of the Work Vars
output.
|
<T> ParseNode |
deepCloneApplyingAssrtSubst(T[] assrtHypArray,
ParseNode[] assrtSubst)
(Deep) Clone a ParseNode while substituting a set of VarHyp substitutions
specified by a parallel Hyp array.
|
ParseNode |
deepCloneApplyingStackSubst(java.util.Deque<ParseNode> stack) |
ParseNode |
deepCloneApplyingWorkVarUpdates()
(Deep) Clone a ParseNode while applying updates to WorkVars.
|
ParseNode |
deepCloneWithGrammarHypSubs(ParseNode[] matchNode,
ParseNodeHolder[] expandedReseqParam)
Clones a ParseNode while substituting for any child nodes that match the
corresponding matchNode array node.
|
ParseNode |
deepCloneWNodeSub(ParseNode matchNode,
ParseNode substNode)
Clones a sub-tree and splices in a substitution node when a given
"matchNode" is found.
|
int |
deepHashCode()
Calculates the hash code based on children deep hash code.
|
ParseNode |
findFirstVarHypNode()
Finds *first* VarHyp node in a sub-tree.
|
boolean |
hasUpdatedWorkVar()
Returns true if subtree contains a WorkVar which has a non-null assigned
substitution update.
|
boolean |
isDeepDup(ParseNode that)
Determine if sub-tree is a duplicate of this sub-tree.
|
boolean |
isDeepDup(ParseNode that,
java.util.Deque<ParseNode> compareNodeStack)
Determine if sub-tree is a duplicate of this sub-tree.
|
int |
renderParsedSubExpr(java.lang.StringBuilder sb,
int maxDepth,
int maxLength)
Converts a parse sub-tree into a sub-expression which is output into a
String Buffer.
|
ParseNode |
shallowClone()
Clone of a ParseNode but leave the sub-trees the same.
|
boolean |
squishTree(java.util.List<ParseNode> encountered) |
ParseNode.SubTreeIterator |
subTreeIterator(boolean excludeVarHyps) |
java.lang.String |
toString() |
int |
unifyWithSubtree(ParseNode parseNode,
java.util.Deque<ParseNode> nodeStack,
java.util.Deque<ParseNode> otherStack,
VarHypSubst[] subtree) |
ParseNode[] |
unifyWithSubtree(ParseNode subtreeRoot,
VarHyp[] varHypArray,
java.util.Deque<ParseNode> unifyNodeStack,
java.util.Deque<ParseNode> compareNodeStack)
Unify an input parse subtree (expression) with this subtree and return an
array of substitutions if successful, or null.
|
public Stmt stmt
public ParseNode[] child
public int firstAppearance
public ParseNode()
public ParseNode(Stmt stmt, ParseNode... child)
stmt
- a proof step.child
- children arraypublic ParseNode(VarHyp varHyp)
varHyp
- a proof or parse step.public ParseNode[] unifyWithSubtree(ParseNode subtreeRoot, VarHyp[] varHypArray, java.util.Deque<ParseNode> unifyNodeStack, java.util.Deque<ParseNode> compareNodeStack)
subtreeRoot
- root of parse subtree to unify with thisvarHypArray
- the VarHyp's in this subtreeunifyNodeStack
- work stackcompareNodeStack
- work stackpublic int unifyWithSubtree(ParseNode parseNode, java.util.Deque<ParseNode> nodeStack, java.util.Deque<ParseNode> otherStack, VarHypSubst[] subtree)
public ParseNode.SubTreeIterator subTreeIterator(boolean excludeVarHyps)
public boolean isDeepDup(ParseNode that, java.util.Deque<ParseNode> compareNodeStack)
that
- ParseNode to compare to this ParseNode.compareNodeStack
- work stack for ParseNodes.public boolean isDeepDup(ParseNode that)
that
- ParseNode to compare to this ParseNode.public int deepHashCode()
public ParseNode deepCloneWithGrammarHypSubs(ParseNode[] matchNode, ParseNodeHolder[] expandedReseqParam)
matchNode
- ParseNode array of matching ParseNodes.expandedReseqParam
- ParseNodeHolder array of nodes to splice in to
the original tree where a matchNode is found.public ParseNode deepCloneWNodeSub(ParseNode matchNode, ParseNode substNode)
Basically, this is used to splice an expression's sub-tree into a VarHyp sub-tree. Note that the original tree is on top, so we're layering another formula on top, with substituted expressions replacing the formula's hypotheses.
matchNode
- ParseNode to look for and replace.substNode
- ParseNode to replace matchNode.public ParseNode deepClone()
public ParseNode shallowClone()
public ParseNode deepCloneApplyingAssrtSubst(Hyp[] assrtHypArray, ParseNode[] assrtSubst, java.util.List<WorkVar> workVarList)
This function is a helper for mmj.pa.ProofUnifier and its friend mmj.pa.ProofWorksheet.
assrtHypArray
- parallel array for assrtSubstassrtSubst
- array of ParseNode sub-tree roots specifying hyp
substitutions.workVarList
- arrayList of WorkVar updated to contain set of Work
Vars used in the subtree. substituted into the output.public <T> ParseNode deepCloneApplyingAssrtSubst(T[] assrtHypArray, ParseNode[] assrtSubst)
T
- Type of assrtHypArrayassrtHypArray
- parallel array for assrtSubstassrtSubst
- array of ParseNode sub-tree roots specifying hyp
substitutions.public ParseNode deepCloneApplyingStackSubst(java.util.Deque<ParseNode> stack)
public ParseNode findFirstVarHypNode()
This is useful mainly for GrammarRule parse trees which have at most one VarHyp per ParseTree.root.child[i].
public int calcMaxDepth()
public int countParseNodes(boolean expanded)
firstAppearance
field.expanded
- true
if repeated subtrees are to be counted as
fully expanded, false
to count them as stubs of size 1public boolean squishTree(java.util.List<ParseNode> encountered)
public ParseTree.RPNStep[] convertToRPN(boolean pressLeaf)
Intended for creating the RPN for an expression rather than an entire formula (with ParseTree).
pressLeaf
- true
if nodes with no children should be
backreferencedpublic void convertToRPN(boolean pressLeaf, ParseTree.RPNStep[] list, int[] dat)
public int convertToRPNExpanded(ParseTree.RPNStep[] outRPN, int dest)
outRPN
- Stmt Array where RPN will be stored.dest
- location in output array to write the next Stmt reference.public int countFormulaLength()
convertToFormula()
.public Formula convertToFormula()
VerifyProofs#convertRPNToFormula(RPNStep[], String)
and
convertToRPN(boolean)
.public int convertToFormula(Sym[] array, int index)
VerifyProofs#convertRPNToFormula(RPNStep[], String)
and
convertToRPN(boolean)
.array
- The array to accumulate intoindex
- The current length of the arraypublic int renderParsedSubExpr(java.lang.StringBuilder sb, int maxDepth, int maxLength)
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 after tidying StringBuilder.
The depth of the sub-tree is checked against the input maxDepth parameter, and if the depth exceeds this number, output terminates after tidying 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.public ParseNode cloneTargetToSourceVars()
Note: this is used by UnifyWorkManager and only for "raw" substitutions which means that any variables in the tree being cloned are, by definition, target variables; we do not expect any of them to be work variables, and furthermore, we expect all of them to have assigned values.
public int checkWorkVarHasOccursIn(WorkVarHyp searchWorkVarHyp)
Note that this function is only called if the searchWorkVarHyp.paSubst == null (which means we are considering assigning a substitution). to it. AND note that it is called only if the currentNode.stmt is a WorkVarHyp.
The reason for this hokeyness is that set.mm contains loops of renames, such as &W1 := & W3 := &W1, etc. Not to mention &W1 := &W2 := &W3 := &W1. THESE are "ok" as long as the subtree depth remains 1 (e.g. not &W1 := ( &W2 -> &W1 ).
searchWorkVarHyp
- the object of the search.public boolean hasUpdatedWorkVar()
public ParseNode cloneResolvingUpdatedWorkVars()
public void accumSetOfWorkVarsUsed(java.util.List<WorkVar> workVarList)
workVarList
- List of WorkVar objects in subtree.public void accumVarHypUsedListBySeq(java.util.List<? super VarHyp> varHypList)
varHypList
- List of VarHyp objects in subtree.public int accumVarHypArray(ParseNode[] varHypList, int index)
varHypList
- List of VarHyp objects in subtree.index
- The number of accumulated VarHyps so farpublic void accumListVarHypUsedListBySeq(java.util.List<VarHyp> optionalVarHypList, java.util.List<VarHyp> optionalVarHypsInUseList)
Lists are maintained without duplicates and are in ascending database sequence.
Note: in ProofUnifier this is used to accumulate a list of optional variables that are in use in a proof.
optionalVarHypList
- List of Var Hyps being sought for accumulation.optionalVarHypsInUseList
- List of Var Hyps accumulated which are in
the formula and are in the input varList.public ParseNode deepCloneApplyingWorkVarUpdates()
This function is a helper for mmj.pa.ProofUnifier and its friend mmj.pa.ProofWorksheet.
public java.lang.String toString()
toString
in class java.lang.Object
public java.lang.String asLisp()