public class Var extends Sym
A Metamath variable can be defined more than once if the $v statements occur within a Scope; outside of that scope the Var is "inactive" and cannot be referenced by subsequent Formula's. However, the "id" -- variable String -- cannot have been previously defined as that of a Cnst, and Cnst's must be defined in global scope. (In practice, Var's are defined globally because they have no meaning without a VarHyp -- a Var is just a "thing" with an identifying character String, just like a Cnst.)
Curiously, Var receives less coverage in mmj than Cnst. But perhaps that is
explained by the fact that to be used in a Formula's Expression, a Var must
not only be "active" (in scope), but there must be an active VarHyp for the
Var, assigning it a Type Code (and Type Codes are Cnst
s).
For convenience, a reference to the activeVarHyp for a Var is stored in var.
FYI, variables used in Syntax Axioms must be in "global scope", and they always have an activeVarHyp. mmj does not do anything with this factoid, but the potential exists to maintain a list of activeVarHyp's and Var's by Type Code... and the list would never be null for those Type Codes that are part of the grammar.
chapterNbr, description, isTempObject, SECTION_AND_MOBJ_NBR, sectionMObjNbr, sectionNbr, seq, SEQ
Modifier | Constructor and Description |
---|---|
|
Var(int seq,
java.util.Map<?,?> symTbl,
java.util.Map<?,?> stmtTbl,
java.lang.String id,
boolean active)
Construct using sequence number and id string.
|
protected |
Var(int seq,
java.lang.String id,
boolean active)
Construct using sequence number and id string.
|
Modifier and Type | Method and Description |
---|---|
void |
accumVarListBySeq(java.util.List<Var> varList)
Accumulate var (no duplicates), storing it in an array list in order of
appearance in the database.
|
boolean |
containedInVarListBySeq(java.util.List<Var> varList)
Searches for this Var in an ArrayList maintained in database input
sequence.
|
static Var |
declareVar(int seq,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
java.lang.String id)
Adds a new "active" Var to LogicalSystem.
|
VarHyp |
getActiveVarHyp()
Return the activeVarHyp for a Var.
|
VarHyp |
getVarHyp(Hyp[] hypArray)
Fetches the VarHyp for a Var given a Hyp array.
|
VarHyp |
getVarHyp(VarHyp[] varHypArray)
Fetches the VarHyp for a Var given an VarHyp array.
|
boolean |
isActive()
Is Sym active?
|
void |
setActive(boolean active)
Marks a Var as "active" or "inactive".
|
void |
setActiveVarHyp(VarHyp activeVarHyp)
Set the activeVarHyp for a Var (or null).
|
static Var |
verifyVarDef(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String varS)
Validates a variable's string (id) to make sure it is properly defined.
|
static Var |
verifyVarDefAndActive(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String varS)
Validates a variable's string (id) to make sure it is properly defined
and active.
|
getChapterNbr, getDescription, getDescriptionForSearch, getIsTempObject, getOrigSectionNbr, getSectionMObjNbr, getSectionNbr, getSeq, setChapterNbr, setDescription, setIsTempObject, setSectionMObjNbr, setSectionNbr
protected Var(int seq, java.lang.String id, boolean active) throws LangException
seq
- MObj.seq numberid
- Sym id stringactive
- true if this var is "active"LangException
- if id is emptypublic Var(int seq, java.util.Map<?,?> symTbl, java.util.Map<?,?> stmtTbl, java.lang.String id, boolean active) throws LangException
seq
- MObj.seq numbersymTbl
- Symbol TablestmtTbl
- Statement Tableid
- Sym id stringactive
- true if this var is "active"LangException
- if Sym.id duplicates the id of another Sym (Cnst or
Var).public static Var declareVar(int seq, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, java.lang.String id) throws LangException
If the Var does not already exist in symTbl, it is added, otherwise, the existing Var is returned.
If the Var symbol duplicates a Cnst symbol or if the Var is already "active", a LangException is thrown.
seq
- MObj.seq number (discarded if Var already exists.)symTbl
- Map containing all Sym
s.stmtTbl
- Map containing all Stmt
s.id
- String value (id) of the Var symbol.LangException
- if the Var symbol duplicates an existing Cnst
symbol or if the Var is already "active" -- or if the Var
symbol duplicates a Stmt label.public void setActive(boolean active)
active
- set Sym true
or false
.public boolean isActive()
Cnst
s are always active as they cannot be defined inside a scope
level, but a Var defined in a non-global scope level is "inactive"
outside of that scope.
The question "is Sym 'x' active" has relevance only in relation to a
Stmt: only "active" Sym
s can be used in a given Stmt
's
Formula.
public void setActiveVarHyp(VarHyp activeVarHyp)
For speed and convenience, an active Var maintains its current VarHyp; this saves having to do a difficult look-up :)
activeVarHyp
- or null.public VarHyp getActiveVarHyp()
For speed and convenience, an active Var maintains its current VarHyp; this saves having to do a difficult look-up :)
Var.activeVarHyp
(may be null).public VarHyp getVarHyp(VarHyp[] varHypArray)
A tedious little routine to help our friend Formula.
varHypArray
- array of VarHyp such as one would find in an Assrt or
LogHyp.Formula
public VarHyp getVarHyp(Hyp[] hypArray)
A tedious little routine to help our friend Formula.
hypArray
- array of Hyp such as one would find in a ScopeFrame.Formula
public static Var verifyVarDefAndActive(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String varS) throws LangException
If so, a reference to the existing Var is returned. Otherwise, LangException generated!
symTbl
- Map of already defined Sym
s.varS
- String identifying a variable.LangException
- thrown if variable is not defined, is defined as a
constant, or is not active.public static Var verifyVarDef(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String varS) throws LangException
If so, a reference to the existing Var is returned. Otherwise, LangException generated!
symTbl
- Map of already defined Sym
s.varS
- String identifying a variable.LangException
- thrown if variable is not defined, is defined as a
constant, or is not active.public void accumVarListBySeq(java.util.List<Var> varList)
Because varList is maintained in database statement sequence order, hypList should either be empty (new) before the call, or already be in that order.
varList
- List of Var's, updated here.public boolean containedInVarListBySeq(java.util.List<Var> varList)
varList
- List of Var's