public class NotationRule extends GrammarRule
NotationRule objects are built from "base" Syntax Axioms, possibly modified by Type Conversion Rules and/or Nulls Permitted Rules.
At this time, only NotationRule objects are stored in the Grammar Rule Tree/Forests, though it may be that use of the Tree/Forest structures are not needed (perhaps an essential use will be found in mmj.verify.GrammarAmbiguity).
Modifier and Type | Field and Description |
---|---|
protected GRNode |
gRTail
gRTail: is an object reference pointing to the terminal node in the Rule
Tree/Forest for this grammar rule.
|
protected int |
isGimmeMatchNbr
isGimmeMatchNbr: equals 1 if the NotationRule is a "gimme match", meaning
that a match to a subsequence of an expression can be taken unequivocally
and irrevocably, regardless of the surrounding symbols (for example, in
set.mm "c0" is a gimme match).
|
isBaseRule, MAX_SEQ_NBR, maxSeqNbr, nbrHypParamsUsed, paramTransformationTree, paramVarHypNode, RULE_NBR, ruleFormatExpr, ruleHypPos, ruleNbr
Constructor and Description |
---|
NotationRule()
Default constructor.
|
NotationRule(Grammar grammar,
Axiom baseSyntaxAxiom)
Constructor -- default GrammarRule for base Syntax Axioms, which means no
parameter "transformations".
|
NotationRule(Grammar grammar,
NotationRule oldNotationRule,
int matchIndex,
GrammarRule substRule)
Construct new NotationRule using a Notation rule which is being "cloned"
and modified by substituting the paramTransformationTree from a
GrammarRule for one of the existing rule's variable hypothesis
paramTransformationTree nodes.
|
Modifier and Type | Method and Description |
---|---|
void |
addToGrammar(Grammar grammar,
Cnst[] ruleFormatExprIn)
Add rule format expression to the Rule Forest.
|
static NotationRule |
buildBaseRule(Grammar grammar,
Axiom baseSyntaxAxiom)
NotationRule "base" Syntax Axiom rule builder, which means no parameter
"transformations".
|
void |
deriveAdditionalRules(Grammar grammar)
deriveAdditionalRules based on the addition of a new GrammarRule to those
already generated and accepted.
|
void |
deriveRulesUsingNullsPermitted(Grammar grammar,
NullsPermittedRule nullsPermittedRule)
Derives new grammar rules from an existing NotationRule and a
NullsPermittedRule, which will be applied to matching variable hypothesis
nodes in the NotationRule.
|
void |
deriveRulesUsingTypeConversion(Grammar grammar,
TypeConversionRule typeConversionRule)
Derives new grammar rules from an existing NotationRule and a
TypeConversionRule, which will be applied to matching variable hypothesis
nodes in the NotationRule.
|
GrammarRule |
getDupRule(Grammar grammar,
Cnst[] ruleFormatExprIn)
Return a duplicate of the input ruleFormatExpr if it exists, or return
null.
|
Cnst[] |
getForestRuleExpr()
Returns the ruleFormatExpr for the Notation Rule after retrieving it from
the Grammar Rule Tree/Forest.
|
GRNode |
getGRTail()
Return gRTail for the NotationRule.
|
int |
getIsGimmeMatchNbr()
Return isGimmeMatchNbr for the NotationRule.
|
void |
setGRTail(GRNode gRTail)
Set the gRTail for the NotationRule.
|
void |
setIsGimmeMatchNbr(int isGimmeMatchNbr)
Set isGimmeMatchNbr for the NotationRule.
|
add, buildGrammaticalParseNode, buildRuleFormatExpr, compareTo, equals, findMatchingVarHypTyp, getBaseSyntaxAxiom, getGrammarRuleTyp, getIsBaseRule, getMaxSeqNbr, getNbrHypParamsUsed, getParamTransformationTree, getParamVarHypNode, getParseNodeHolderExpr, getRuleFormatExpr, getRuleFormatExprAsString, getRuleFormatExprFirst, getRuleFormatExprIthSymbol, getRuleHypPos, getRuleNbr, getSyntaxAxiomVarHypReseq, hashCode, setIsBaseRule, setMaxSeqNbr, setNbrHypParamsUsed, setRuleFormatExpr, showRuleFormatExprAsString, toString
protected int isGimmeMatchNbr
Note: -1 and 0 are used in mmj.verify.GrammarAmbiguity to signify "not a gimmeMatchNbr" in two different circumstances.
protected GRNode gRTail
public NotationRule()
public NotationRule(Grammar grammar, Axiom baseSyntaxAxiom)
grammar
- The Grammar.baseSyntaxAxiom
- Syntax Axiom.public NotationRule(Grammar grammar, NotationRule oldNotationRule, int matchIndex, GrammarRule substRule)
Note that the output paramTransformationTree is built using a deep clone of the existing rule's paramTransformationTree but the substituting tree does not need cloning BECAUSE when the GrammaticalParser builds a ParseTree for an expression, *it* does a full cloning operation; this, of course assumes that once a GrammarRule is created and fully populated that it is never modified (changing the grammar means rebuilding it, in other words.)
grammar
- The Grammar.oldNotationRule
- rule being "cloned".matchIndex
- index to paramVarHypNode array indicating which VarHyp
is being substituted.substRule
- the modifying rule.public static NotationRule buildBaseRule(Grammar grammar, Axiom baseSyntaxAxiom)
grammar
- The Grammar.baseSyntaxAxiom
- Syntax Axiom.public GrammarRule getDupRule(Grammar grammar, Cnst[] ruleFormatExprIn)
getDupRule
in class GrammarRule
grammar
- The Grammar.ruleFormatExprIn
- the expression to check.public void addToGrammar(Grammar grammar, Cnst[] ruleFormatExprIn)
addToGrammar
in class GrammarRule
grammar
- The Grammar object (Mr Big).ruleFormatExprIn
- the expression to add.public void deriveAdditionalRules(Grammar grammar)
A PriorityQueue is used to store new derivedGrammarRules awaiting processing (dup checking, parse checking and possible addition to the Grammar data.) The Comparator orders derived rules based on MaxSeqNbr and ruleNbr so that low Metamath sequence number statements are added to the Grammar before higher sequenced statements. The existing rules are stored in separate repositories, which are scanned, as needed, when a new rule is added; the order that the repositories are scanned is irrelevant because the PriorityQueue controls update processing sequence.
Note also that a newly derived rule may generate other derived rules, which in turn trigger other derivations; this is a "feature" (as well as a scary opportunity for an infinite loop!) The benefit is that each pair of rules may be considered separately; when processing the pair there is no need to worry about other possible Type Conversion and Null Permitted Rules. For example, an "A" Type hypothesis in a Notation Rule may be the target of a "B to A" Type Conversion, but the fact that there is a "C to B" or "C to A" conversion can be ignored -- if the "B to A" conversion generates a variant rule of the original rule, then when *that* rule comes back through the PriorityQueue, the "C to B" rule will automatically come into play. This also means that a "B to A" conversion will combine with a "C to B" conversion to generate a "C to A" conversion -- eventually.
deriveAdditionalRules
in class GrammarRule
grammar
- The Grammar.public void deriveRulesUsingNullsPermitted(Grammar grammar, NullsPermittedRule nullsPermittedRule)
grammar
- The Grammar.nullsPermittedRule
- the modifying rule.public void deriveRulesUsingTypeConversion(Grammar grammar, TypeConversionRule typeConversionRule)
Note: combinations of var hyps are not considered here, just one application of the TypeConversionRule per derived rule. The reason is that the new derived rule goes into the queue and is then itself used to create new rules (if any). Eventually all matching combinations are considered without the complexity of dealing with them here.
grammar
- The Grammar.typeConversionRule
- the modifying rule.public Cnst[] getForestRuleExpr()
getForestRuleExpr
in class GrammarRule
public GRNode getGRTail()
public void setGRTail(GRNode gRTail)
gRTail
- for the NotationRule.public int getIsGimmeMatchNbr()
public void setIsGimmeMatchNbr(int isGimmeMatchNbr)
isGimmeMatchNbr
- for the NotationRule.