public class ProofAsst extends java.lang.Object implements TheoremLoaderCommitListener
ProofAsst
, along with the rest of the mmj.pa
package
provides a graphical user interface (GUI) facility for developing Metamath
proofs. ProofAsst
is the go-to guy, essentially a control module that
knows where to go to get things done. It is invoked by
mmj.util.ProofAsstBoss.java, and invokes mmj.pa.ProofAsstGUI, among others.
Nomenclature: a proof-in-progress is implemented by the
mmj.pa.ProofWorksheet.java class. A large quantity of information and useful
stuff is contained in mmj.pa.PaConstants.java.Modifier and Type | Field and Description |
---|---|
MacroManager |
macroManager |
ProofUnifier |
proofUnifier |
Constructor and Description |
---|
ProofAsst(ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
VerifyProofs verifyProofs,
TheoremLoader theoremLoader,
MacroManager macroManager)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
void |
commit(MMTTheoremSet mmtTheoremSet)
Applies a set of updates from the TheoremLoader as specified in the
mmtTheoremSet object to the ProofAsst local caches of data.
|
void |
doGUI(Messages m)
Triggers the Proof Assistant GUI.
|
java.lang.String |
exportOneTheorem(java.lang.String theoremLabel) |
java.lang.String |
exportOneTheorem(Theorem theorem) |
void |
exportToFile(java.io.Writer exportWriter,
Messages messages,
int numberToExport,
Theorem selectorTheorem,
OutputBoss outputBoss)
Export Theorem proofs to a given Writer.
|
Messages |
exportViaGMFF(java.lang.String proofText)
Invokes GMFF to export the current Proof Worksheet.
|
Messages |
extractTheoremToMMTFolder(Theorem theorem)
Invokes TheoremLoader to extract a theorem to the MMT Folder.
|
ProofWorksheet |
getExistingProof(Theorem oldTheorem,
boolean exportFormatUnified,
HypsOrder hypsOrder)
Builds ProofWorksheet for an existing theorem.
|
Grammar |
getGrammar() |
boolean |
getInitializedOK() |
LogicalSystem |
getLogicalSystem() |
Messages |
getMessages() |
ProofWorksheet |
getNextProof(int currProofMaxSeq,
boolean exportFormatUnified,
HypsOrder hypsOrder)
Builds ProofWorksheet for the next theorem after a given MObj sequence
number.
|
ProofAsstPreferences |
getPreferences() |
ProofWorksheet |
getPreviousProof(int currProofMaxSeq,
boolean exportFormatUnified,
HypsOrder hypsOrder)
Builds ProofWorksheet for the first theorem before a given MObj sequence
number.
|
ProofAsstGUI |
getProofAsstGUI() |
java.util.List<Assrt> |
getSortedAssrtSearchList() |
java.lang.Iterable<Theorem> |
getSortedSkipSeqTheoremIterable(java.lang.String startTheoremLabel) |
Stmt |
getStmt(java.lang.String s) |
Theorem |
getTheorem(java.lang.String theoremLabel)
Fetches a Theorem using an input Label String.
|
VerifyProofs |
getVerifyProofs() |
void |
importFromFileAndUnify(java.io.Reader importReader,
Messages messages,
int numberToProcess,
Theorem selectorTheorem,
OutputBoss outputBoss,
boolean asciiRetest)
Import Theorem proofs from a given Reader.
|
void |
importFromMemoryAndUnify(Messages messages,
int selectorCount,
Theorem selectorTheorem,
OutputBoss outputBoss,
boolean asciiRetest)
Import Theorem proofs from memory and unifies.
|
void |
importFromMemoryAndUnifyManyTheorems(int selectorCount,
OutputBoss outputBoss,
boolean asciiRetest)
Import Theorem proofs from memory and unifies.
|
void |
importFromMemoryAndUnifyOneTheorem(Theorem selectorTheorem,
OutputBoss outputBoss,
boolean asciiRetest)
Imports one theorem proof from memory and unifies.
|
void |
initAutotransformations(boolean enabled,
boolean debugOutput,
boolean supportPrefix)
This function initialize auto-transformation component.
|
boolean |
initializeLookupTables(Messages messages)
Initialized Unification lookup tables, etc.
|
Messages |
loadTheoremsFromMMTFolder()
Invokes TheoremLoader to load all theorems in the MMT Folder.
|
void |
optimizeTheoremSearch()
Perform the optimizations for theorem search during "parallel"
unification
|
void |
preprocessRequestBatchTest(java.lang.String proofText,
Messages messages,
OutputBoss outputBoss,
PreprocessRequest preprocessRequest)
Exercises the PreprocessRequest code for one proof.
|
java.util.List<Assrt> |
sortAssrtListForSearch(java.util.List<Assrt> list) |
ProofWorksheet |
startNewNextProof(int currProofMaxSeq)
Builds new ProofWorksheet for the next theorem after the current theorem
sequence number on the ProofAsstGUI.
|
ProofWorksheet |
startNewProof(java.lang.String newTheoremLabel)
Builds new ProofWorksheet for a theorem.
|
void |
stepSelectorBatchTest(java.io.Reader importReader,
Messages messages,
OutputBoss outputBoss,
int cursorPos,
int selectionNumber)
Exercises the StepSelectorSearch for one proof.
|
ProofWorksheet |
tmffReformat(boolean inputCursorStep,
java.lang.String proofText,
int inputCursorPos)
Reformats a ProofWorksheet using TMFF.
|
ProofWorksheet |
unify(boolean renumReq,
boolean noConvertWV,
java.lang.String proofText,
PreprocessRequest preprocessRequest,
StepRequest stepRequest,
TLRequest tlRequest,
int inputCursorPos,
boolean printOkMessages)
Attempts Unification for a proof contained in a String proof text area.
|
Messages |
verifyAllProofs()
Verifies all proofs in the Logical System
|
public final ProofUnifier proofUnifier
public final MacroManager macroManager
public ProofAsst(ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, VerifyProofs verifyProofs, TheoremLoader theoremLoader, MacroManager macroManager)
proofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectverifyProofs
- the mmj.verify.VerifyProofs objecttheoremLoader
- the mmj.tl.TheoremLoader objectmacroManager
- the mmj.pa.MacroManager objectpublic void doGUI(Messages m)
m
- the mmj.lang.Messages object used to store error and
informational messages.public boolean getInitializedOK()
public LogicalSystem getLogicalSystem()
public Messages getMessages()
public ProofAsstGUI getProofAsstGUI()
public ProofAsstPreferences getPreferences()
public Grammar getGrammar()
public VerifyProofs getVerifyProofs()
public java.util.List<Assrt> sortAssrtListForSearch(java.util.List<Assrt> list)
public boolean initializeLookupTables(Messages messages)
messages
- the mmj.lang.Messages object used to store error and
informational messages.public java.util.List<Assrt> getSortedAssrtSearchList()
public void commit(MMTTheoremSet mmtTheoremSet)
commit
in interface TheoremLoaderCommitListener
mmtTheoremSet
- MMTTheoremSet object containing the adds and updates
already made to theorems in the LogicalSystem.public Messages verifyAllProofs()
This is here because the Proof Assistant GUI doesn't know how to do anything...
public Messages loadTheoremsFromMMTFolder()
This is here because the Proof Assistant GUI doesn't know how to do anything...
public Messages exportViaGMFF(java.lang.String proofText)
proofText
- Proof Worksheet text string.public Messages extractTheoremToMMTFolder(Theorem theorem)
This is here because the Proof Assistant GUI doesn't know how to do anything...
theorem
- the theorem to extractpublic ProofWorksheet startNewProof(java.lang.String newTheoremLabel)
Note: this method is called by ProofAsstGUI.java!
Note that the output ProofWorksheet is skeletal and is destined for a straight-shot, output to the GUI screen. The ProofAsst and its components retain no memory of a ProofWorksheet between screen actions. Each time the user requests a new action the text is scraped off the screen and built into a new ProofWorksheet object!
Notice also that this function just invokes a ProofWorksheet constructor. Why? Because the ProofAsstGUI.java program has no access to or knowledge of LogicalSystem, Grammar, etc. The only external knowledge it has is ProofAsstPreferences.
newTheoremLabel
- the name of the new proofpublic ProofWorksheet startNewNextProof(int currProofMaxSeq)
Note: this method is called by ProofAsstGUI.java!
This function is provided for students who wish to work their way through Metamath databases such as set.mm and prove each theorem. It is like Forward-GetProof except that it returns a skeletal Proof Worksheet, and thus helps the student by not revealing the contents of the existing proof in the Metamath database.
Note that the output ProofWorksheet is skeletal and is destined for a straight-shot, output to the GUI screen. The ProofAsst and its components retain no memory of a ProofWorksheet between screen actions. Each time the user requests a new action the text is scraped off the screen and built into a new ProofWorksheet object!
Notice also that this function just invokes a ProofWorksheet constructor. Why? Because the ProofAsstGUI.java program has no access to or knowledge of LogicalSystem, Grammar, etc. The only external knowledge it has is ProofAsstPreferences.
currProofMaxSeq
- sequence number of current proof on ProofAsstGUI
screen.public Theorem getTheorem(java.lang.String theoremLabel)
Note: this method is called by ProofAsstGUI.java!
theoremLabel
- label of Theorem to retrieve from statement table.public Stmt getStmt(java.lang.String s)
public ProofWorksheet getExistingProof(Theorem oldTheorem, boolean exportFormatUnified, HypsOrder hypsOrder)
Note: this method is called by ProofAsstGUI.java!
oldTheorem
- theorem to getexportFormatUnified
- true means include step Ref labelshypsOrder
- the order of step Hypspublic ProofWorksheet getNextProof(int currProofMaxSeq, boolean exportFormatUnified, HypsOrder hypsOrder)
The search wraps to the start if the end is reached.
Note: The search list excludes any Theorems excluded by the user from Proof Unification (see RunParm ProofAsstUnifySearchExclude). The exclusion is made for technical reasons (expediency) -- if you don't like it a whole lot we can change it.
Note: this method is called by ProofAsstGUI.java!
currProofMaxSeq
- sequence number of ProofWorksheet from
ProofAsstGUI currProofMaxSeq field.exportFormatUnified
- true means include step Ref labelshypsOrder
- the order of step Hypspublic ProofWorksheet getPreviousProof(int currProofMaxSeq, boolean exportFormatUnified, HypsOrder hypsOrder)
The search wraps to the end if the start is reached.
Note: The search list excludes any Theorems excluded by the user from Proof Unification (see RunParm ProofAsstUnifySearchExclude). The exclusion is made for technical reasons (expediency) -- if you don't like it a whole lot we can change it.
Note: this method is called by ProofAsstGUI.java!
currProofMaxSeq
- sequence number of ProofWorksheet from
ProofAsstGUI currProofMaxSeq field.exportFormatUnified
- true means include step Ref labelshypsOrder
- the order of step Hypspublic ProofWorksheet unify(boolean renumReq, boolean noConvertWV, java.lang.String proofText, PreprocessRequest preprocessRequest, StepRequest stepRequest, TLRequest tlRequest, int inputCursorPos, boolean printOkMessages)
Note: this method is called by ProofAsstGUI.java!
The ProofWorksheetParser class is used to parse the input proof text. The reason for using this intermediary is that the system is designed to be able to read a file of proof texts (which is a feature designed for testing purposes, but still available to a user via the BatchMMJ2 facility.)
proofText
- proof text from ProofAsstGUI screen, or any String
conforming to the formatting rules of ProofAsst.renumReq
- renumbering of proof steps requestednoConvertWV
- true if we should not replace work vars with dummy
vars in derivation stepspreprocessRequest
- if not null specifies an editing operation to be
applied to the proof text before other processing.inputCursorPos
- caret offset plus one of input or -1 if caret pos
unavailable to caller.stepRequest
- may be null, or StepSelector Search or Choice request
and will be loaded into the ProofWorksheet.tlRequest
- may be null or a TLRequest.printOkMessages
- whether we could print any messages except errors?public ProofWorksheet tmffReformat(boolean inputCursorStep, java.lang.String proofText, int inputCursorPos)
Note: this method is called by ProofAsstGUI.java!
Reformatting is not attempted if the ProofWorksheet has structural errors (returned from the parser).
inputCursorStep
- set to true to reformat just the proof step
underneath the cursor.proofText
- proof text from ProofAsstGUI screen, or any String
conforming to the formatting rules of ProofAsst.inputCursorPos
- caret offset plus one of input or -1 if caret pos
unavailable to caller.public void importFromMemoryAndUnify(Messages messages, int selectorCount, Theorem selectorTheorem, OutputBoss outputBoss, boolean asciiRetest)
This is a simulation routine for testing purposes.
messages
- Messages object for output messages.selectorCount
- use to restrict the number of theorems present.selectorTheorem
- just process one theorem, ignore selectorCount.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.asciiRetest
- instructs program to re-unify the output Proof
Worksheet text after unification.public void importFromMemoryAndUnifyOneTheorem(Theorem selectorTheorem, OutputBoss outputBoss, boolean asciiRetest)
This is a simulation routine for testing purposes.
selectorTheorem
- process selected theorem.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.asciiRetest
- instructs program to re-unify the output Proof
Worksheet text after unification.public void importFromMemoryAndUnifyManyTheorems(int selectorCount, OutputBoss outputBoss, boolean asciiRetest)
This is a simulation routine for testing purposes.
selectorCount
- use to restrict the number of theorems present.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.asciiRetest
- instructs program to re-unify the output Proof
Worksheet text after unification.public void optimizeTheoremSearch()
public void initAutotransformations(boolean enabled, boolean debugOutput, boolean supportPrefix)
enabled
- Set to false to de-initialize an already loaded
transformation managerdebugOutput
- when it is true auto-transformation component will
produce a lot of debug outputsupportPrefix
- when it is true auto-transformation component will
try to use implication prefix in transformationspublic void importFromFileAndUnify(java.io.Reader importReader, Messages messages, int numberToProcess, Theorem selectorTheorem, OutputBoss outputBoss, boolean asciiRetest)
importReader
- source of proofsmessages
- Messages object for output messages.numberToProcess
- use to restrict the number of theorems present.selectorTheorem
- just process one theorem, ignore numberToProcess.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.asciiRetest
- instructs program to re-unify the output Proof
Worksheet text after unification.public void preprocessRequestBatchTest(java.lang.String proofText, Messages messages, OutputBoss outputBoss, PreprocessRequest preprocessRequest)
proofText
- one Proof Text Area in a String.messages
- Messages object for output messages.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.preprocessRequest
- to apply before unificationpublic void stepSelectorBatchTest(java.io.Reader importReader, Messages messages, OutputBoss outputBoss, int cursorPos, int selectionNumber)
importReader
- source of proofsmessages
- Messages object for output messages.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.cursorPos
- offset of input cursor.selectionNumber
- choice from StepSelectorResultspublic void exportToFile(java.io.Writer exportWriter, Messages messages, int numberToExport, Theorem selectorTheorem, OutputBoss outputBoss)
Uses ProofAsstPreferences.getExportFormatUnified() to determine whether output proof derivation steps contain Ref statement labels (if "unified" then yes, add labels.)
An incomplete input proof generates an incomplete output proof as well as an error message.
exportWriter
- destination for output proofs.messages
- Messages object for output messages.numberToExport
- use to restrict the number of theorems present.selectorTheorem
- just process one theorem, ignore numberToExport.outputBoss
- mmj.util.OutputBoss object, if not null means, please
print the proof test.public java.lang.String exportOneTheorem(java.lang.String theoremLabel)
public java.lang.String exportOneTheorem(Theorem theorem)
public java.lang.Iterable<Theorem> getSortedSkipSeqTheoremIterable(java.lang.String startTheoremLabel) throws ProofAsstException
ProofAsstException