public abstract class MObj
extends java.lang.Object
Originally coded without a common root, but eventually bowed to the inevitable. The ability to hold an array/collection of Syms and Stmts is helpful, and eventually may become an absolute necessity -- if and when a LogicalSystem can be output, we will need to store Begin and End Scope statements, and perhaps Include Files and Comments.
Modifier and Type | Field and Description |
---|---|
protected int |
chapterNbr
chapterNbr assigned by BookManager which is optionally enabled.
|
protected java.lang.String |
description
description is derived from Metamath comments (initially...
|
protected boolean |
isTempObject
isTempObject flag denotes a dummy or temporary object that is not stored
in the Sym table or Stmt table and has the lifespan of a single
transaction.
|
static java.util.Comparator<MObj> |
SECTION_AND_MOBJ_NBR
SECTION_AND_MOBJ_NBR sequences by sectionNbr and sectionMObjNbr;
|
protected int |
sectionMObjNbr
sectionMObjNbr is assigned by BookManager which is optionally enabled.
|
protected int |
sectionNbr
sectionNbr assigned by BookManager which is optionally enabled.
|
protected int |
seq
Provides an ordering of Metamath objects.
|
static java.util.Comparator<MObj> |
SEQ
SEQ sequences by MObj.seq.
|
Modifier | Constructor and Description |
---|---|
protected |
MObj(int inSeq)
Construct MObj with sequence number.
|
Modifier and Type | Method and Description |
---|---|
boolean |
equals(java.lang.Object obj)
Compare for equality with another MObj.
|
int |
getChapterNbr()
Return chapterNbr;
|
java.lang.String |
getDescription()
Returns description text derived from Metamath comments.
|
java.lang.String |
getDescriptionForSearch() |
boolean |
getIsTempObject()
Returns tempObject boolean.
|
int |
getOrigSectionNbr() |
int |
getSectionMObjNbr()
Return sectionMObjNbr;
|
int |
getSectionNbr()
Return sectionNbr;
|
int |
getSeq()
Note: an extensive set of tests showed that direct access to .seq is an
infintesimal bit faster than getSeq() :) So public access to MObj.seq was
revoked!
|
int |
hashCode()
Computes hashcode for this MObj
|
void |
setChapterNbr(int chapterNbr)
Updates chapterNbr;
|
void |
setDescription(java.lang.String description) |
void |
setIsTempObject(boolean isTempObject)
Sets tempObject boolean value.
|
void |
setSectionMObjNbr(int sectionMObjNbr)
Updates sectionMObjNbr;
|
void |
setSectionNbr(int sectionNbr)
Updates sectionNbr;
|
java.lang.String |
toString()
Converts to MObj to String.
|
protected final int seq
The concept of database sequence is key for Metamath. Statements can only refer to statements previously defined -- no forward references and no self references are allowed. Also, the sequence of hypotheses is by MObj.seq, as is the ordering of items on the Proof Work Stack.
Metamath allows variables to be "active" or "inactive", based on the
scope level in which they are referenced by VarHyp
s. This allows
for an unlimited number of VarHyp
s with a limited set of of
Var
s, but it complicates things elsewhere! Even the grammatical
parser has to deal with non-terminal symbols that change depending on
context (@see mmj.verify.Grammar).
protected boolean isTempObject
protected java.lang.String description
protected int chapterNbr
chapterNbr is zero if the MObj has not been assigned to a Chapter. Chapter numbers are assigned from 1 by 1 within the set of loaded Metamath input files (see mmj.lang.BookManager.java for more info.)
protected int sectionNbr
sectionNbr is zero if the MObj has not been assigned to a Section. Section numbers are assigned from 1 by 1, and correspond to "sub-sections" in a Metamath input file (see set.mm), except that each input Metamath "sub-section" is broken down into 4 mmj2 Sections: 1: Sym (Cnst and Var), 2: VarHyp, 3: Syntax and 4: Logic (logic includes logic axioms, theorems and logical hypotheses). These categories are assigned in sequence so that a "logic" section number is therefore always divisible by 4, syntax by 3, and so on (see mmj.lang.BookManager.java for more info.)
protected int sectionMObjNbr
sectionMObjNbr is zero if the MObj has not been assigned to a Section. sectionMObj numbers are assigned from 1 by 1 within Section (see mmj.lang.BookManager.java for more info.)
public static final java.util.Comparator<MObj> SEQ
public static final java.util.Comparator<MObj> SECTION_AND_MOBJ_NBR
protected MObj(int inSeq)
inSeq
- the sequence numberpublic int getSeq()
public boolean getIsTempObject()
public void setIsTempObject(boolean isTempObject)
isTempObject
- boolean flag denoting dummy/temp objects.public java.lang.String toString()
toString
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object obj)
Equal if and only if the MObj sequence numbers are equal. and the obj to be compared to this object is not null and is a MObj as well.
equals
in class java.lang.Object
public java.lang.String getDescription()
This contains the complete Metamath comment statement except for the $( and $) delimiter tokens.
public java.lang.String getDescriptionForSearch()
public void setDescription(java.lang.String description)
public int getChapterNbr()
public void setChapterNbr(int chapterNbr)
chapterNbr
- for the MObj.public int getOrigSectionNbr()
public int getSectionNbr()
public void setSectionNbr(int sectionNbr)
sectionNbr
- for the MObj.public int getSectionMObjNbr()
public void setSectionMObjNbr(int sectionMObjNbr)
sectionMObjNbr
- for the MObj.