public class ProofWorksheet
extends java.lang.Object
There are several inner classes, and due to the interrelated nature of the statements of a proof all of these classes are put together in ProofWorksheet (inner classes can access the outer class methods and elements.)
A large quantity of information and useful stuff is contained in mmj.pa.PaConstants.java.
=====================================================
"Derive" Feature Notes (Version 0.02)
=====================================================
The are a few changes in ProofWorksheet to support the Proof Assistant "Derive" feature. The major changes involve the Hyp and Formula fields in DerivationStep:
1. Formula: on DerivationSteps except for the "qed" step, Formula is now optional, but if Formula is not entered then Ref is required. Simple: Formula and/or Ref required on non-"qed" derivation steps.
If Formula is not entered, then the first token after the Step:Hyp:Ref field's token must be the start of a new statement in column 1 of a new line.
The new "deriveStepFormula" flag is set to true if Formula not input on a non-"qed" derivation step.
2, Hyp: "?" Hyp entries in the Hyp sub-field of Step:Hyp:Ref have a new meaning if Ref is input; there are new validation edits in this case. NOTE: this applies even to the "qed" step, but of course not the HypothesisSteps, for which a Hyp entry is meaningless and forbidden.
If one or more Hyp entries is "?" and Ref is input, then the ProofUnifier will invoke the "Derive" feature. The new "DeriveStepHyps" flag is set to true and the number of non-"?" Hyp entries must be < the number of Logical Hyps for the Ref assertion. If fewer Hyp entries are input than needed by the Ref, and one of the Hyp entries is "?", then extra "?" entries are suffixed to the Hyp sub-field. For example, if the user inputs Hyp = "?,2" and the Ref requires 3 Logical Hypotheses then the Hyp is automatically expanded to "?,2,?". Excessive "?" Hyps are also "forgiven", meaning that if the user inputs "?,2,?" and the Ref requires only 2 Logical Hypotheses, then the Hyp is shortened to "?,2" (the excess "?" Hyps are removed from the right.)
The new int field, "nbrMissingHyps" is set to the number of "?" Hyp entries -- after adjustment for the number of Logical Hypotheses needed by the Ref.
The new ProofStepStmt field, generatedByDeriveFeature
designates a
step as being automatically generated by the "Derive" feature. When set to
true a proof step can be subjected to extra/custom processing, for example,
after the unification search process.
=====================================================
Constructor and Description |
---|
ProofWorksheet(ProofAsstPreferences proofAsstPreferences,
Messages messages,
boolean structuralErrors,
ProofAsstCursor proofCursor)
Constructor for skeletal ProofWorksheet.
|
ProofWorksheet(java.lang.String newTheoremLabel,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages)
Constructor creating a ProofWorksheet initialized for a new proof for a
specific theorem label This constructor is used by
ProofAsst.startNewProof().
|
ProofWorksheet(Theorem theorem,
java.util.List<ProofDerivationStepEntry> proofDerivationStepList,
boolean deriveFormulas,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages)
Constructor used for exporting a Proof Worksheet containing a completed
proof.
|
ProofWorksheet(Tokenizer proofTextTokenizer,
ProofAsstPreferences proofAsstPreferences,
LogicalSystem logicalSystem,
Grammar grammar,
Messages messages,
MacroManager macroManager)
Constructor creating empty ProofWorksheet to be loaded using a Tokenizer.
|
Modifier and Type | Method and Description |
---|---|
DerivationStep |
addDerivStep(DerivationStep derivStep,
ProofStepStmt[] generatedHyp,
java.lang.String[] generatedHypStep,
java.lang.String refLabel,
Formula formula,
ParseTree formulaParseTree,
java.util.List<WorkVar> workVarList) |
DerivationStep |
addDerivStepForDeriveFeature(java.util.List<WorkVar> workVarList,
Formula formula,
ParseTree formulaParseTree,
DerivationStep derivStep)
Generates a DerivationStep and adds it to the proofWorkStmtList ArrayList
on behalf of ProofUnifier.
|
void |
addGeneratedProofStmt(java.util.List<Stmt> parenList,
java.lang.String letters) |
void |
addGeneratedProofStmt(ParseTree.RPNStep[] rpnProof)
Insert a GeneratedProofStmt into the ProofWorksheet
|
static ProofAsstException |
addLabelContext(ProofWorksheet proofWorksheet,
ErrorCode code,
java.lang.Object... args) |
static <T extends MMJException> |
addLabelContext(ProofWorksheet proofWorksheet,
T e) |
java.util.Set<WorkVar> |
buildProofWorksheetWorkVarSet() |
int |
computeProofWorkStmtLineNbr(ProofWorkStmt x)
Computes the line number of a ProofWorkStmt on the screen text area.
|
ProofWorkStmt |
computeProofWorkStmtOfLineNbr(int n)
Determines which ProofWorkStmt is located at a given line number of the
screen text area.
|
int |
computeTotalLineCnt()
Computes the total number of text area lines required to display all
ProofWorkStmt objects in the ProofWorksheet.
|
void |
doubleSpaceQedStep()
Add extra newline to end of qed step so that the footer step has a blank
line before it.
|
ProofWorkStmt |
findFirstMatchingRefOrStep(java.lang.String localRef) |
ProofStepStmt |
findMatchingStepFormula(Formula searchFormula,
ProofStepStmt exclusiveEndpointStep)
Searches up to an exclusive endpoint in the proofWorkStmtList for a step
whose formula matches the input formula.
|
ProofWorkStmt |
findMatchingStepNbr(java.lang.String newStepNbr) |
void |
generateAndAddDjVarsStmts()
Generate DistinctVariablesStmt set for soft DjVars errors.
|
DerivationStep |
generateDerivStep(ProofStepStmt[] generatedHyp,
java.lang.String[] generatedHypStep,
java.lang.String refLabel,
Formula formula,
ParseTree formulaParseTree,
java.util.List<WorkVar> workVarList) |
int |
generateNewDerivedStepNbr()
Generates the next value of greatestStepNbr for use in the ProofUnifier
Derive feature and returns the new value.
|
ScopeFrame |
getComboFrame()
Returns the proof theorem's "comboFrame".
|
DistinctVariablesStmt[] |
getDvStmtArray()
Returns the DistinctVariablesStmt array from the ProofWorksheet.
|
java.lang.String |
getErrorLabelIfPossible() |
static java.lang.String |
getErrorLabelIfPossible(ProofWorksheet proofWorksheet) |
FooterStmt |
getFooterStmt()
Returns the ProofWorksheet FooterStmt object.
|
GeneratedProofStmt |
getGeneratedProofStmt()
Returns the GeneratedProofStmt from the ProofWorksheet
|
HypothesisStep |
getHypothesisStepFromList(LogHyp h)
Returns a given HypothesisStep from the ProofWorkStmtList.
|
int |
getHypStepCnt()
Gets the hypStepCnt counter of the number of HypothesisStep statements in
the ProofWorksheet.
|
java.lang.String |
getLocAfterLabel() |
int |
getMaxSeq()
Returns the ProofWorksheet theorem maxSeq value.
|
int |
getNbrDerivStepsReadyForUnify()
Gets the number of proof derivation steps that are ready for Unification.
|
java.lang.String |
getOutputMessageText()
Obtain output message text from ProofWorksheet.
|
static java.lang.String |
getOutputMessageText(Messages messages)
Obtain output message text from ProofWorksheet.
|
static java.lang.String |
getOutputMessageTextAbbrev(Messages m) |
java.lang.String |
getOutputProofText()
Obtain output proof text from ProofWorksheet.
|
ProofAsstCursor |
getProofCursor()
Get the ProofWorksheet ProofCursor object.
|
java.lang.Iterable<ProofWorkStmt> |
getProofWorkStmtList()
Returns an Iterable over the ProofWorksheet ProofWorkStmt ArrayList.
|
int |
getProofWorkStmtListCnt()
Returns the count of items in the ProofWorksheet ProofWorkStmt ArrayList.
|
Cnst |
getProvableLogicStmtTyp() |
DerivationStep |
getQedStep()
Returns the QED step of the proof, which is the final derivation step.
|
ParseTree.RPNStep[] |
getQedStepProofRPN()
Returns the proof RPN of the QED step of the proof.
|
ParseTree.RPNStep[] |
getQedStepSquishedRPN() |
int |
getRPNProofLeftCol() |
StepRequest |
getStepRequest() |
Theorem |
getTheorem()
Returns the ProofWorksheet's Theorem reference.
|
java.lang.String |
getTheoremLabel()
Returns the theorem label, if present.
|
VarHyp |
getVarHypFromComboFrame(Var v) |
boolean |
hasStructuralErrors()
Gets structuralErrors switch for ProofWorksheet.
|
void |
incNbrDerivStepsReadyForUnify() |
void |
incompleteStepCursorPositioning() |
boolean |
isNewTheorem()
Returns the isNewTheorem boolean value indicating whether the theorem is
new or is already in the Metamath file that was loaded.
|
void |
loadComboFrameAndVarMap()
Load the combo frame and var array object for use throughout the
ProofWorksheet.
|
java.lang.String |
loadWorksheet(java.lang.String nextToken,
int inputCursorPos,
StepRequest stepRequestIn)
Load the ProofWorksheet starting with the input token.
|
void |
loadWorksheetProofLevelNumbers()
Initial load of proof worksheet step level numbers.
|
void |
makeLocalRefRevisionsToWorksheet() |
void |
outputCursorInstrumentationIfEnabled() |
boolean |
posCursorAtFirstIncompleteStmt(boolean afterCursor)
Positions the ProofWorksheet ProofCursor at the first ProofWorkStmt with
status = incomplete and sets the cursor at the start of the Ref
sub-field.
|
boolean |
posCursorAtLastIncompleteStmt(boolean beforeCursor)
Positions the ProofWorksheet ProofCursor at the last ProofWorkStmt with
status = incomplete and sets the cursor at the start of the Ref
sub-field.
|
void |
posCursorAtQedStmt()
Positions the cursor at the 'qed' step if the cursor is not already set.
|
void |
renumberProofSteps(int renumberStart,
int renumberInterval)
Renumbers each ProofWorkStmt according to an input renumberInterval and
alters each Hyp reference to conform to the new step numbers.
|
void |
runCallback(MacroManager.CallbackType c)
Run a macro callback.
|
void |
setMaxSeq(int maxSeq) |
void |
setNewTheorem(boolean newTheorem) |
void |
setProofCursor(ProofAsstCursor proofCursor)
Set the ProofWorksheet ProofCursor object.
|
void |
setStructuralErrors(boolean structuralErrors)
Sets structuralErrors switch for ProofWorksheet.
|
void |
tmffReformat(boolean inputCursorStep)
Reformats all or just one ProofStepStmt using TMFF.
|
void |
triggerLoadStructureException(ErrorCode code,
java.lang.Object... args) |
void |
triggerLoadStructureException(int errorFldChars,
ErrorCode code,
java.lang.Object... args) |
public ProofAsstPreferences proofAsstPreferences
public LogicalSystem logicalSystem
public Grammar grammar
public Messages messages
public Tokenizer proofTextTokenizer
public TMFFPreferences tmffPreferences
public TMFFStateParams tmffSP
public java.lang.StringBuilder tmffFormulaSB
public MacroManager macroManager
public StepSelectorResults stepSelectorResults
public StepRequest stepRequest
public SearchOutput searchOutput
public boolean structuralErrors
public int nbrDerivStepsReadyForUnify
public boolean hasWorkVarsOrDerives
public boolean newTheorem
public Theorem theorem
public Stmt locAfter
public int maxSeq
public ScopeFrame comboFrame
public java.util.Map<java.lang.String,Var> comboVarMap
public java.util.List<ProofWorkStmt> proofWorkStmtList
public HeaderStmt headerStmt
public FooterStmt footerStmt
public DerivationStep qedStep
public GeneratedProofStmt generatedProofStmt
public int greatestStepNbr
public int dvStmtCnt
public DistinctVariablesStmt[] dvStmtArray
public int hypStepCnt
public ProofAsstCursor proofCursor
public ProofAsstCursor proofInputCursor
public java.util.List<java.util.List<DjVars>> proofSoftDjVarsErrorList
public java.util.List<DerivationStep> stepsWithLocalRefs
public ProofWorksheet(ProofAsstPreferences proofAsstPreferences, Messages messages, boolean structuralErrors, ProofAsstCursor proofCursor)
proofAsstPreferences
- variable settingsmessages
- the mmj.lang.Messages object used to store error and
informational messages.structuralErrors
- indicates whether or not the ProofWorksheet has
severe/fatal validation errors.proofCursor
- ProofAsstCursor set to position of error.public ProofWorksheet(Tokenizer proofTextTokenizer, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages, MacroManager macroManager)
proofTextTokenizer
- the mmj.mmio.Tokenizer input stream parser.proofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.macroManager
- the mmj.pa.MacroManager objectpublic ProofWorksheet(java.lang.String newTheoremLabel, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages)
newTheoremLabel
- Theorem label String.proofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.public ProofWorksheet(Theorem theorem, java.util.List<ProofDerivationStepEntry> proofDerivationStepList, boolean deriveFormulas, ProofAsstPreferences proofAsstPreferences, LogicalSystem logicalSystem, Grammar grammar, Messages messages)
theorem
- to be used to create ProofWorksheet.proofDerivationStepList
- List of
mmj.verify.ProofDerivationStepEntry created by VerifyProofsderiveFormulas
- if true, derive formulas during creationproofAsstPreferences
- variable settingslogicalSystem
- the loaded Metamath datagrammar
- the mmj.verify.Grammar objectmessages
- the mmj.lang.Messages object used to store error and
informational messages.public boolean hasStructuralErrors()
public void setStructuralErrors(boolean structuralErrors)
See hasStructuralErrors() for more info.
structuralErrors
- boolean, true or false.public int getNbrDerivStepsReadyForUnify()
Note: a derivation step with a "?" in its Hyp field is not ready for unification, but interestingly, a subsequent step that refers to that step as one of its Hyps, can be unified (it just can't be "proved".)
public void incNbrDerivStepsReadyForUnify()
public boolean isNewTheorem()
public void setNewTheorem(boolean newTheorem)
public Theorem getTheorem()
public int getMaxSeq()
For an existing theorem (in the loaded database), maxSeq is just the MObj.seq number of the theorem itself. For a new theorem the LocAfter statement label defines the maxSeq (maxSeq = locAfter.seq + 1)
The maxSeq value sets a boundary for parsing, proofs, formulas, etc. A Metamath statement cannot legitimately use or refer to another Metamath statement with a sequence number >= its own (no recursive references.)
public void setMaxSeq(int maxSeq)
public ScopeFrame getComboFrame()
"comboFrame" and comboVarMap combine the optional and mandatory frame entries for the theorem, including any $d statements added as part of the proof.
For an existing theorem this just means merging the Assrt.mandFrame, Theorem.optFrame and any proof $d's, and then deriving the comboVarMap from the set of VarHyp's in the comboFrame.
For a new theorem this means constructing comboFrame using (ScopeDef)(LogicalSystem.getScopeDefList()).get(0) to obtain the sets of globally active Var's, VarHyp's and DjVars (new Theorems in ProofAsst can only use global scope Var's and VarHyp's) and adding in any $d's from the proof.
The REASON why the optional and mandatory frames can be combined in this way is a little bit subtle: they only need to be separate if the new theorem is going to be referred to in later theorems' proofs, and ProofAsst does not provide that capability at this time.
The REASON why we want to combine the optional and mandatory frames is to simplify handling of derivation steps within the proof. Variables used in the intermediate steps would normally be part of the optional frame, if not used in the theorem's formula or its LogHyp formulas. That would create more work, especially at grammatical parse time, when we need to match each Var to its active VarHyp. Soooo...instead of building a mandatory frame for each intermediate step we just build a combo frame for use in every step (and note that DjVars apply to every step regardless of the location of the $d ProofWorkStmt within the Proof Text area.
public int getHypStepCnt()
public HypothesisStep getHypothesisStepFromList(LogHyp h)
h
- the LogHyp sought in the ProofWorkStmtList.public java.util.Set<WorkVar> buildProofWorksheetWorkVarSet()
public java.lang.Iterable<ProofWorkStmt> getProofWorkStmtList()
public int getProofWorkStmtListCnt()
public int computeProofWorkStmtLineNbr(ProofWorkStmt x)
This algorithm requires that we know in advance how many lines are occupied by each ProofWorkStmt. The computation is then simple: just total the previous lineCnt's and add 1. (But if lineCnt is wrong, then we are doomed -- note that TMFF went to a lot of trouble to obtain lineCnt, and lineCnt is computed during parsing of an input ProofWorksheet!)
x
- the owner ProofWorkStmtpublic ProofWorkStmt computeProofWorkStmtOfLineNbr(int n)
n
- the line numberpublic int computeTotalLineCnt()
public FooterStmt getFooterStmt()
public DerivationStep getQedStep()
Note: the nomenclature here "qed step" is something made up for ProofAssistant to make things easier to explain.
public ParseTree.RPNStep[] getQedStepProofRPN()
Note that each DerivationStep will have its own proof -- if the proof is valid -- but the QED step's proof is the proof of the theorem itself!
public ParseTree.RPNStep[] getQedStepSquishedRPN()
public ProofAsstCursor getProofCursor()
public void setProofCursor(ProofAsstCursor proofCursor)
proofCursor
- object for ProofWorksheet.public void posCursorAtQedStmt()
public boolean posCursorAtLastIncompleteStmt(boolean beforeCursor)
beforeCursor
- true if the search starts at the cursorpublic boolean posCursorAtFirstIncompleteStmt(boolean afterCursor)
afterCursor
- true if the search starts at the cursorpublic void incompleteStepCursorPositioning()
public void outputCursorInstrumentationIfEnabled()
public java.lang.String getErrorLabelIfPossible()
public static java.lang.String getErrorLabelIfPossible(ProofWorksheet proofWorksheet)
public static <T extends MMJException> T addLabelContext(ProofWorksheet proofWorksheet, T e)
public static ProofAsstException addLabelContext(ProofWorksheet proofWorksheet, ErrorCode code, java.lang.Object... args)
public java.lang.String getTheoremLabel()
public java.lang.String getLocAfterLabel()
public StepRequest getStepRequest()
public int getRPNProofLeftCol()
public ProofStepStmt findMatchingStepFormula(Formula searchFormula, ProofStepStmt exclusiveEndpointStep)
searchFormula
- Formula we're looking forexclusiveEndpointStep
- Exclusive endpoint of the search (return
null as soon as this step is reached, even if its formula
matches.)public void renumberProofSteps(int renumberStart, int renumberInterval)
renumberStart
- is the number to start at. Commonly equal to 1.renumberInterval
- is the number to add to each new step number.
Commonly equal to 1.public void tmffReformat(boolean inputCursorStep)
inputCursorStep
- set to true to reformat just the proof step
underneath the cursor.public void doubleSpaceQedStep()
public DerivationStep addDerivStepForDeriveFeature(java.util.List<WorkVar> workVarList, Formula formula, ParseTree formulaParseTree, DerivationStep derivStep)
If !workVarList.isEmpty() then the new step is marked incomplete and given a Hyp = "?" -- no unification need be attempted. Otherwise, unification can be attempted using no Hyps. If this fails then because the step is marked "generated", the step can be updated to show Hyp "?" (this is a helpful feature for the users, going the extra mile...)
workVarList
- List of Work Vars in formula.formula
- Formula of new step.formulaParseTree
- ParseTree of new FormuladerivStep
- insert point for new step.public DerivationStep addDerivStep(DerivationStep derivStep, ProofStepStmt[] generatedHyp, java.lang.String[] generatedHypStep, java.lang.String refLabel, Formula formula, ParseTree formulaParseTree, java.util.List<WorkVar> workVarList)
public DerivationStep generateDerivStep(ProofStepStmt[] generatedHyp, java.lang.String[] generatedHypStep, java.lang.String refLabel, Formula formula, ParseTree formulaParseTree, java.util.List<WorkVar> workVarList)
public int generateNewDerivedStepNbr()
public java.lang.String loadWorksheet(java.lang.String nextToken, int inputCursorPos, StepRequest stepRequestIn) throws java.io.IOException, MMIOException, ProofAsstException
Otherwise, return the nextToken value which should be the first token of the next ProofWorksheet or null if EOF. (Each routine that loads a statement will return the next token after the end of the statement's input text.)
nextToken
- the first token to be loaded.inputCursorPos
- offset plus one of Caret in Proof TextArea or -1 if
not available.stepRequestIn
- may be null, or StepSelector Search or Choice
request and will be loaded into the ProofWorksheet.java.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic void makeLocalRefRevisionsToWorksheet()
public void loadWorksheetProofLevelNumbers()
public java.lang.String getOutputMessageText()
Note: this is a key function used by ProofAsstGUI.
Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.
public static java.lang.String getOutputMessageText(Messages messages)
Note: this is a key function used by ProofAsstGUI.
Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.
messages
- Messages object.public static java.lang.String getOutputMessageTextAbbrev(Messages m)
public java.lang.String getOutputProofText()
Note: this is a key function used by ProofAsstGUI.
Note: with word wrap 'on', newlines are ignored in JTextArea, so we insert spacer lines.
public void addGeneratedProofStmt(ParseTree.RPNStep[] rpnProof)
Note: this is used by ProofAsst after successful unification.
rpnProof
- Proof Stmt array.public void addGeneratedProofStmt(java.util.List<Stmt> parenList, java.lang.String letters)
public GeneratedProofStmt getGeneratedProofStmt()
Note: returns null if unification unsuccessful or not yet performed.
public DistinctVariablesStmt[] getDvStmtArray()
Note: may return null.
public void generateAndAddDjVarsStmts()
Input is ProofWorksheet.proofSoftDjVarsErrorList and ProofAsstPreferences, which determines whether a full replacement set of DistinctVariableStmt's must be created, or only the differences to what is already on the theorem in the .mm database.
Note that the ProofWorksheet's dvStmtArray, dvStmtCnt and comboFrame are updated -- even though at this time there is no known use of these data items after this point in the processing (which is just prior to displaying the fully-unified proof on the GUI screen). However, there may be a use for the updated data items in testing, and in any case it is best no to leave loose ends dangling.
public Cnst getProvableLogicStmtTyp()
public ProofWorkStmt findFirstMatchingRefOrStep(java.lang.String localRef)
public ProofWorkStmt findMatchingStepNbr(java.lang.String newStepNbr)
public void loadComboFrameAndVarMap()
public void triggerLoadStructureException(ErrorCode code, java.lang.Object... args) throws ProofAsstException
ProofAsstException
public void triggerLoadStructureException(int errorFldChars, ErrorCode code, java.lang.Object... args) throws ProofAsstException
ProofAsstException
public void runCallback(MacroManager.CallbackType c)
c
- The type of callback (event trigger)