public class DerivationStep extends ProofStepStmt
Modifier and Type | Field and Description |
---|---|
MMJException |
heldDjErrorMessage |
formulaParseTree, formulaStartCharNbr
Constructor and Description |
---|
DerivationStep(ProofWorksheet w)
Default Constructor.
|
DerivationStep(ProofWorksheet w,
java.lang.String generatedStep,
ProofStepStmt[] generatedHyp,
java.lang.String[] generatedHypStep,
java.lang.String refLabel,
Formula generatedFormula,
ParseTree generatedParseTree,
boolean generatedFormulaFldIncomplete,
boolean generatedHypFldIncomplete,
boolean auto,
java.util.List<WorkVar> generatedWorkVarList)
Constructor for generated DerivationSteps created during Unification.
|
DerivationStep(ProofWorksheet w,
java.lang.String step,
java.lang.String[] hypStep,
java.lang.String refLabel,
Formula formula,
ParseTree parseTree,
boolean setCaret,
int proofLevel)
Constructor for incomplete DerivationStep destined only for output to the
GUI.
|
DerivationStep(ProofWorksheet w,
java.lang.String step,
java.lang.String[] hypStep,
java.lang.String refLabel,
Formula formula,
ParseTree parseTree,
boolean setCaret,
int proofLevel,
boolean autoStep)
Constructor for incomplete DerivationStep destined only for output to the
GUI.
|
Modifier and Type | Method and Description |
---|---|
void |
buildSoftDjErrorMessage(java.util.List<DjVars> softDjVarsErrorList)
Builds an error message detailing the "soft" DjVars errors and stores it
in the heldDjErrorMessage field.
|
java.lang.StringBuilder |
buildStepHypRefSB()
Creates the Step/Hyp/Ref field and loads it into a new StringBuilder.
|
ParseNode |
getAssrtSubst(int i) |
ParseNode[] |
getAssrtSubstList() |
int |
getAssrtSubstNumber() |
ProofStepStmt |
getHyp(int i) |
ProofStepStmt[] |
getHypList() |
int |
getHypNumber() |
ProofStepStmt |
getLocalRef() |
java.lang.String |
getLogHypsL1HiLoKey() |
int |
getLogHypsMaxDepth() |
ParseTree |
getProofTree()
Get the proofTree.
|
ProofStepStmt[] |
getSortedHypArray()
Gets the HypArray sorted using a lazy evaluation to perform the sort.
|
boolean |
hasDeriveStepFormula() |
boolean |
hasDeriveStepHyps() |
boolean |
hasWorkVarsInStepOrItsHyps()
Returns true if the DerivationStep or its hypotheses contain Work
Variables.
|
boolean |
isAutoStep() |
boolean |
isGeneratedByDeriveFeature() |
boolean |
isHypFldIncomplete() |
java.lang.String |
loadDerivationStep(int origStepHypRefLength,
int lineStartCharNbr,
java.lang.String stepField,
java.lang.String hypField,
java.lang.String refField)
Loads DerivationStep with step, hyp and ref.
|
void |
loadDerivationStepHypLevels()
Set proofLevel numbers of hypotheses of DerivationStep.
|
void |
loadGeneratedFormulaIntoDerivStep(Formula genFormula,
ParseTree genFormulaParseTree,
boolean stmtTextAlreadyLoaded)
Loads generated Formula and its ParseTree into DerivationStep and
recomputes reference steps' L1HiLo key values.
|
java.lang.String |
loadLocalRefDerivationStep(int origStepHypRefLength,
int lineStartCharNbr,
java.lang.String stepField,
java.lang.String hypField,
java.lang.String localRefField)
Loads DerivationStep with step, hyp and a localRef to a previous proof
step.
|
void |
reloadLogHypKeysAndMaxDepth()
Updates these pesky things used in ProofUnifier for speedy scanning
during Unification Search.
|
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.
|
void |
resetSortedHypArray()
Sets the sortedHypArray to null.
|
void |
setAssrtSubst(int i,
ParseNode node) |
void |
setAssrtSubstList(ParseNode[] assrtSubst)
Set the assrtSubst array.
|
void |
setAutoStep(boolean autoStep) |
void |
setHyp(int i,
ProofStepStmt stmt) |
void |
setHypFldIncomplete(boolean hypFldIncomplete) |
void |
setHypList(ProofStepStmt[] hypArray) |
void |
setHypStep(int i,
java.lang.String s) |
void |
setHypStepList(java.lang.String[] hypStep) |
void |
setLocalRef(ProofStepStmt localRef) |
void |
setProofTree(ParseTree proofTree)
Set the proofTree.
|
void |
setSortedHypArray(ProofStepStmt[] sortedHypArray)
Sets the sortedHypArray.
|
static ProofStepStmt[] |
sortDerivStepHypArray(ProofStepStmt[] dArray)
Sorts DerivationStep hyp array in descending order of hypothesis step
formula length.
|
boolean |
stmtIsIncomplete()
Returns true if the DerivationStep is considered incomplete.
|
void |
swapHyps(int i,
int j)
Swap two hyp references in a DerivationStep.
|
void |
tmffReformat()
Reformats Derivation Step using TMFF.
|
java.lang.String |
toString() |
void |
validateHyps() |
accumSetOfWorkVarsUsed, accumWorkVarList, computeFieldIdCol, computeFieldIdColRef, getCanonicalForm, getFormula, getNewFormulaStepParseTree, getRef, getRefLabel, getStep, getStmtDiagnosticInfo, hashCode, hasMatchingRefLabel, hasMatchingStepNbr, loadProofLevel, loadStepHypRefIntoStmtText, loadStmtText, loadStmtTextWithFormula, reviseStepHypRefInStmtText, reviseStepHypRefInStmtTextArea, setCanonicalForm, setFormula, setRef, setRefLabel, setStep, updateFormulaParseTree, updateStmtTextWithWorkVarUpdates, updateWorkVarList
public MMJException heldDjErrorMessage
public DerivationStep(ProofWorksheet w)
w
- the owner ProofWorksheetpublic DerivationStep(ProofWorksheet w, java.lang.String step, java.lang.String[] hypStep, java.lang.String refLabel, Formula formula, ParseTree parseTree, boolean setCaret, int proofLevel, boolean autoStep)
Creates "incomplete" DerivationStep 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 owner ProofWorksheetstep
- step number of the proof stephypStep
- array of hyp step numbers for 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.autoStep
- true if this step is auto steppublic DerivationStep(ProofWorksheet w, java.lang.String step, java.lang.String[] hypStep, java.lang.String refLabel, Formula formula, ParseTree parseTree, boolean setCaret, int proofLevel)
Creates "incomplete" DerivationStep 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 owner ProofWorksheetstep
- step number of the proof stephypStep
- array of hyp step numbers for 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 DerivationStep(ProofWorksheet w, java.lang.String generatedStep, ProofStepStmt[] generatedHyp, java.lang.String[] generatedHypStep, java.lang.String refLabel, Formula generatedFormula, ParseTree generatedParseTree, boolean generatedFormulaFldIncomplete, boolean generatedHypFldIncomplete, boolean auto, java.util.List<WorkVar> generatedWorkVarList)
w
- the owner ProofWorksheetgeneratedHyp
- array of ProofStepStmtgeneratedStep
- array of step number stringsgeneratedHypStep
- array of hyp step numbers for the proof steprefLabel
- Ref label of the proof step (could be "")generatedFormula
- Formula of new step.generatedParseTree
- Formula's ParseTreegeneratedFormulaFldIncomplete
- see
ProofStepStmt.formulaFldIncomplete
generatedHypFldIncomplete
- see
hypFldIncomplete
auto
- true if this is an autocomplete stepgeneratedWorkVarList
- List of Work Vars in formulapublic static ProofStepStmt[] sortDerivStepHypArray(ProofStepStmt[] dArray)
dArray
- array of ProofStepStmt.public void loadDerivationStepHypLevels()
public boolean hasWorkVarsInStepOrItsHyps()
public boolean stmtIsIncomplete()
"Incomplete" here means that hypFldIncomplete, or formulaFldIncomplete is true, or the formulaParseTree is null.
stmtIsIncomplete
in class ProofWorkStmt
public 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 tmffReformat()
tmffReformat
in class ProofStepStmt
public java.lang.String loadDerivationStep(int origStepHypRefLength, int lineStartCharNbr, java.lang.String stepField, java.lang.String hypField, 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, hyp and ref fields and loads them into the DerivationStep -- 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 fieldhypField
- step hyps fieldrefField
- step ref fieldjava.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic void validateHyps() throws ProofAsstException
ProofAsstException
public java.lang.String loadLocalRefDerivationStep(int origStepHypRefLength, int lineStartCharNbr, java.lang.String stepField, java.lang.String hypField, java.lang.String localRefField) throws java.io.IOException, MMIOException, ProofAsstException
This routine exists solely to validate the localRef and the step number so that subsequent step(s) that refer to it (as a Hyp) can be validated, and then later be redirected to point to the step that the localRef is pointing to. There are two possibilities: a structure error -- in which case the ProofWorksheet is redisplayed as is -- or the step and localRef are 100% valid, in which case this step will be deleted from the ProofWorksheet during the "finale" of loadWorksheet() in ProofWorksheet.java. So none of the other fields in the DerivationStep are important.
origStepHypRefLength
- length of first token of statementlineStartCharNbr
- character number in the input stream of the
statement startstepField
- step number fieldhypField
- step hyps fieldlocalRefField
- ProofStepStmt ref to previous stepjava.io.IOException
- if an error occurredMMIOException
- if an error occurredProofAsstException
- if an error occurredpublic void loadGeneratedFormulaIntoDerivStep(Formula genFormula, ParseTree genFormulaParseTree, boolean stmtTextAlreadyLoaded)
This is a helper routine for ProofUnifier.java.
genFormula
- new generated Formula.genFormulaParseTree
- ParseTree for Formula.stmtTextAlreadyLoaded
- false if stmtText must be recomputed from
scratch.public void reloadStepHypRefInStmtText()
This is needed because Unify can alter Hyp and Ref.
reloadStepHypRefInStmtText
in class ProofStepStmt
public void reloadLogHypKeysAndMaxDepth()
public java.lang.StringBuilder buildStepHypRefSB()
public void setAssrtSubstList(ParseNode[] assrtSubst)
assrtSubst
- ParseNode array.public ParseNode[] getAssrtSubstList()
public int getAssrtSubstNumber()
public ParseNode getAssrtSubst(int i)
public void setAssrtSubst(int i, ParseNode node)
public ParseTree getProofTree()
public void setProofTree(ParseTree proofTree)
proofTree
- new proof tree.public void swapHyps(int i, int j)
i
- index of first hyp to swapj
- index of second hyp to swappublic void buildSoftDjErrorMessage(java.util.List<DjVars> softDjVarsErrorList)
softDjVarsErrorList
- List of DjVars reported to be missing from the
Dj Vars of the theorem which are needed by the Derivation
Step.public ProofStepStmt[] getSortedHypArray()
public void resetSortedHypArray()
public void setSortedHypArray(ProofStepStmt[] sortedHypArray)
sortedHypArray
- sorted array of ProofStepStmt.public ProofStepStmt[] getHypList()
public void setHypList(ProofStepStmt[] hypArray)
public ProofStepStmt getHyp(int i)
public void setHyp(int i, ProofStepStmt stmt)
public int getHypNumber()
public java.lang.String toString()
toString
in class java.lang.Object
public void setHypStep(int i, java.lang.String s)
public void setHypStepList(java.lang.String[] hypStep)
public java.lang.String getLogHypsL1HiLoKey()
public int getLogHypsMaxDepth()
public boolean hasDeriveStepFormula()
public boolean hasDeriveStepHyps()
public ProofStepStmt getLocalRef()
getLocalRef
in class ProofStepStmt
public void setLocalRef(ProofStepStmt localRef)
public boolean isGeneratedByDeriveFeature()
public boolean isHypFldIncomplete()
public void setHypFldIncomplete(boolean hypFldIncomplete)
public boolean isAutoStep()
public void setAutoStep(boolean autoStep)