public class ScopeFrame
extends java.lang.Object
mandFrame
, the Mandatory "Frame" of an
Assrt (assertion), as well as optFrame
, the Optional "Frame" of a
Theorem (OptFrame not present in other Assrt's).
Add mandFrame
to optFrame
and you have a Metamath "Extended
Frame".
Modifier and Type | Field and Description |
---|---|
DjVars[] |
djVarsArray
These are the disjoint variable (pair)restrictions, if any, that apply to
the Assrt and any of its proof steps.
|
Hyp[] |
hypArray
These are the "mandatories" that are referenced in an assertion, in order
of appearance in the database.
|
Constructor and Description |
---|
ScopeFrame()
Default Constructor.
|
ScopeFrame(ScopeDef scopeDef,
int maxSeq)
Builds a Frame using a ScopeDef and an array of Distinct Variables,
limited by an input maximum sequence number.
|
ScopeFrame(ScopeFrame mandFrame,
ScopeFrame optFrame)
Builds a composite ("combo") Frame using a MandFrame plus an OptFrame,
augmented by additional $d specifications.
|
Modifier and Type | Method and Description |
---|---|
void |
addDjVarGroups(Var[][] dvGroupArray)
Accumulates an array of DvGroups into the djVarsArray.
|
boolean |
areBothDjVarsInHypArray(DjVars djVars)
Checks to see whether or not both variables in a DjVars pair are
referenced in the MandFrame's array of hypotheses.
|
static DjVars[] |
buildConsolidatedDvArray(DistinctVariablesStmt[] distinctVariablesStmtArray)
Converts an array of ProofWorksheet DistinctVariablesStmt objects into an
array of DjVars objects.
|
static java.util.List<java.util.List<Var>> |
consolidateDvGroups(DjVars[] dvArray)
Attempts to do a good job consolidating pairs of disjoint variables into
groups of three or more.
|
java.util.Map<java.lang.String,Var> |
getVarMap()
Builds and returns Var HashMap derived from the MandFrame hypArray.
|
static boolean |
isVarPairInDjArray(ScopeFrame frame,
Var vLo,
Var vHi)
Checks to see if a certain pair of variables is mentioned in a OptFrame's
DjVars array.
|
static void |
loadDvGroupsIntoList(java.util.List<DjVars> arrayList,
Var[][] dvGroupArray)
Accumulates new Distinct Variables into an List of DjVars pairs.
|
public Hyp[] hypArray
For a Theorem these include not only the variable hypotheses for variables referenced in the assertion's Formula, but the logical hypotheses in scope of the Theorem plus the variable hypotheses for variables referenced by *those* logical hypotheses.
For an optFrame
, these include all Hyps in scope not present in
the mandatory hypArray
.
public DjVars[] djVarsArray
For an optFrame
, these include all DjVars (pairs) in scope not
present in the mandatory djVarsArray
.
public ScopeFrame()
public ScopeFrame(ScopeDef scopeDef, int maxSeq)
scopeDef
- ScopeDef, intended to be global scope.maxSeq
- MObj.seq must be < maxSeqpublic ScopeFrame(ScopeFrame mandFrame, ScopeFrame optFrame)
mandFrame
- a Theorem's MandFrameoptFrame
- a Theorem's OptFramepublic static boolean isVarPairInDjArray(ScopeFrame frame, Var vLo, Var vHi)
Note: vLo and vHi are automatically switched if vLo is not low.
Note: this function is the reason that DjVars vars are stored as "lo" and "hi". Low and High are irrelevant to the mathematics of this situation. But if the vars were stored randomly or arbitrarily, then twice as many comparisons would be needed here.
frame
- Scope Frame to inspect.vLo
- the "low" variable in the pair.vHi
- the "high" variable in the pair.public static DjVars[] buildConsolidatedDvArray(DistinctVariablesStmt[] distinctVariablesStmtArray)
distinctVariablesStmtArray
- array of DistinctVariablesStmt object.public static void loadDvGroupsIntoList(java.util.List<DjVars> arrayList, Var[][] dvGroupArray)
arrayList
- list of DjVars objectsdvGroupArray
- array of Var[] arrays.public static java.util.List<java.util.List<Var>> consolidateDvGroups(DjVars[] dvArray)
The input dvArray is assumed to be in ascending order according to DjVars.compareTo. We assume AND require that it be free from duplicates. Here is an example of dvArray -- sorted and with no duplicates:
[(a,b),(a,c),(a,d),(b,c),(b,d),(b,e),(c,d),(c,f)]The output List contains an ordered set of Lists of disjoint variables, sorted by the first Var character string in the list. Here is sample output for the example above:
[ [a,b,c,d], [b,e], [c,f] ]The algorithm should be capable of consolidating $d's into [ [a,x,y,z], [b,x,y,z] ], as well as [ [x,y,z,a], [x,y,z,b] ].
Note that within a DjVars object. varLo and varHi are loaded by Var.Id. Thus, for disjoint vars "a" and "b", varLo = a, and varHi = b. Also, varLo is never equal to varHi.
dvArray
- the input list of DjVarspublic boolean areBothDjVarsInHypArray(DjVars djVars)
Note: checks only the VarHyp's.
djVars
- -- DjVars object containing 2 variables to be checked
against the variables referenced in the MandFrame hypArray.public void addDjVarGroups(Var[][] dvGroupArray)
FYI, a DvGroup is an array of at least 2 variables which are by definition supposed to be distinct from each other. So [ph th ch] is a DvGroup which could be obtained from a $d statement like "$d ph th ch $."
dvGroupArray
- array of array of disjoint variables.public java.util.Map<java.lang.String,Var> getVarMap()