Interface | Description |
---|---|
GrammaticalParser |
GrammaticalParser is an interface established so that the Grammar class can
use different parsers (even though the choice of parser is presently
hard-coded into Grammar).
|
Class | Description |
---|---|
BottomUpParser |
Bottom Up Parser, too slow and stupid for set.mm use.
|
EarleyItem |
EarleyItem is a work item generated as part of the EarleyParse algorithm
representing partial or complete satisfaction of a grammar rule by a
subsequence of an expression being parsed.
|
EarleyParser |
EarleyParser is my implementation of the Earley Parse algorithm, enhanced
with Lookahead and various attempts at efficiency in Java.
|
Grammar |
Grammar processes a mmj LogicalSystem, extracts a Grammar, which it also
validates, and parses statements in the system.
|
GrammarAmbiguity |
GrammarAmbiguity was separated out from Grammar because a) Grammar was
already getting too long, and b) the topic of "ambiguity" is large and the
code will likely be a work-in-progress (until someone has a brainstorm).
|
GrammarConstants |
Constants used in Grammar-related classes.
|
GrammarConstants.LabelContext | |
GrammarRule |
GrammarRule is the superclass of NotationRule, NullsPermittedRule and
TypeConversionRule.
|
GRForest |
GRForest is a collection of static functions that operate on GRNode Trees.
|
GRNode |
see RBCell(dot)java by Doug Lea, public domain; clone that puppy, and added
Up/Down fields to create hierarchical forest of Grammar Rule Trees.
|
LRParser |
LR Parser
|
NotationRule |
Notation Grammar Rules are the main Grammar Rules used to arrange symbols
representing grammatical types, such as "wff" and "class".
|
NullsPermittedRule |
A Nulls Permitted Rule is a Grammar Rules that says that a certain type of
grammatical expression may be null, (may have zero-length symbol sequences).
|
ProofConstants |
Constants used in mmj.verify.VerifyProofs class.
|
ProofDerivationStepEntry |
Proof Derivation Step Entry is a simple data structure used to hold a
non-syntax axiom assertion proof step (i.e.
|
SubstMapEntry |
SubstMapEntry is a data structure used in an array in VerifyProofs for making
variable substitutions.
|
TypeConversionRule |
A Type Conversion Rule is a Grammar Rules that says that any grammatical
expression of a certain type may be substituted for any expression of another
grammatical Type.
|
VerifyProofs |
VerifyProofs implements the proof verification process described in
Metamath(dot)pdf.
|
Enum | Description |
---|---|
HypsOrder |
This enumeration is used to indicate the order of theorem hypotheses during
(mainly) loading or storing.
|
Exception | Description |
---|---|
VerifyException |
Thrown by package mmj.verify methods when a verification error is detected in
LogicalSystem.
|