public abstract class ProofStepStmt extends ProofWorkStmt
Modifier and Type | Field and Description |
---|---|
ParseTree |
formulaParseTree
if parse tree null, unification cannot be attempted for the step or for
other steps that refer to this step as an hypothesis.
|
protected int |
formulaStartCharNbr
obtained on input, used for carat positioning on errors during input
validation.
|
Constructor and Description |
---|
ProofStepStmt(ProofWorksheet w)
Default Constructor.
|
ProofStepStmt(ProofWorksheet w,
java.lang.String step,
java.lang.String refLabel,
Formula formula,
boolean setCaret)
Constructor for incomplete ProofStepStmt destined only for output to the
GUI.
|
Modifier and Type | Method and Description |
---|---|
void |
accumSetOfWorkVarsUsed(java.util.Set<WorkVar> set) |
protected void |
accumWorkVarList(WorkVar workVar) |
int |
computeFieldIdCol(int fieldId)
Computes column number in the proof step text of the input field id.
|
int |
computeFieldIdColRef()
Function used for cursor positioning.
|
ParseNode |
getCanonicalForm() |
Formula |
getFormula() |
ProofStepStmt |
getLocalRef() |
protected void |
getNewFormulaStepParseTree() |
Stmt |
getRef()
Gets the Ref Stmt for the step.
|
java.lang.String |
getRefLabel()
Gets the Ref label for the step.
|
java.lang.String |
getStep() |
java.lang.String |
getStmtDiagnosticInfo()
Returns diagnostic data for this ProofWorkStmt, which in this case is the
Class name.
|
int |
hashCode() |
boolean |
hasMatchingRefLabel(java.lang.String ref)
Function to determine whether the ProofWorkStmt Ref Label matches the
input string (always false in base class.)
|
boolean |
hasMatchingStepNbr(java.lang.String newStepNbr)
Compares input Step number to this step.
|
void |
loadProofLevel(int proofLevel)
Loads the proofLevel number with the input proofLevel but only if the
existing proofLevel is zero.
|
protected void |
loadStepHypRefIntoStmtText(int origStepHypRefLength,
java.lang.StringBuilder stepHypRef) |
protected int |
loadStmtText(java.lang.StringBuilder stepHypRef,
Formula formula,
ParseTree parseTree)
Renders formula into stepHypRef string buffer and returns the number of
lines in the formula.
|
java.lang.String |
loadStmtTextWithFormula(boolean workVarsOk)
Loads stmtText and formula fields with the input tokens.
|
abstract void |
reloadStepHypRefInStmtText()
Updates the Step/Hyp/Ref field in the statement text area of the proof
step.
|
abstract void |
renum(java.util.Map<java.lang.String,java.lang.String> renumberMap)
Renumbers step numbers using a HashMap containing old and new step number
pairs.
|
protected void |
reviseStepHypRefInStmtText(java.lang.StringBuilder newStepHypRef) |
static void |
reviseStepHypRefInStmtTextArea(java.lang.StringBuilder textArea,
java.lang.StringBuilder newTextPrefix)
Updates the first token of the text area.
|
void |
setCanonicalForm(ParseNode canonicalForm) |
void |
setFormula(Formula formula) |
void |
setRef(Stmt ref)
Sets the Ref Stmt for the step.
|
void |
setRefLabel(java.lang.String refLabel)
Sets the Ref label for the step.
|
void |
setStep(java.lang.String step) |
void |
tmffReformat()
Reformats Derivation Step using TMFF.
|
void |
updateFormulaParseTree(ParseTree parseTree)
Updates the ProofStepStmt ParseTree, resetting maxDepth and levelOneTwo
data.
|
boolean |
updateStmtTextWithWorkVarUpdates(VerifyProofs verifyProofs)
Updates stmtText in place using substitution values assigned to work
variables used in the step.
|
void |
updateWorkVarList(java.util.List<WorkVar> workVarList)
Updates the workVarList for the ProofStepStmt and if the revised
workVarList is null turns off the formulaFldIncomplete flag.
|
appendToProofText, getLineCnt, getProofWorksheet, getStmtText, load, loadAllStmtTextGetNextStmt, loadStmtTextGetNextStmt, loadStmtTextGetOptionalToken, loadStmtTextGetRequiredToken, setStmtCursorToCurrLineColumn, stmtIsIncomplete, updateLineCntUsingTokenizer
protected int formulaStartCharNbr
public ParseTree formulaParseTree
public ProofStepStmt(ProofWorksheet w)
w
- the owning ProofWorksheetpublic ProofStepStmt(ProofWorksheet w, java.lang.String step, java.lang.String refLabel, Formula formula, boolean setCaret)
Creates "incomplete" ProofStepStmt which is destined only for output to the GUI, hence, the object references, etc. are not loaded. After display to the GUI this worksheet disappears -- recreated via "load" each time the user selects "StartUnification".
w
- The owning ProofWorksheetstep
- step number of the ProofStepStmtrefLabel
- Ref label of the ProofStepStmtformula
- the proof step formulasetCaret
- true means position caret of TextArea to this statement.public java.lang.String getStep()
public void setStep(java.lang.String step)
public void loadProofLevel(int proofLevel)
Note: does not update a non-zero proofLevel because a step can be used more than once as an hypothesis, so different level numbers could result.
proofLevel
- value to store if existing level is zero.public int computeFieldIdCol(int fieldId)
computeFieldIdCol
in class ProofWorkStmt
fieldId
- value identify ProofWorkStmt field for cursor positioning,
as defined in PaConstants.FIELD_ID_*.public void tmffReformat()
tmffReformat
in class ProofWorkStmt
public int computeFieldIdColRef()
The function looks for the Ref in the 2nd colon in the ProofWorkStmt.stmtText and sets the output column to the column *after* the 2nd colon -- but returns 1 if whitespace is found before the 2nd colon in the stmtText.
public void updateFormulaParseTree(ParseTree parseTree)
parseTree
- the new ParseTree for the step.public void accumSetOfWorkVarsUsed(java.util.Set<WorkVar> set)
public void updateWorkVarList(java.util.List<WorkVar> workVarList)
workVarList
- List of WorkVar listing the WorkVar used in the step
formula.public boolean updateStmtTextWithWorkVarUpdates(VerifyProofs verifyProofs)
NOTE: This is a dirty little hack :-)
verifyProofs
- instance of VerifyProofs for use converting an RPN
list to a formula.public java.lang.String loadStmtTextWithFormula(boolean workVarsOk) throws java.io.IOException, MMIOException, ProofAsstException
The formula is loaded and validated before Step/Hyp/Ref so that the formula symbols can be validated as they are read in. We return to validate Step/Hyp/Ref after doing the formula. The big problem being solved here is positioning the caret as accurately as possible to the first reported error on the line.
workVarsOk
- indicator to allow/disallow WorkVar syms in this
formula.java.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic boolean hasMatchingRefLabel(java.lang.String ref)
hasMatchingRefLabel
in class ProofWorkStmt
ref
- string to compare to ProofWorkStmt refLabel string.public boolean hasMatchingStepNbr(java.lang.String newStepNbr)
hasMatchingStepNbr
in class ProofWorkStmt
newStepNbr
- step number to comparepublic void setRef(Stmt ref)
ref
- Stmt in LogicalSystempublic Stmt getRef()
public void setRefLabel(java.lang.String refLabel)
Note: refLabel is input first and Ref is derived, but for new Theorems, Ref may not exist, which is why we carry both around at all times.
refLabel
- Ref label for the step.public java.lang.String getRefLabel()
public java.lang.String getStmtDiagnosticInfo()
ProofWorkStmt
getStmtDiagnosticInfo
in class ProofWorkStmt
public static void reviseStepHypRefInStmtTextArea(java.lang.StringBuilder textArea, java.lang.StringBuilder newTextPrefix)
Assumes text already contains StepHypRef token.
Objective is to avoid changing the position of the other tokens within the text area -- as much as possible.
textArea
- step stmtText area or similar text area.newTextPrefix
- revised first token of text area.protected int loadStmtText(java.lang.StringBuilder stepHypRef, Formula formula, ParseTree parseTree)
stepHypRef
- the string bufferformula
- the formulaparseTree
- of the Formula to be rendered. If left null, the formula
will be output in unformattedprotected void accumWorkVarList(WorkVar workVar)
protected void getNewFormulaStepParseTree() throws ProofAsstException
ProofAsstException
protected void loadStepHypRefIntoStmtText(int origStepHypRefLength, java.lang.StringBuilder stepHypRef)
public abstract void reloadStepHypRefInStmtText()
This is needed because Unify can alter Hyp and Ref.
protected void reviseStepHypRefInStmtText(java.lang.StringBuilder newStepHypRef)
public abstract void renum(java.util.Map<java.lang.String,java.lang.String> renumberMap)
renumberMap
- contains key/value pairs defining newly assigned step
numbers.public ProofStepStmt getLocalRef()
public Formula getFormula()
public void setFormula(Formula formula)
public ParseNode getCanonicalForm()
public void setCanonicalForm(ParseNode canonicalForm)
public int hashCode()
hashCode
in class java.lang.Object