public class WorkVarManager
extends java.lang.Object
Constructor and Description |
---|
WorkVarManager(Grammar grammar)
Sole constructor for WorkVarManager.
|
Modifier and Type | Method and Description |
---|---|
WorkVar |
alloc(Cnst typ)
Allocates a new WorkVar for the input Type Code.
|
WorkVar |
alloc(java.lang.String workVarIn)
Allocates the WorkVar specified by the input token if necessary assuming
it is a valid WorkVar token string.
|
WorkVar |
alloc(WorkVar workVar)
Allocates a given WorkVar.
|
WorkVarHyp |
allocWorkVarHyp(Cnst typ)
Allocates a new WorkVar for the input Type Code and returns the
corresponding WorkVarHyp.
|
boolean |
areWorkVarsDeclared()
Returns true if the Work Variables have been declared.
|
void |
dealloc(WorkVar workVar)
Deallocates a WorkVar.
|
void |
dealloc(WorkVarHyp workVarHyp)
Deallocates a WorkVar given a WorkVarHyp
|
void |
deallocAll()
Deallocates all Work Variables.
|
void |
deallocAndReallocAll(ProofWorksheet w) |
void |
declareWorkVars(Grammar grammar,
LogicalSystem logicalSystem)
Declare the Work Variables that have been defined.
|
void |
defineWorkVarType(Grammar grammar,
java.lang.String grammaticalTypCdIn,
java.lang.String workVarPrefixIn,
int nbrWorkVarsIn)
Define the Work Variables to be used for a given grammatical type code.
|
Cnst |
editGrammaticalTypCd(Grammar grammar,
java.lang.String grammaticalTypCdIn)
Validates an input string as being a valid Type Code for Work Variables.
|
java.lang.Integer |
editNbrWorkVars(int nbrWorkVarsIn)
Validates an input string specifying the number of WorkVar objects to be
declared for a specific Type Code.
|
java.lang.String |
editWorkVarPrefix(java.lang.String workVarPrefixIn)
Validates an input string as being a valid WorkVar Prefix.
|
boolean |
isAllocated(WorkVar workVar)
Returns true if input Work Var is allocated.
|
void |
resolveWorkVarUpdates()
Deallocates Work Vars that have updates and eliminates chains of WorkVar
updates so that a Work Var update subtree contains only non-updated Work
Vars.
|
void |
setPrevAllocNbr(Cnst typ,
int prevAllocNbr)
Sets the value of prevAllocIndex for a Type Code.
|
public WorkVarManager(Grammar grammar)
Does nothing except allocate the Arraylists to hold input definitions. Note therefore that the WorkVarManager object is not ready for use by ProofAsst or elsewhere until the Work Variables are actually declared, and a NullPointerException will result if access is attempted before then.
grammar
- Grammar object for loaded .mm file.public boolean areWorkVarsDeclared()
If no Work Variable definitions are input and the Proof Assistant is instantiated prior to declaration of Work Variables, ProofAsstBoss.java will declare the Work Variables using the default definitions. Which is why we need this function...
public void defineWorkVarType(Grammar grammar, java.lang.String grammaticalTypCdIn, java.lang.String workVarPrefixIn, int nbrWorkVarsIn) throws VerifyException
The definitions are stored separately from the tables constructed by "Declare". This allows mixing of definitions and default values for Work Variables.
grammar
- Grammar object for loaded .mm file.grammaticalTypCdIn
- String holding the Cnst used as a Type Code
(e.g. "wff").workVarPrefixIn
- String holding the prefix to be used with a
numeric suffix to name Work Variables of a given Type.nbrWorkVarsIn
- number of Work Variables to declare for this Type
Code.VerifyException
- if individual field values are invalid.public void declareWorkVars(Grammar grammar, LogicalSystem logicalSystem) throws VerifyException
The input definitions and default values for each grammatical Type Code are used to create the Work Variable objects and finalize the WorkVarManager object for actual use.
Note that final validation checks are performed to ensure that there are no duplicate Var or VarHyp names, either among the Work Variable objects or the other symbols and statements defined in the LogicalSystem for the input .mm file. This means checking for duplicate Work Var prefixes as well as checking each WorkVar and WorkVarHyp name against the LogicalSystem's Symbol and Statement tables.
grammar
- Grammar object for loaded .mm file.logicalSystem
- LogicalSystem for loaded .mm file.VerifyException
- if duplicate Var or VarHyp names result or if
there is a conflict with the Symbol and Statement table
namespaces.public Cnst editGrammaticalTypCd(Grammar grammar, java.lang.String grammaticalTypCdIn) throws VerifyException
grammar
- Grammar object for loaded .mm file.grammaticalTypCdIn
- String Type Code (Cnst)VerifyException
- if input Type Code invalid.public java.lang.String editWorkVarPrefix(java.lang.String workVarPrefixIn) throws VerifyException
Duplicate checking is not done here, just checking to make sure that the input prefix characters are valid Metamath "math symbols".
workVarPrefixIn
- String of Metamath math symbols.VerifyException
- if workVarPrefixIn has non math symbols or is
null or empty.public java.lang.Integer editNbrWorkVars(int nbrWorkVarsIn) throws VerifyException
Basically this is just a range check: greater than some number (9) and less than some other number (999).
nbrWorkVarsIn
- Number of WorkVar objects for a given Type Code.VerifyException
- if nbrWorkVarsIn out of range.public boolean isAllocated(WorkVar workVar)
Note: this is a weird function, since how could an unallocated WorkVar be
input to see whether or not it is allocates? BUT... consult
StepUnifier.finalizeAndLoadAssrtSubst()
for explanatory
remarks...
workVar
- the Work Var to checkpublic void resolveWorkVarUpdates()
Processing is by Type Code, in reverse order by Work Var number within Type Code so that subsequent alloc() calls begin with the lowest deallocated Work Var numbers.
Example: WorkVar "A" where = B and B = C results in update clone of A.paSubst: A = C.
public WorkVar alloc(java.lang.String workVarIn)
If the WorkVar is already allocated it just returns the WorkVar instance.
The input String must consist of a prefix which matches one of the specified WorkVar prefixes, followed by a positive integer within the range of WorkVar numbers specified for the Type Code corresponding to the prefix.
workVarIn
- token specifying a WorkVar (id)java.lang.IllegalArgumentException
- if workVarIn is null or an empty String.public WorkVar alloc(WorkVar workVar)
It is hard to envision using this function...
workVar
- to be allocated.public WorkVarHyp allocWorkVarHyp(Cnst typ) throws VerifyException
typ
- Cnst Type Code of WorkVar to be allocated.VerifyException
- if no remaining WorkVar objects are available for
use with the given Type Code.public WorkVar alloc(Cnst typ) throws VerifyException
typ
- Cnst Type Code of WorkVar to be allocated.VerifyException
- if no remaining WorkVar objects are available for
use with the given Type Code.public void deallocAndReallocAll(ProofWorksheet w)
public void deallocAll()
public void dealloc(WorkVarHyp workVarHyp)
workVarHyp
- workVarHyp to be deallocated.public void dealloc(WorkVar workVar)
workVar
- to be deallocated.public void setPrevAllocNbr(Cnst typ, int prevAllocNbr)
In other words, if we input '1' for &W1, then the next allocation will be &W2.
If the input prevAllocNbr is invalid a default setting of zero is used instead.
typ
- Cnst Type Code of prevAllocIndex to set.prevAllocNbr
- is one greater than prevAllocIndex