public class NullsPermittedRule extends GrammarRule
In Metamath terms, a Nulls Permitted Rule can be derived from a $a
statement whose Formula has length equal to 1.
For example: wffNullOK $a wff $.
states that wff-type variables and
expressions may be empty or "null".
Nulls Permitted Rules can also be derived from other Grammar Rules, including Type Conversion Rules and Notation Rules. Things get complicated very quickly when using Nulls! Look at this example:
$c NUMBER INTEGER $.
$v x y z i j k $.
NX $f NUMBER x $.
Ii $f INTEGER i $.
NullOkINTEGER $a INTEGER $.
ConvINTEGER $a NUMBER i $.
What that says is that we have two grammatical Type Codes, "NUMBER" and "INTEGER", with NUMBER variables x, y, z and INTEGER variables i, j, and k. And it says that INTEGER has Nulls Permitted, and that every INTEGER is a NUMBER. But it implies -- generates -- NUMBER has Nulls Permitted also! A Nulls Permitted Rule is derived from Type Conversion statement "ConvInteger" using statement "NullOkINTEGER".
Similar derivations occur with Notation Rules when Nulls and Type Conversions are involved. Very tricky stuff!
isBaseRule, MAX_SEQ_NBR, maxSeqNbr, nbrHypParamsUsed, paramTransformationTree, paramVarHypNode, RULE_NBR, ruleFormatExpr, ruleHypPos, ruleNbr
Constructor and Description |
---|
NullsPermittedRule()
Default constructor.
|
NullsPermittedRule(Grammar grammar,
Axiom baseSyntaxAxiom)
Constructor -- default GrammarRule for base Syntax Axioms, which means no
parameter "transformations".
|
NullsPermittedRule(Grammar grammar,
GrammarRule oldGrammarRule,
int matchIndex,
NullsPermittedRule nullsPermittedRule)
Build new NullsPermittedRule using an existing GrammarRule which is being
"cloned" and modified by substituting the paramTransformationTree from a
NullsPermittedRule for one of the existing rule's variable hypothesis
paramTransformationTree nodes.
|
Modifier and Type | Method and Description |
---|---|
void |
addToGrammar(Grammar grammar,
Cnst[] ruleFormatExprIn)
Add Nulls Permitted rule format expression to the system "repository".
|
static NullsPermittedRule |
buildBaseRule(Grammar grammar,
Axiom baseSyntaxAxiom)
Nulls Permitted Rule builder for base Syntax Axioms, which means no
parameter "transformations".
|
void |
deriveAdditionalRules(Grammar grammar)
deriveAdditionalRules based on the addition of a new GrammarRule to those
already generated and accepted.
|
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 Nulls Permitted Rule, simulating
retrieving it from the Grammar Rule Tree/Forest.
|
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
public NullsPermittedRule()
public NullsPermittedRule(Grammar grammar, Axiom baseSyntaxAxiom)
grammar
- The Grammar.baseSyntaxAxiom
- Syntax Axiom.public NullsPermittedRule(Grammar grammar, GrammarRule oldGrammarRule, int matchIndex, NullsPermittedRule nullsPermittedRule)
Note that the output paramTransformationTree is built using a deep clone of the existing rules 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.)
Example, a TypeConversionRule is morphed into a NullsPermittedRule by substituting the NullsPermitted paramTransformationTree for the TypeConversionRule's variable hypothesis.
grammar
- The Grammar.oldGrammarRule
- rule being "cloned".matchIndex
- index to paramVarHypNode array indicating which VarHyp
is being substituted.nullsPermittedRule
- the modifying rule.public static NullsPermittedRule 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.
NullsPermittedRule.deriveAdditionalRules -- The new NullsPermittedRule may generate variants of of NullsPermittedRules, TypeConversionRules and NotationRules. A NullsPermittedRule can be substituted *into* any matching hypothesis, and the resulting GrammarRule can morph!
deriveAdditionalRules
in class GrammarRule
grammar
- The Grammar.public Cnst[] getForestRuleExpr()
In reality, the ruleFormatExpr for a Nulls Permitted Rule is an zero-length sequence of symbol...
getForestRuleExpr
in class GrammarRule