public class DjVars extends java.lang.Object implements java.lang.Comparable<DjVars>
Modifier and Type | Field and Description |
---|---|
static java.util.Comparator<? super Var> |
DV_LEX
This is a plain ASCII sort of the variables, for use when the active var
hyp field is not reliable.
|
static java.util.Comparator<? super Var> |
DV_ORDER
This is the ordering that will be used to determine which variable in a
DjVars is "hi" and which is "lo", and is visible to the user as the
ordering of variables in missing $d statmements generated by the program.
|
Constructor and Description |
---|
DjVars(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String loS,
java.lang.String hiS)
Construct using two Var id Strings.
|
DjVars(Var lo,
Var hi)
Construct using two Var's.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
areBothDjVarsInExtendedFrame(DjVars djVars,
ScopeFrame mandFrame,
ScopeFrame optFrame)
Helper routine for Theorem Loader to confirm that both DjVars variables
are in the Extended Frame of a theorem.
|
static java.util.List<java.lang.StringBuilder> |
buildMetamathDjVarsStatementList(DistinctVariablesStmt[] distinctVariablesStmtArray)
Builds a LinkedList of StringBuilders containing the Metamath formatted
text $d statements for the theorem.
|
static java.util.List<java.lang.StringBuilder> |
buildMetamathDjVarsStatementList(Theorem theorem)
Builds a LinkedList of StringBuilders containing the Metamath format text
$d statements for the theorem.
|
int |
compareTo(DjVars obj)
Compares DjVars object based on the variables.
|
static java.util.List<java.lang.StringBuilder> |
convertDvGroupsListToMetamathList(java.util.List<java.util.List<Var>> comboDvGroups)
Converts a ArrayList of Lists containing distinct variables into a
LinkedList of StringBuilders containing Metamath format text $d
statements.
|
boolean |
equals(java.lang.Object obj) |
Var |
getVarHi()
Return the "high" Dj Var, varHi.
|
Var |
getVarLo()
Return the "low" Dj Var, varLo.
|
int |
hashCode() |
static boolean |
isDjVarsVarInExtendedFrame(Var djVarsVar,
ScopeFrame mandFrame,
ScopeFrame optFrame)
Helper routine for Proof Assistant to confirm that a DjVars variable is
defined in the Theorem's Extended Frame.
|
void |
set(Var lo,
Var hi)
Set the contents of this DjVars object.
|
static DjVars[] |
sortAndCombineDvArrays(DjVars[] array1,
DjVars[] array2)
Merges two arrays of DjVars returning a single array in ascending
compareTo order with duplicates eliminated.
|
static DjVars[] |
sortAndCombineDvListOfLists(java.util.List<java.util.List<DjVars>> list1)
Merges lists of lists of DjVars returning a single array in ascending
compareTo order with duplicates eliminated.
|
java.lang.String |
toString()
Converts DjVars to String.
|
public static java.util.Comparator<? super Var> DV_ORDER
public static java.util.Comparator<? super Var> DV_LEX
public DjVars(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String loS, java.lang.String hiS) throws LangException
symTbl
- Symbol Table (Map)loS
- Var1 id String.hiS
- Var2 id String.LangException
- if the two Var id's are identical, or are not
defined and active vars.public DjVars(Var lo, Var hi) throws LangException
lo
- Var 1.hi
- Var 2.LangException
- if the two Var id's are identical.public static boolean areBothDjVarsInExtendedFrame(DjVars djVars, ScopeFrame mandFrame, ScopeFrame optFrame)
djVars
- DjVars object to check.mandFrame
- Mandatory Frame from a Theorem.optFrame
- Optional Frame from a Theorem.public static boolean isDjVarsVarInExtendedFrame(Var djVarsVar, ScopeFrame mandFrame, ScopeFrame optFrame)
djVarsVar
- variable object to check.mandFrame
- Mandatory Frame from a Theorem.optFrame
- Optional Frame from a Theorem.public static java.util.List<java.lang.StringBuilder> buildMetamathDjVarsStatementList(DistinctVariablesStmt[] distinctVariablesStmtArray)
The input DistinctVariablesStmt array objects are consolidated to remove duplicates, sorted and then merged to create a concise set of $d statements.
distinctVariablesStmtArray
- array of Proof Worksheet
DistinctVariablesStmt objects.public static java.util.List<java.lang.StringBuilder> buildMetamathDjVarsStatementList(Theorem theorem)
theorem
- the theorem for which $d statements are needed.public static java.util.List<java.lang.StringBuilder> convertDvGroupsListToMetamathList(java.util.List<java.util.List<Var>> comboDvGroups)
comboDvGroups
- List of Lists containing distinct variables.public static DjVars[] sortAndCombineDvArrays(DjVars[] array1, DjVars[] array2)
array1
- 1st array of DjVars objects, may be null.array2
- 2nd array of DjVars objects, may be null.public static DjVars[] sortAndCombineDvListOfLists(java.util.List<java.util.List<DjVars>> list1)
list1
- List containing List elements of DjVars objects.public void set(Var lo, Var hi) throws LangException
lo
- Var 1.hi
- Var 2.LangException
- if the two Var id's are identical.public Var getVarLo()
public Var getVarHi()
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)
equals
in class java.lang.Object
public int compareTo(DjVars obj)
compareTo
in interface java.lang.Comparable<DjVars>
obj
- Order object to compare to this Order