public class GrammarConstants
extends java.lang.Object
There are two primary types of constants: parameters that are "hardcoded" which affect/control processing, and error/info messages.
Each mmj message begins with a code, such as this:
E-LA-0007
where the format of the code is X-YY-9999
X
: error level
E
= Error
I
= Information
A
= Abort (processing terminates, usually a bug).
YY
: source code
GM
= mmj.gmff package (see GMFFConstants
)
GR
= mmj.verify.Grammar and related code (see
GrammarConstants
)
IO
= mmj.mmio package (see MMIOConstants
)
LA
= mmj.lang package (see GMFFConstants
)
PA
= mmj.pa package (proof assistant) (see PaConstants
)
PR
= mmj.verify.VerifyProof and related code (see
ProofConstants
)
TL
= mmj.tl package (Theorem Loader).
TM
= mmj.tmff.AlignColumn and related code
UT
= mmj.util package. (see UtilConstants
)
TR
= mmj.transforms package (proof assistant) (see
TrConstants
)
9999
: sequential number within the source code, 0001 through
9999.
Modifier and Type | Class and Description |
---|---|
static class |
GrammarConstants.LabelContext |
Constructor and Description |
---|
GrammarConstants() |
public static final int PARSE_TREE_MAX_FOR_AMBIG_EDIT
Normally set at 2, but can be altered for testing to as many as desired (which will generate huge messages...)
public static final java.lang.String[] DEFAULT_PROVABLE_LOGIC_STMT_TYP_CODES
At this time only one Provable Logic Statement Type Code can be used for a Metamath system.
public static final java.lang.String[] DEFAULT_LOGIC_STMT_TYP_CODES
In the grammatical parse process a "Start Type Code" is identified for the expression being parsed, and this is the expected Type Code given the formula's Type Code. Generally speaking, if the Formula's Type is the Provable Logic Statement Type Code then the Start Type used is the corresponding Logical Statement Type Code; thus, the grammatical parse Start Type Code for a Formula with Type Code "|-" is "wff" -- and that means that the parse tree root Stmt's Type Code had better be "wff"!
At this time only one Logical Statement Type Code can be used for a Metamath system. There is a "loophole" however -- it is not prohibited for another Type Code to convert *to* a Logical Statement Type Code, so "wffa" could convert to "wff" (but "|-" can never be the Type of a variable and cannot convert to "wff").
public static final boolean DEFAULT_COMPLETE_GRAMMAR_AMBIG_EDITS
public static final boolean DEFAULT_COMPLETE_STATEMENT_AMBIG_EDITS
public static final int MAX_DERIVED_RULE_QUEUE_SIZE
Thus, this is not the maximum number of GrammarRules but a limit to the number waiting to be processed after being derived from one GrammarRule (a GrammarRule such as a TypeConversionRule or NullsPermittedRule can "trigger" other new GrammarRules). For this limit to be breached, something very unorthodox would need to be used, such as putting a key TypeConversion Syntax Axiom at the end of a huge list of other Syntax Axioms (set.mm has only about 500 GrammarRules in total).
public static final int MAX_PARSE_RETRIES
A retry involves re-allocating the arrays with a larger size and then repeating the parse from the start. BUT if the maximum number of retries is exceeded than there may be a bug in the code -- this is a fail-safe feature, in other words.
public static final int EARLEY_PARSE_MIN_ITEMSET_MAXIMUM
Used only if larger than the number of NotationRules. Established because of certain test files with very small numbers of NotationRules which ended up overflowing in the retry routine.
public static final int EARLEY_PARSE_CITEMSET_ITEMSET_RATIO
--> i.e. there are expected to be at most 1/2 as many Completed Items as there are Active/Predicted Items.
public static final int BOTTOM_UP_GOVERNOR_LIMIT
NOTE: BottomUpParser is not normally used but is retained in mmj for experimental purposes.
If BOTTOM_UP_GOVERNOR_LIMIT does not get the job done then the grammar is probably unsuitable for the BottomUp parse algorithm (for example, parsing "supeu" in set.mm with BottomUpParser has never been achieved -- it requires millions of loops, or thereabouts.)
public static final int BOTTOM_UP_GOVERNOR_LIMIT_MAX
Thus, the Ultra-Maximum number of loops through the BottomUpParser.java
algorithm is then set =
BOTTOM_UP_GOVERNOR_LIMIT
times the length of the expression being parsed
times BOTTOM_UP_GOVERNOR_LIMIT_MAX;
public static final int BOTTOM_UP_STACK_HARD_FAILURE_MAX
Since this equates to the maximum parse tree depth, it is a ridiculously high number for the BottomUpParser, especially since we are using a governor limit on the number of times through the main loop; in other words, this is a fail-safe, belt *and* suspenders and velcro.
public static final ErrorCode ERRMSG_MAX_RETRIES_EXCEEDED
public static final ErrorCode ERRMSG_RETRY_TO_BE_INITIATED
public static final ErrorCode ERRMSG_BU_GOVERNOR_LIMIT_EXCEEDED
public static final ErrorCode ERRMSG_BU_PARSE_STACK_OVERFLOW
public static final ErrorCode ERRMSG_EXPR_USES_TYP_AS_CNST
public static final ErrorCode ERRMSG_START_RULE_TYPE_UNDEF
public static final ErrorCode ERRMSG_EARLEY_ITEMSET_OVERFLOW
public static final ErrorCode ERRMSG_EARLEY_C_ITEMSET_OVERFLOW
public static final ErrorCode ERRMSG_FATAL_ARRAY_INDEX_ERROR
public static final ErrorCode ERRMSG_EARLEY_HYP_PARAMS_NOTFND
public static final ErrorCode ERRMSG_EARLEY_HYPMAP_PARAMS_NOTFND
public static final ErrorCode ERRMSG_RIGHT_TWEENER_ERROR
public static final ErrorCode ERRMSG_LEFT_TWEENER_ERROR
public static final ErrorCode ERRMSG_PARSE_FAILED_AT_POS
public static final ErrorCode ERRMSG_PARSE_FAILED
public static final ErrorCode ERRMSG_2_PARSE_TREES
public static final ErrorCode ERRMSG_GRAMMAR_RULE_PARSEABLE
public static final ErrorCode ERRMSG_GRAMMAR_RULE_2_PARSEABLE
public static final ErrorCode ERRMSG_PROVABLE_TYP_PARAM_INVALID
public static final ErrorCode ERRMSG_LOGIC_TYP_PARAM_INVALID
public static final ErrorCode ERRMSG_PROVABLE_TYP_CD_BOGUS
public static final ErrorCode ERRMSG_PROVABLE_TYP_DUPS
public static final ErrorCode ERRMSG_PROVABLE_DUP_OF_LOGICAL
public static final ErrorCode ERRMSG_LOGIC_TYP_CD_BOGUS
public static final ErrorCode ERRMSG_LOGIC_TYP_DUPS
public static final ErrorCode ERRMSG_PROVABLE_TYP_NOT_A_CNST
public static final ErrorCode ERRMSG_LOGIC_TYP_NOT_A_CNST
public static final ErrorCode ERRMSG_VARHYP_TYP_PROVABLE
public static final ErrorCode ERRMSG_DJ_VARS_ON_SYNTAX
public static final ErrorCode ERRMSG_LOGHYP_FOR_SYNTAX
public static final ErrorCode ERRMSG_SYNTAX_VARHYP_MISMATCH
public static final ErrorCode ERRMSG_SYNTAX_VAR_GT_1_OCC
public static final ErrorCode ERRMSG_SYNTAX_USES_TYP_AS_CNST
public static final ErrorCode ERRMSG_GRFOREST_EXPR_LENGTH_ZERO
public static final ErrorCode ERRMSG_GRFOREST_RULE_NULL
public static final ErrorCode ERRMSG_GRFOREST_RULE_DUP
public static final ErrorCode ERRMSG_GRFOREST_NODE_LOST
public static final ErrorCode ERRMSG_TYPCONV_VARHYP_NOTFND
public static final ErrorCode ERRMSG_TYPCONV_2_VARHYP_NOTFND
public static final ErrorCode ERRMSG_TYPCONV_AXIOM_LOOP
public static final ErrorCode ERRMSG_TYPCONV_NBRHYP_NE_1
public static final java.lang.String ERRMSG_AT_CAPTION
public static final java.lang.String ERRMSG_DOT_CAPTION
public static final java.lang.String ERRMSG_AFTER_DOT_CAPTION
public static final java.lang.String ERRMSG_COLON_CAPTION
public static final java.lang.String ERRMSG_RULE_EXPR_CAPTION
public static final ErrorCode ERRMSG_BASE_RULE_IS_DUP
public static final ErrorCode ERRMSG_DUP_RULE_DIFF_TYP
public static final ErrorCode ERRMSG_BOGUS_PARAM_VARHYP_NODE
public static final ErrorCode ERRMSG_UNDEF_NON_TERMINAL
public static final ErrorCode ERRMSG_GRAMMAR_UNAMBIGUOUS
public static final ErrorCode ERRMSG_NOTATION_VARHYP_NOTFND
public static final ErrorCode ERRMSG_NOTATION_GRFOREST_DUP
public static final ErrorCode ERRMSG_N_PARSE_TREES
public static final java.lang.String ERRMSG_N_PARSE_TREES_2
public static final ErrorCode ERRMSG_REDUCE_REDUCE
public static final java.lang.Class<? extends GrammaticalParser> DEFAULT_PARSER_PROTOTYPE