public class TypeConversionRule extends GrammarRule
In Metamath terms, a Type Conversion can be derived from a $a
statement whose Formula has length equal to 2 and whose 2nd symbol has a
grammatical Type Code that differs from the 1st Symbol (the first symbol of
every Metamath Formula must be -- is always -- a Constant, and is, in effect
a "Type Code").
The most famous Metamath Type Conversion is "cv", from set.mm:
cv $a class x $.
, which states that every set is a class, that any
set variable or expression with Type "set" can be used as a replacement for
any class variable or expression with Type "class".)
Type Conversion Rules can also be derived from other Grammar Rules, including Type Conversion Rules and Notation Rules. Things get complicated very quickly, especially when Nulls Permitted Rules are involved.
An example:
$c NUMBER INTEGER POSITIVEINTEGER wff term = $.
$v x y i j m n$.
Nx $f NUMBER x $.
Ny $f NUMBER y $.
Ii $f INTEGER i $.
Ij $f INTEGER j $.
Pm $f POSITIVEINTEGER m $.
Pn $f POSITIVEINTEGER n $.
NullOkPOSITIVEINTEGER $a POSITIVEINTEGER $.
ConvINTEGER $a NUMBER i $.
ConvPOSITIVEINTEGER $a INTEGER m $.
TermAdd $a term m n $.
WffEquals $a wff x = y $.
OK, that very hypothetical example explicitly says that we have:
But we're not done yet, those are only the explicit Grammar Rules. A number of implicit -- derived -- Grammar Rules follow:
WHEW!
Part of mmj's grammar validation checks for Type Conversion loops, such as "a ISA b" + "b ISA c" + "c ISA a". It also rejects "a ISA a".
Implicit grammar rules are derived in mmj and made explicit, so if "a ISA b" and "z ISA a", then mmj will derive "z ISA b".
Since derived grammar rules may duplicate user-input Syntax Axioms (the "base" Grammar Rules), mmj reports as an error a user-input rule that duplicates a derived rule already in existence. This means that the user should move her rule towards the beginning of the .mm file to establish precedence.
In other words, mmj reports as an error any user-input grammar rules that have no effect, but silently ignores any newly derived rules that duplicate user-input rules (unless there is a Type Code conflict between the two!)
Modifier and Type | Field and Description |
---|---|
protected Cnst |
convTyp
convTyp is the "from" or source Typ Cd for The Type Conversion Rule,
which is converted "to" the Rule's Type Code.
|
isBaseRule, MAX_SEQ_NBR, maxSeqNbr, nbrHypParamsUsed, paramTransformationTree, paramVarHypNode, RULE_NBR, ruleFormatExpr, ruleHypPos, ruleNbr
Constructor and Description |
---|
TypeConversionRule()
Default constructor.
|
TypeConversionRule(Grammar grammar,
Axiom baseSyntaxAxiom,
Cnst convTyp)
Constructor -- default GrammarRule for base Syntax Axioms, which means no
parameter "transformations".
|
TypeConversionRule(Grammar grammar,
NotationRule oldNotationRule,
int matchIndex,
NullsPermittedRule nullsPermittedRule)
Builds a new TypeConversionRule using a Notation rule which is being
"cloned" and modified by substituting the paramTransformationTree from a
NullsPermittedRule for one of the existing rule's variable hypothesis
paramTransformationTree nodes.
|
TypeConversionRule(Grammar grammar,
TypeConversionRule oldTCRule,
int matchIndex,
TypeConversionRule typeConversionRule)
Builds a new TypeConversionRule using an existing TypeConversion rule
which is being "cloned" and and modified by substituting the
paramTransformationTree from another TypeConversionRule for one of the
existing rule's variable hypothesis paramTransformationTree nodes.
|
Modifier and Type | Method and Description |
---|---|
void |
addToGrammar(Grammar grammar,
Cnst[] ruleFormatExprIn)
Add Type Conversion rule format expression to the system "repository".
|
protected static TypeConversionRule |
buildBaseRule(Grammar grammar,
Axiom baseSyntaxAxiom,
ParseNodeHolder[] parseNodeHolderExpr)
Type Conversion 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.
|
protected void |
deriveRulesUsingNullsPermitted(Grammar grammar,
NullsPermittedRule nullsPermittedRule)
Generates a NullsPermittedRule *if* the input NullsPermittedRule Type
Code matches the Type Code of the TypeConversionRule's VarHyp.
|
protected void |
deriveRulesUsingTypeConversion(Grammar grammar,
TypeConversionRule typeConversionRule)
Generates a TypeConversionRule *if* the input TypeConversionRule Type
Code matches the Type Code of this TypeConversionRule's VarHyp.
|
Cnst |
getConvTyp()
Return convTyp, the "from" part of the Type conversion.
|
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 Type Conversion Rule by simulating
retrieving it from the Grammar Rule Tree/Forest.
|
static boolean |
isLoop(Cnst fromTyp,
Cnst toTyp)
isLoop determines whether or not a new Type Conversion from/to pair of
Type Codes create a "loop" -- meaning that "from" converts to "to" and
"to" converts to "from", directly or indirectly.
|
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 Cnst convTyp
Note that there is no need to store the "to" Type code here in the TypeConversionRule because it can easily be derived from the Type Code via GrammarRule.getBaseSyntaxAxiom().getTyp() AND from the root node's Stmt of GrammarRule.paramTransformationTree.
public TypeConversionRule()
public TypeConversionRule(Grammar grammar, Axiom baseSyntaxAxiom, Cnst convTyp)
grammar
- The Grammar.baseSyntaxAxiom
- Syntax Axiom.convTyp
- the "from" type code of this conversionpublic TypeConversionRule(Grammar grammar, NotationRule oldNotationRule, int matchIndex, NullsPermittedRule nullsPermittedRule)
(That sounds hairy :)
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.nullsPermittedRule
- the modifying rule.public TypeConversionRule(Grammar grammar, TypeConversionRule oldTCRule, int matchIndex, TypeConversionRule typeConversionRule)
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.oldTCRule
- rule being "cloned".matchIndex
- index to paramVarHypNode array indicating which VarHyp
is being substituted.typeConversionRule
- the modifying rule.protected static TypeConversionRule buildBaseRule(Grammar grammar, Axiom baseSyntaxAxiom, ParseNodeHolder[] parseNodeHolderExpr)
grammar
- The Grammar.baseSyntaxAxiom
- Syntax Axiom.parseNodeHolderExpr
- Expression in parseNodeHolder array.public static boolean isLoop(Cnst fromTyp, Cnst toTyp)
isLoop relies on Cnst.convFromTypGRArray already being fully populated with all "from" Type Codes for the subject Cnst, including direct conversions and all indirect conversions; this puts the onus on TypeConversionRule.deriveAdditionalRules to figure out the complicated stuff.
fromTyp
- the "from" converstion Type Code.toTyp
- the "to" converstion Type Code.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.protected void deriveRulesUsingNullsPermitted(Grammar grammar, NullsPermittedRule nullsPermittedRule)
Note: The form of a TypeConversionRule *expression* is exactly one variable whose Type Code differs from that of the rule's Type.
grammar
- The Grammar.nullsPermittedRule
- the modifying rule.protected void deriveRulesUsingTypeConversion(Grammar grammar, TypeConversionRule typeConversionRule)
Note: The form of a TypeConversionRule *expression* is exactly one variable whose Type Code differs from that of the rule's Type.
grammar
- The Grammar.typeConversionRule
- the modifying rule.public Cnst getConvTyp()
public Cnst[] getForestRuleExpr()
In reality, the ruleFormatExpr for a Type Conversion Rule is an length = 1 symbol sequence = convTyp.
getForestRuleExpr
in class GrammarRule