public class Formula
extends java.lang.Object
Sub-Classes of Formula exist: VarHypFormula and LogicFormula but their function is basically just to simplify certain coding in VarHyp, LogHyp, etc. In theory, the distinction would be useful for creating default exprRPN's.
Formula: contains Cnst in sym[0], followed by the formula's "expression", which consists of zero or more Cnst's and Var's in sym[1]...sym[cnt - 1].
Formula Factoids:
Modifier | Constructor and Description |
---|---|
|
Formula(java.util.Collection<Sym> symList)
Construct using Sym List.
|
|
Formula(int workCnt,
Sym[] workFormula)
Construct using cnt and Sym array.
|
protected |
Formula(java.util.Map<java.lang.String,Sym> symTbl,
int sz,
java.lang.String typS)
Construct Formula of given size and Type.
|
|
Formula(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String typS,
java.util.List<java.lang.String> symList,
java.util.List<Hyp> hypList)
Construct using String Type Code and Sym List.
|
Modifier and Type | Method and Description |
---|---|
static <T extends Hyp> |
accumHypInList(java.util.List<T> hypList,
T hypNew)
Accumulate unique hypotheses (no duplicates), storing them in an array
list in order of their appearance in the database.
|
VarHyp[] |
buildMandVarHypArray(Hyp[] tempHypArray)
Uses an array of Hyps to build an array of VarHyps containing only the
VarHyps needed for the variables actually used in the Formula.
|
Cnst[] |
buildRuleFormatExpr(VarHyp[] varHypArray)
Builds a "rule format" version of the Formula's Expression.
|
void |
collectConstFrequenceAndInitConstList(java.util.Map<Cnst,java.lang.Integer> frequency)
This function should be used to collect frequency statistic for some
metamath library and create an array of constant symbols.
|
int |
computeWidthOfWidestExprCnst()
Computes the width in characters of the widest Cnst in the Formula's
Expression.
|
static Formula |
constructTempDummyFormula(Cnst typ,
java.lang.String dummySym)
Construct a temporary dummy Formula for transient use.
|
boolean |
equals(java.lang.Object obj)
Compare for equality with another Formula.
|
boolean |
exprEquals(java.lang.Object obj)
Compare Expression for equality with another Formula's expr (don't
compare Type Codes, in other words).
|
java.lang.String |
exprToString()
Computes a character string version of the expression portion of the
formula.
|
int |
getCnt() |
Sym[] |
getExpr() |
ParseNodeHolder[] |
getParseNodeHolderExpr(Hyp[] hypArray)
Builds a "custom" version of an Expression in which an array of
ParseNodeHolders is output for use in generating a ParseTree.
|
ParseNodeHolder[] |
getParseNodeHolderExpr(VarHyp[] varHypArray)
Builds a "custom" version of an Expression in which an array of
ParseNodeHolders is output for use in generating a ParseTree.
|
Sym[] |
getSym() |
Cnst |
getTyp()
Return Formula Type Code.
|
Var |
getVarHypVar()
Return the Formula's Var (sym[1]), assuming this is a VarHyp formula.
|
int |
hashCode()
Computes hashcode for this Formula.
|
boolean |
preunificationCheck(Formula other)
This function is needed to exclude quickly the incompatible with this
formulas.
|
void |
setTyp(Cnst typ)
Set Formula Type Code.
|
Sym |
setTyp(java.util.Map<java.lang.String,Sym> symTbl,
java.lang.String typS)
Set Formula Type Code.
|
void |
sortConstList(java.util.Comparator<Cnst> comp)
When the frequency information has been collected this function should be
used in order to sort the constant symbols array
|
boolean |
srcStmtEquals(SrcStmt srcStmt)
Compare SrcStmt typ and symList to Formula.
|
int |
toProofWorksheetStringBuilder(java.lang.StringBuilder sb,
int leftColContinuation,
int marginRight)
Formats formula symbol strings into a column of characters within a text
area.
|
java.lang.String |
toString()
Computes a character string version of Formula for printing.
|
java.lang.StringBuilder |
toStringBuilderLineList(java.util.List<java.lang.StringBuilder> list,
java.lang.StringBuilder sb,
int leftColContinuation,
int marginRight,
java.lang.String endToken)
Formats formula into StringBuilder lines in a List.
|
public Formula(int workCnt, Sym[] workFormula)
workCnt
- the correct length of the formula.workFormula
- the formula's Sym array.public Formula(java.util.Collection<Sym> symList)
symList
- List containing formula symbolsprotected Formula(java.util.Map<java.lang.String,Sym> symTbl, int sz, java.lang.String typS) throws LangException
symTbl
- Symbol Table (Map)sz
- Size of the formulatypS
- Formula Type codeLangException
- if an error occurredpublic Formula(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String typS, java.util.List<java.lang.String> symList, java.util.List<Hyp> hypList) throws LangException
Verifies that each Sym id in Expression is active and accumulates the matching VarHyp's in the input exprHypList param.
symTbl
- Map containing Cnst and Var definitions.typS
- Formula Type Code String.symList
- expression's symbol character stringshypList
- List of Hyp's. Is updated with unique variable hypotheses
in the expression. Because the list is maintained in database
statement sequence order, hypList should either be empty (new)
before the call, or already be in that order (see
accumHypInList
.LangException
- if duplicate symbol, etc. (see
mmj.lang.LangConstants.java
)public static Formula constructTempDummyFormula(Cnst typ, java.lang.String dummySym) throws LangException
typ
- is the Formula's TypCd Cnst.dummySym
- a string of characters that should not have non-printable
characters or whitespace (else renderFormula may come out
wrong!)LangException
- if dummySym is emptypublic void collectConstFrequenceAndInitConstList(java.util.Map<Cnst,java.lang.Integer> frequency)
frequency
- the map from constant to its frequency in the metamath
librarypublic void sortConstList(java.util.Comparator<Cnst> comp)
comp
- the comparatorpublic boolean preunificationCheck(Formula other)
other
- the other formula which should be checked for constant set
inclusionpublic Cnst getTyp()
public void setTyp(Cnst typ)
typ
- Formula Type Code (sym[0]).public Sym[] getExpr()
public int getCnt()
public Sym[] getSym()
public Var getVarHypVar()
public Sym setTyp(java.util.Map<java.lang.String,Sym> symTbl, java.lang.String typS) throws LangException
symTbl
- Symbol Table (Map).typS
- Type Code String identifying a Cnst.LangException
- if Type Code is undefined or not defined as a Cnst.public ParseNodeHolder[] getParseNodeHolderExpr(VarHyp[] varHypArray)
The key fact about the output ParseNodeHolders is that a Cnst in the Formula Expression just goes into the holder's "mObj" -- it will not be part of the ParseTree and the ParseNode element is null.
On the other hand, Variables in the Formula's Expression are converted into ParseNodes with Stmt = the VarHyp; the ParseNodeHolder's "mObj" element is set to the VarHyp Stmt reference -- and this ParseNode will be part of the ultimate Parse Tree. In effect, we're "parsing" VarHyps and creating their output ParseNodes at this time.)
varHypArray
- Array of VarHyp for Formula.java.lang.IllegalArgumentException
- if unable to find a VarHyp for one of
the Formula's Var's.public ParseNodeHolder[] getParseNodeHolderExpr(Hyp[] hypArray)
hypArray
- Array of Hyp for Formula.java.lang.IllegalArgumentException
- if unable to find a VarHyp for one of
the Formula's Var's.public Cnst[] buildRuleFormatExpr(VarHyp[] varHypArray)
varHypArray
- Array of VarHyp for Formula.java.lang.IllegalArgumentException
- if unable to find a VarHyp for one of
the Formula's Var's.public VarHyp[] buildMandVarHypArray(Hyp[] tempHypArray)
Note: if the input array of Hyps does not contain all of the necessary VarHyps, an IllegalArgumentException is thrown! No mercy.
tempHypArray
- array of Hyp.java.lang.IllegalArgumentException
- if unable to find a VarHyp for one of
the Formula's Var's.public int hashCode()
hashCode
in class java.lang.Object
public boolean exprEquals(java.lang.Object obj)
Equal if and only if the Sym strings are equal. and the obj to be compared to this object is not null and is a Formula as well.
obj
- Formula whose Expression will be compared to this Formula's
Expression.public boolean srcStmtEquals(SrcStmt srcStmt)
srcStmt
- from mmj.mmio.Statementizer.java.public boolean equals(java.lang.Object obj)
Equal if and only if the Sym strings are equal. and the obj to be compared to this object is not null and is a Formula as well.
equals
in class java.lang.Object
obj
- Formula that will be compared to this Formula.public java.lang.String toString()
Note: LogicalSystem does not validate for "printable" characters in Sym, and output of certain non-printable characters can cause abrupt termination of DOS windows (though mmj.mmio does extensive validation, LogicalSystem itself is unconcerned about the contents of Sym id strings.)
toString
in class java.lang.Object
public java.lang.String exprToString()
Note: the "expression" here is the 2nd thru nth symbols of the formula -- that is, the type code at the start is discarded.
public int toProofWorksheetStringBuilder(java.lang.StringBuilder sb, int leftColContinuation, int marginRight)
sb
- StringBuilder to append to.leftColContinuation
- the leftmost column in the text area for use
by formulas.marginRight
- the rightmost column for use by formulas.public java.lang.StringBuilder toStringBuilderLineList(java.util.List<java.lang.StringBuilder> list, java.lang.StringBuilder sb, int leftColContinuation, int marginRight, java.lang.String endToken)
list
- list of StringBuilder lines.sb
- StringBuilder to append to.leftColContinuation
- the leftmost column in the text area for use
by formulas.marginRight
- the rightmost column for use by formulas.endToken
- string such as "$." or "$="public static <T extends Hyp> void accumHypInList(java.util.List<T> hypList, T hypNew)
T
- the actual type of the listhypList
- -- List of Hyp's. Is updated with unique variable
hypotheses in the expression. Because the list is maintained
in database statement sequence order, hypList should either be
empty (new) before the call, or already be in that order (see
accumHypInList
.hypNew
- candidate Hyp to be added to hypList if not already there.public int computeWidthOfWidestExprCnst()