public class LogicalSystem extends java.lang.Object implements SystemLoader
LogicalSystem
, along with the rest of the mmj.lang
package, implements the abstract portion of the Metamath language -- the
"object" language of Metamath, as opposed to the "metalanguage" of Metamath
source files. For example, note that LogicalSystem.java
does not care
which characters are used in Constant, Variable and Label strings. The
characters are represented internally in Unicode, not the 7-bit ASCII
employed in Metamath (.mm) source files. Nevertheless, the logical rules
concerning Constant, Variable and Label namespaces are enforced
rigorously :) As much as possible, the concerns of source files are delegated
to the mmj.mmio
package and its highest level class,
Systemizer.java
, which uses LogicalSystem.java
to create a
Metamath logical system in memory. Once Systemizer.java
has input a
set of Metamath statements into a LogicalSystem.java
object, the
Logical System can be processed independently of all mmj.mmio
code.
In fact, a GUI system need not use mmj.mmio
or
Systemizer.java
at all (however it should be noted that none of this
code is "thread aware" as of now...)Modifier and Type | Field and Description |
---|---|
BookManager |
bookManager |
GMFFManager |
gmffManager |
java.lang.String |
logicStmtTypeParm |
java.lang.String |
provableLogicStmtTypeParm |
SeqAssigner |
seqAssigner |
Constructor and Description |
---|
LogicalSystem(java.lang.String provableLogicStmtTypeParm,
java.lang.String logicStmtTypeParm,
GMFFManager gmffManager,
BookManager bookManager,
SeqAssigner seqAssigner,
int symTblInitialSize,
int stmtTblInitialSize,
ProofVerifier proofVerifier,
SyntaxVerifier syntaxVerifier)
Construct with full set of parameters.
|
Modifier and Type | Method and Description |
---|---|
void |
accumTheoremLoaderCommitListener(TheoremLoaderCommitListener t)
Adds a TheoremLoaderCommitListener to the TheoremLoaderCommitListener
list if the instance is not already in the list.
|
Axiom |
addAxiom(java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Add Axiom to Logical System.
|
Cnst |
addCnst(java.lang.String id)
Add Cnst to Logical System.
|
DjVars |
addDjVars(java.lang.String djVar1S,
java.lang.String djVar2S)
Add DjVars (Disjoint Variables Restriction) to Logical System.
|
LogHyp |
addLogHyp(java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Add LogHyp (Logical Hypothesis) to Logical System.
|
LogHyp |
addLogHypForTheoremLoader(int seq,
java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList)
Add LogHyp (Logical Hypothesis) to Logical System.
|
void |
addNewChapter(java.lang.String chapterTitle)
Add new BookManager Chapter.
|
void |
addNewSection(java.lang.String sectionTitle)
Add new BookManager Section.
|
Theorem |
addTheorem(java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
BlockList proofBlockList,
Messages messages)
Add Theorem to Logical System.
|
Theorem |
addTheorem(java.lang.String labelS,
int column,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList,
Messages messages)
Add Theorem to Logical System.
|
Theorem |
addTheoremForTheoremLoader(int seq,
java.lang.String labelS,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<java.lang.String> proofList)
Add Theorem to Logical System for TheoremLoader.
|
Var |
addVar(java.lang.String id)
Add Var to Logical System.
|
VarHyp |
addVarHyp(java.lang.String labelS,
java.lang.String typS,
java.lang.String varS)
Add VarHyp to Logical System.
|
void |
beginScope()
Begin a new (nested) scope level for the Logical System.
|
void |
cacheTypesettingCommentForGMFF(java.lang.String comment)
Cache Metamath comment containing typesetting definitions for use by
GMFF.
|
void |
clearTheoremLoaderCommitListenerList()
Empties the TheoremLoaderCommitListener list.
|
void |
endScope()
Ends a (nested) scope level for the Logical System.
|
void |
finalizeEOF(Messages messages,
boolean prematureEOF)
EOF processing for Logical System after file loaded.
|
ScopeDef |
getCurrScopeDef()
Get current ScopeDef object in use.
|
GMFFManager |
getGMFFManager()
Returns the GMFF Manager.
|
java.lang.String |
getLogicStmtTypeParm()
Returns the logic stmt type code string value.
|
ProofCompression |
getProofCompression()
Returns an instance of ProofCompression.
|
ProofVerifier |
getProofVerifier() |
java.lang.String |
getProvableLogicStmtTypeParm()
Returns the provable logic stmt type code string value.
|
java.util.List<ScopeDef> |
getScopeDefList()
Get LogicalSystem scopeDefList
|
int |
getScopeLvl()
Get current scope level.
|
java.util.Map<java.lang.String,Stmt> |
getStmtTbl()
Returns the current stmtTbl, a Map containing all
Hyp s and
Assrt s. |
java.util.Map<java.lang.String,Sym> |
getSymTbl()
Returns the current symTbl, a Map containing all
Cnst s and
Var s. |
SyntaxVerifier |
getSyntaxVerifier() |
boolean |
isBookManagerEnabled()
Is BookManager enabled?
|
void |
removeTheoremLoaderCommitListener(TheoremLoaderCommitListener t)
Removes a TheoremLoaderCommitListener from the
TheoremLoaderCommitListener list if the instance is in the list.
|
void |
setProofCompression(ProofCompression proofCompression)
Sets the reference to the local ProofCompression instance.
|
ProofVerifier |
setProofVerifier(ProofVerifier newProofVerifier)
Sets the current ProofVerifier.
|
SyntaxVerifier |
setSyntaxVerifier(SyntaxVerifier newSyntaxVerifier)
Sets the current SyntaxVerifier.
|
void |
theoremLoaderCommit(MMTTheoremSet mmtTheoremSet)
Finalizes any changes made to the mmj2 state by TheoremLoader for a
mmtTheoremSet set of updates.
|
void |
theoremLoaderRollback(MMTTheoremSet mmtTheoremSet,
MMJException error,
Messages messages,
boolean auditMessages)
Reverses any changes made to the mmj2 state by TheoremLoader for a
mmtTheoremSet set of updates.
|
void |
verifyAllExprRPNAsProofs(Messages messages)
Double-checks the results of
verifyAllSyntax by feeding the
output exprRPN 's through the ProofVerifier. |
void |
verifyAllSyntax(Messages messages)
Does Syntactical Analysis of the grammar and all statements in the
LogicalSystem.
|
void |
verifyProofs(Messages messages)
Verifies every theorem's proof according to Metamath.pdf specifications.
|
public final java.lang.String provableLogicStmtTypeParm
public final java.lang.String logicStmtTypeParm
public final BookManager bookManager
public final GMFFManager gmffManager
public final SeqAssigner seqAssigner
public LogicalSystem(java.lang.String provableLogicStmtTypeParm, java.lang.String logicStmtTypeParm, GMFFManager gmffManager, BookManager bookManager, SeqAssigner seqAssigner, int symTblInitialSize, int stmtTblInitialSize, ProofVerifier proofVerifier, SyntaxVerifier syntaxVerifier)
provableLogicStmtTypeParm
- Type Code String of provable statements.
Defaults to "|-".logicStmtTypeParm
- Type Code String value of logic expressions.
Defaults to "wff".gmffManager
- used for Graphics Mode Formula Formatting in Proof
Assistant but loaded with $t typesetting info by Systemizer.bookManager
- optional, used for tracking MObjs by Chapter and
Section number.seqAssigner
- used to generate sequence numbers for MObjssymTblInitialSize
- should equal number of constant and variables,
times 1.33 plus a fudge factor. If set too small the system
will automatically increase, but at the expense of
reallocating and copying. BUT, if the input value is less than
10, the program assumes a programming error exists and throws
an IllegalArgumentException. A suggested default value is
provided in LangConstants.java.stmtTblInitialSize
- should equal number of variable and logical
hypotheses plus the number of axioms and theorems, times 1.33
plus a fudge factor. If set too small the system will
automatically increase, but at the expense of reallocating and
copying. BUT, if the input value is less than 100, the program
assumes a programming error exists and throws an
IllegalArgumentException. A suggested default value is
provided in LangConstants.java.proofVerifier
- ProofVerifier interface object. Leave null if
automatic proof verification not desired.syntaxVerifier
- SyntaxVerifier interface object. Leave null if
automatic loading of ExprRPN's is not desired.public Cnst addCnst(java.lang.String id) throws LangException
1) validates constant:
2)adds to symTbl table
3)return the constant object that now exists in the symbol table (this is done for consistency with the other addXXX methods -- we want everyone to use the only objects that exist in LogicalSystem... otherwise, CHAOS would occur!
addCnst
in interface SystemLoader
id
- Constant's symbol string to be added to the Logical System.LangException
- if duplicate symbol, etc.public Var addVar(java.lang.String id) throws LangException
1) validates variable:
2) add to symTbl table; if already there but inactive, mark it active.
3) get current ScopeDef array list item, (if any) and add the new var to the scope array list of Var's.
4) return the variable object that now exists in the symbol table (a key step so that everyone is using the same object!!!)
addVar
in interface SystemLoader
id
- Var's symbol string to be added to the Logical System.LangException
- if duplicate symbol, etc.public VarHyp addVarHyp(java.lang.String labelS, java.lang.String typS, java.lang.String varS) throws LangException
1)Validates VarHyp label:
2)Validates VarHyp typ and var:
3)Manufacture an active VarHyp, complete with sequence number
4)Add the new variable hypothesis to the statement table.
5) get current ScopeDef array list item, (if any) and add the new VarHyp to the scope array list of VarHyp's
6) return the VarHyp object that now exists in the statement table.
addVarHyp
in interface SystemLoader
labelS
- String label of variable hypothesistypS
- String Metamath constant character (type code)varS
- String Metamath variable characterLangException
- if duplicate symbol, etc. (see
mmj.lang.LangConstants.java
)public DjVars addDjVars(java.lang.String djVar1S, java.lang.String djVar2S) throws LangException
1) validates disjoint variables:
2) construct DjVars element (swapping the items if necessary to ensure varLo < varHi.--see constructor).
3) get current ScopeDef array list item
4) add the DjVars elment to the scope list of DjVars, but only if the pair of variables is not already there (we cannot use "==" in this case because DjVars are not maintained as "unique" in the same way as Sym's and Stmt's.)
addDjVars
in interface SystemLoader
djVar1S
- disjoint variable symbol string 1djVar2S
- disjoint variable symbol string 2LangException
- if duplicate vars, etc. (see
mmj.lang.LangConstants.java
)public LogHyp addLogHyp(java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws LangException
Basically a clone of addAxiom
below, except that:
LogHyp is a Hyp
, not an Assrt
and has attribute
"VarHyp[] varHypArray
.
Required processing:
1) validates input label, type and expression symbols, and in the process obtaining references to their existing definitions in LogicalSystem:
2) construct the LogHyp object
3) add it to the stmtTbl and to the existing scope.
4) return it to the caller
addLogHyp
in interface SystemLoader
labelS
- logical hypothesis label stringtypS
- logical hypothesis type code (symbol) stringsymList
- list containing expression symbol strings (zero or more
symbols).LangException
- if duplicate label, undefined vars, etc.public LogHyp addLogHypForTheoremLoader(int seq, java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws LangException
The main difference from the regular addLogHyp is that the BookManager is not called.
seq
- preassigned MObj seq numberlabelS
- logical hypothesis label stringtypS
- logical hypothesis type code (symbol) stringsymList
- list containing expression symbol strings (zero or more
symbols).LangException
- if duplicate label, undefined vars, etc.public Axiom addAxiom(java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList) throws LangException
1) validates input label, type and expression symbols, and in the process obtaining references to their existing definitions in LogicalSystem:
2) Build the MetaMath "Frame" for the Axiom (see ScopeFrame)
3) construct the Axiom object
4) add it to the stmtTbl
5) return it to the caller
addAxiom
in interface SystemLoader
labelS
- axiom label stringtypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).LangException
- if duplicate label, undefined vars, etc.public Theorem addTheorem(java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, Messages messages) throws LangException
addTheorem is basically a clone of addAxiom except that it builds an "extended" Frame containing "optional" hypotheses and disjoint variable restriction information. And it validates the input proof list then stores it with the new Theorem object.
1) validates input label, type and expression symbols, and in the process obtaining references to their existing definitions in LogicalSystem:
2) Build the MetaMath Extended Frame for the Theorem (consists here in mmj of MandFrame + OptFrame).
3) Validates proof steps
4) Construct Theorem object
5) add it to the stmtTbl
6) return it to the caller
addTheorem
in interface SystemLoader
labelS
- axiom label stringcolumn
- the column at which the "$p" line startstypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).proofList
- list containing proof step symbol strings (1 or more
symbols -- which may be "?" if a step is unknown).messages
- for error reportingLangException
- if duplicate label, undefined vars, etc.public Theorem addTheoremForTheoremLoader(int seq, java.lang.String labelS, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList) throws LangException
Main difference of regular addTheorem is that it does not call BookManager.
seq
- preassigned MObj seq numberlabelS
- axiom label stringtypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).proofList
- list containing proof step symbol strings (1 or more
symbols -- which may be "?" if a step is unknown).LangException
- if duplicate label, undefined vars, etc.public Theorem addTheorem(java.lang.String labelS, int column, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<java.lang.String> proofList, BlockList proofBlockList, Messages messages) throws LangException
addTheorem is basically a clone of addAxiom except that it builds an "extended" Frame containing "optional" hypotheses and disjoint variable restriction information. And it validates the input proof list then stores it with the new Theorem object.
This variant is invoked when the input contains a compressed proof.
addTheorem
in interface SystemLoader
labelS
- axiom label stringcolumn
- the column at which the "$p" line startstypS
- axiom type code (symbol) stringsymList
- list containing axiom expression symbol strings (zero or
more symbols).proofList
- list containing the contents of the parenthesized
portion of a compressed proof (does not include the
parentheses)proofBlockList
- list containing one or more blocks of compressed
proof symbols.messages
- for error reportingLangException
- if duplicate label, undefined vars, etc.public void beginScope()
Adds a new ScopeDef item to the "stack" and increments the level number by 1 (all of the hard work is in endScope()!)
Note: *global* scope has level number = 0.
beginScope
in interface SystemLoader
ScopeDef
public void endScope() throws LangException
Processing:
1) if scope level = 0 (global), raise LangException.
otherwise,
2)
endScope
in interface SystemLoader
LangException
- if scope is already at the global scope level.ScopeDef
public void finalizeEOF(Messages messages, boolean prematureEOF) throws LangException
Called at end of file to verify that there was an End Scope statement for each Begin Scope. At the time this routine is called, the ScopeDef list should contain just one entry, the "global" scope level (which is, by definition, level 0.)
finalizeEOF
in interface SystemLoader
messages
- Messages object to error reporting.prematureEOF
- signals LoadLimit requested by user has been reached,
so stop loading even if in the middle of a scope level.LangException
- if scope is NOT at the global scope level UNLESS
premature EOF signalled. (see
mmj.lang.LangConstants.java
)public void verifyAllSyntax(Messages messages) throws VerifyException
messages
- Messages
object for reporting errors.VerifyException
- if an error occurredpublic void verifyProofs(Messages messages) throws VerifyException
messages
- Messages
object for reporting errors.VerifyException
- if an error occurredpublic void verifyAllExprRPNAsProofs(Messages messages) throws VerifyException
verifyAllSyntax
by feeding the
output exprRPN
's through the ProofVerifier.
Based on the fact that the output of the grammatical parser is a *proof* that a statement's formula can be generated using the grammatical parse tree -- which is stored in LogicalSystem in Reverse Polish Notation, like proofs.
Should not be necessary in normal use, but is very helpful for testing.
messages
- Messages
object for reporting errors.VerifyException
- if an error occurredpublic java.util.List<ScopeDef> getScopeDefList()
scopeDefList is an List of ScopeDef objects where element 0 is global scope, element 1 is scope level 1, etc. At the end of LoadFile the scopeDefList should contain only 1 element -- the global ScopeDef.
public ScopeDef getCurrScopeDef()
public int getScopeLvl()
Level 0 is global scope, 1 is level 1, etc.
public ProofVerifier getProofVerifier()
public ProofVerifier setProofVerifier(ProofVerifier newProofVerifier)
newProofVerifier
- a ProofVerifier or null is ok.public SyntaxVerifier getSyntaxVerifier()
public SyntaxVerifier setSyntaxVerifier(SyntaxVerifier newSyntaxVerifier)
newSyntaxVerifier
- a SyntaxVerifier or null is ok.public java.util.Map<java.lang.String,Sym> getSymTbl()
Cnst
s and
Var
s.
Note: in theory, symTbl is an excellent candidate for being a real class. There are numerous operations involving it, and more possibilities.
Cnst
s and Var
s.public java.util.Map<java.lang.String,Stmt> getStmtTbl()
Hyp
s and
Assrt
s.
Note: in theory, stmtTbl is an excellent candidate for being a real class. There are numerous operations involving it, and more possibilities.
Hyp
s and Assrt
s.public ProofCompression getProofCompression()
Reuses the existing ProofCompression instance if present, otherwise constructs one.
public void setProofCompression(ProofCompression proofCompression)
proofCompression
- instance or null.public java.lang.String getProvableLogicStmtTypeParm()
(Default value is "|-", fyi.)
public java.lang.String getLogicStmtTypeParm()
(Default value is "wff", fyi.)
public GMFFManager getGMFFManager()
public void cacheTypesettingCommentForGMFF(java.lang.String comment)
Note: comment is from mmj.mmio.SrcStmt so it does not contain the "$(" and "$)" start/end comment id tokens which are standard to Metamath comments.
Note: per agreement with Norm, the "$t" token identifying typesetting definitions in a comment is the first non-whitespace token after the "$(" in the comment.
cacheTypesettingCommentForGMFF
in interface SystemLoader
comment
- Typesetting definition comment ("$t) from Metamath file
minus the "$(" and "$)" tokens.public void addNewChapter(java.lang.String chapterTitle)
See mmj.lang.BookManager.java for more info.
addNewChapter
in interface SystemLoader
chapterTitle
- Title of chapter or blank or empty String.public void addNewSection(java.lang.String sectionTitle)
See mmj.lang.BookManager.java for more info.
addNewSection
in interface SystemLoader
sectionTitle
- Title of section or blank or empty String.public boolean isBookManagerEnabled()
If BookManager is enabled then Chapters and Sections will be stored.
isBookManagerEnabled
in interface SystemLoader
public void clearTheoremLoaderCommitListenerList()
public void accumTheoremLoaderCommitListener(TheoremLoaderCommitListener t)
t
- TheoremLoaderCommitListener object.public void removeTheoremLoaderCommitListener(TheoremLoaderCommitListener t)
t
- TheoremLoaderCommitListener object.public void theoremLoaderRollback(MMTTheoremSet mmtTheoremSet, MMJException error, Messages messages, boolean auditMessages) throws TheoremLoaderException
Reverses any changes to the LogicalSystem scopeDefList.
Rollsback any changes to the SeqAssigner.
Scans the mmtTheoremSet and un-does each TheoremStmtGroup object's updates, if any,
mmtTheoremSet
- set of MMTTheoremStmtGroups which may or may not
have already been updated into mmj2.error
- an explanatory message about the cause of the rollback to be
inserted into a final message if the rollback itself fails.messages
- Messages object.auditMessages
- flag indicating whether or not audit messages about
the rollback are to be written to the Messages object.TheoremLoaderException
- with the rollback infopublic void theoremLoaderCommit(MMTTheoremSet mmtTheoremSet)
Commits SeqAssigner updates.
Commits BookManager updates.
Sends commit() request to every TheoremLoaderCommitListener.
mmtTheoremSet
- set of MMTTheoremStmtGroups which may or may not
have already been updated into mmj2.java.lang.IllegalArgumentException
- if the commit operation fails.