public class TheoremStmtGroup
extends java.lang.Object
Note: TheoremStmtGroup refers to the fact that a MMTTheoremFile consists of a group of Metamath .mm statements.
Modifier and Type | Field and Description |
---|---|
static java.util.Comparator<TheoremStmtGroup> |
NBR_LOG_HYP_SEQ
NBR_LOG_HYP_SEQ sequences by number of LogHyps and Seq.
|
static java.util.Comparator<TheoremStmtGroup> |
SEQ
SEQ sequences by TheoremStmtGroup.theorem.getSeq().
|
Constructor and Description |
---|
TheoremStmtGroup(MMTTheoremFile mmtTheoremFile,
LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Constructor for TheoremStmtGroup.
|
Modifier and Type | Method and Description |
---|---|
int |
compareTo(java.lang.Object obj)
Compares TheoremStmtGroup object based on the label.
|
boolean |
equals(java.lang.Object obj) |
int[] |
getAssignedLogHypSeq()
Returns the assigned sequence number array for new Logical Hypotheses.
|
int |
getAssignedTheoremSeq()
Returns the assigned sequence number for a new Theorem.
|
int |
getInsertSectionNbr()
Gets the BookManager insertSectionNbr for the theorem.
|
boolean |
getIsTheoremNew()
Gets the isTheoremNew flag.
|
LogHyp[] |
getLogHypArray()
Gets the LogHyp array which may contain nulls if the Theorem is new and
has not yet been stored in the Logical System.
|
java.lang.String |
getSourceFileName()
Returns the MMTTheoremFile absolute pathname.
|
Theorem |
getTheorem()
Gets the Theorem object or null if the theorem is new and has not yet
been stored in the Logical System.
|
java.lang.String |
getTheoremLabel()
Gets the theorem label.
|
boolean[] |
getWasLogHypAppendedArray()
Gets the wasLogHypAppended flag array.
|
boolean[] |
getWasLogHypInsertedArray()
Gets the wasLogHypInserted flag array.
|
boolean |
getWasTheoremAppended()
Gets the wasTheoremAppended flag.
|
boolean |
getWasTheoremInserted()
Gets the wasTheoremInserted flag.
|
boolean |
getWasTheoremUpdated()
Gets the wasTheoremUpdated flag.
|
int |
hashCode() |
void |
initializeMustAppend()
Initializes the mustAppend flag for the TheoremStmtGroup.
|
void |
queueDependentsForUpdate(java.util.Deque<TheoremStmtGroup> readyQueue,
java.util.List<TheoremStmtGroup> waitingList)
Requeues every MMT Theorem which uses this theorem.
|
void |
queueForUpdates(java.util.Queue<TheoremStmtGroup> readyQueue,
java.util.List<TheoremStmtGroup> waitingList)
Queues the theorem into either the ready list or the waiting list.
|
void |
reverseStmtTblUpdates(java.util.Map<java.lang.String,Stmt> stmtTbl)
Backs out the updates made into the Logical System.
|
java.lang.String |
toString()
Converts TheoremStmtGroup to String.
|
void |
updateLogicalSystem(LogicalSystem logicalSystem,
Messages messages,
TlPreferences tlPreferences)
Adds or updates the LogicalSystem with the MMT Theorem and if the Logical
System has a Proof Verifier it runs the Metamath Proof Verification
algorithm.
|
void |
validateTheoremSrcStmtProofLabels(LogicalSystem logicalSystem,
java.util.Map<java.lang.String,TheoremStmtGroup> theoremStmtGroupTbl)
Validates the labels used in the TheoremStmtGroup proof.
|
public static final java.util.Comparator<TheoremStmtGroup> SEQ
public static final java.util.Comparator<TheoremStmtGroup> NBR_LOG_HYP_SEQ
public TheoremStmtGroup(MMTTheoremFile mmtTheoremFile, LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException
The constructor loads the input file into the TheoremStmtGroup and performs data validation of the input data.
mmtTheoremFile
- MMTTheoremFile to be read.logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- is thrown if there are data errors in the
input MMTTheoremFile.public void initializeMustAppend()
The initial (default) setting of mustAppend is false unless the theorem is new and has an incomplete proof.
public void validateTheoremSrcStmtProofLabels(LogicalSystem logicalSystem, java.util.Map<java.lang.String,TheoremStmtGroup> theoremStmtGroupTbl) throws TheoremLoaderException
During processing the highest sequence number referred to is updated,
Also, isProofIncomplete is set to true if a "?" is found in the proof.
And, two key lists about which theorems are used are updated:
theoremStmtGroupUsedList
and usedByTheoremStmtGroupList
.
These lists are the basis for determining the order in which theorems are
loaded into the Logical System.
logicalSystem
- LogicalSystem object.theoremStmtGroupTbl
- the MMTTheoremSet Map containing the MMT
Theorems in the set.TheoremLoaderException
- is thrown if there are data errors in the
input MMTTheoremFile.public void queueForUpdates(java.util.Queue<TheoremStmtGroup> readyQueue, java.util.List<TheoremStmtGroup> waitingList)
If the theorem's theoremStmtGroupUsedList is empty then it is ready to update because it doesn't refer to any other theorems in the MMTTheoremSet. Otherwise it goes into the waiting list. (When a theorem is stored into the LogicalSystem it is removed from the theoremStmtGroupUsedList of each theorem which refers to it.)
readyQueue
- queue of MMTTheorems ready for updating into the
LogicalSystem.waitingList
- list of MMTTheorems which are not yet ready to update
into the LogicalSystem.public void queueDependentsForUpdate(java.util.Deque<TheoremStmtGroup> readyQueue, java.util.List<TheoremStmtGroup> waitingList) throws TheoremLoaderException
When a theorem is stored into the LogicalSystem it is removed from the theoremStmtGroupUsedList of each theorem which refers to it. To determine which theorems need requeueing, the updated theorem's usedByTheoremStmtGroup list is read and each theorem in that list is requeued.
readyQueue
- queue of MMTTheorems ready for updating into the
LogicalSystem.waitingList
- list of MMTTheorems which are not yet ready to update
into the LogicalSystem.TheoremLoaderException
- if a data error is discovered resulting
from the theorem update.public void updateLogicalSystem(LogicalSystem logicalSystem, Messages messages, TlPreferences tlPreferences) throws TheoremLoaderException, LangException
Note: a proof verification error does not trigger a TheoremLoaderException, which would thus halt the update of the entire MMTTheoremSet. Instead, any proof verification errors are stored in the Messages object for later display.
When a theorem is stored into the LogicalSystem it is removed from the theoremStmtGroupUsedList of each theorem which refers to it. To determine which theorems need requeueing, the updated theorem's usedByTheoremStmtGroup list is read and each theorem in that list is requeued.
logicalSystem
- LogicalSystem object.messages
- Messages object.tlPreferences
- TlPreferences object.TheoremLoaderException
- if a data error is discovered.LangException
- if a data error is discovered.public void reverseStmtTblUpdates(java.util.Map<java.lang.String,Stmt> stmtTbl)
If the theorem is new, it and its logical hypotheses are removed from the Logical System's statement table.
If the theorem was updated then the previous value of the theorem's proof and its $d restrictions are restored.
stmtTbl
- the LogicalSystem object's stmtTbl.public boolean getIsTheoremNew()
public java.lang.String getTheoremLabel()
public java.lang.String getSourceFileName()
public boolean getWasTheoremUpdated()
public boolean getWasTheoremInserted()
public boolean getWasTheoremAppended()
public Theorem getTheorem()
public boolean[] getWasLogHypInsertedArray()
public boolean[] getWasLogHypAppendedArray()
public LogHyp[] getLogHypArray()
public int getInsertSectionNbr()
public int[] getAssignedLogHypSeq()
public int getAssignedTheoremSeq()
public java.lang.String toString()
toString
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public int compareTo(java.lang.Object obj)
obj
- TheoremStmtGroup object to compare to this TheoremStmtGrouppublic boolean equals(java.lang.Object obj)
equals
in class java.lang.Object