public class HypothesisStep extends ProofStepStmt
On the GUI a HypothesisStep is shown with an 'h' prefix to step number.
A HypothesisStep cannot have Hyp's in its Step/Hyp/Ref field. Nor does it have a proof, just a parse tree.
formulaParseTree, formulaStartCharNbr
Constructor and Description |
---|
HypothesisStep(ProofWorksheet w)
Default Constructor.
|
HypothesisStep(ProofWorksheet w,
java.lang.String step,
java.lang.String refLabel,
Formula formula,
ParseTree parseTree,
boolean setCaret,
int proofLevel)
Constructor for incomplete DerivationStep destined only for output to the
GUI.
|
Modifier and Type | Method and Description |
---|---|
boolean |
hasMatchingRefLabel(java.lang.String newRefLabel)
Compares input Ref label to this step.
|
java.lang.String |
loadHypothesisStep(int origStepHypRefLength,
int lineStartCharNbr,
java.lang.String stepField,
java.lang.String refField)
Loads HypothesisStep with step and ref.
|
void |
reloadStepHypRefInStmtText()
Updates the Step/Hyp/Ref field in the statement text area of the proof
step.
|
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.
|
boolean |
stmtIsIncomplete()
Is statement incomplete?
|
void |
tmffReformat()
Reformats Hypothesis Step using TMFF.
|
java.lang.String |
toString() |
accumSetOfWorkVarsUsed, accumWorkVarList, computeFieldIdCol, computeFieldIdColRef, getCanonicalForm, getFormula, getLocalRef, getNewFormulaStepParseTree, getRef, getRefLabel, getStep, getStmtDiagnosticInfo, hashCode, hasMatchingStepNbr, loadProofLevel, loadStepHypRefIntoStmtText, loadStmtText, loadStmtTextWithFormula, reviseStepHypRefInStmtText, reviseStepHypRefInStmtTextArea, setCanonicalForm, setFormula, setRef, setRefLabel, setStep, updateFormulaParseTree, updateStmtTextWithWorkVarUpdates, updateWorkVarList
public HypothesisStep(ProofWorksheet w)
w
- the owning ProofWorksheetpublic HypothesisStep(ProofWorksheet w, java.lang.String step, java.lang.String refLabel, Formula formula, ParseTree parseTree, boolean setCaret, int proofLevel)
Creates "incomplete" HypothesisStep 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 proof steprefLabel
- Ref label of the proof stepformula
- the proof step formulaparseTree
- formula ParseTree (can be null)setCaret
- true means position caret of TextArea to this statement.proofLevel
- level of step in proof.public boolean stmtIsIncomplete()
ProofWorkStmt
-- used primarily for cursor positioning:
-- a virtual method that checks the statement for the state of "incompleteness" of data as indicated by state variables in the specific ProofWorkStmt types.
stmtIsIncomplete
in class ProofWorkStmt
public boolean hasMatchingRefLabel(java.lang.String newRefLabel)
hasMatchingRefLabel
in class ProofStepStmt
newRefLabel
- ref label to comparepublic void renum(java.util.Map<java.lang.String,java.lang.String> renumberMap)
ProofStepStmt
renum
in class ProofStepStmt
renumberMap
- contains key/value pairs defining newly assigned step
numbers.public void reloadStepHypRefInStmtText()
This is needed because Unify can alter Hyp and Ref.
reloadStepHypRefInStmtText
in class ProofStepStmt
public void tmffReformat()
Note: This isn't guaranteed to work unless the Proof Worksheet is free of structural errors. Also, a formula which has not yet been parsed or which failed to parse successfully will contain a null parse tree and be formatted using Format 0 - "Unformatted".
tmffReformat
in class ProofStepStmt
public java.lang.String loadHypothesisStep(int origStepHypRefLength, int lineStartCharNbr, java.lang.String stepField, java.lang.String refField) throws java.io.IOException, MMIOException, ProofAsstException
This method is passed the contents of the first token which has already been parsed into step, and ref fields and loads them into the HypothesisStep -- which already contains the step's formula! This back-asswardness is a result of trying to maintain cursor/caret control when the formula is validated. Messy...
origStepHypRefLength
- length of first token of statementlineStartCharNbr
- character number in the input stream of the
statement startstepField
- step number fieldrefField
- step ref fieldjava.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic java.lang.String toString()
toString
in class java.lang.Object