public interface SyntaxVerifier
Refer to mmj.verify.GrammarConstants.java for information about parse parameters and error messages.
Modifier and Type | Method and Description |
---|---|
boolean |
initializeGrammar(Messages messages,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Initializes the grammar.
|
void |
parseAllFormulas(Messages messages,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Parse all Statement Formulas and update stmtTbl with results.
|
ParseTree |
parseFormula(Messages messages,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
Formula formula,
VarHyp[] varHypArray,
int highestSeq,
Stmt defaultStmtForRPN)
Parse a single formula.
|
ParseTree |
parseOneStmt(Messages messages,
java.util.Map<java.lang.String,Sym> symTbl,
java.util.Map<java.lang.String,Stmt> stmtTbl,
Stmt stmt)
Parse a single Statement.
|
ParseTree parseFormula(Messages messages, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, Formula formula, VarHyp[] varHypArray, int highestSeq, Stmt defaultStmtForRPN)
Note: access to symTbl and stmtTbl is required in case the grammar needs to be re-initialized.
Note: highestSeq is similar to the restriction in proof verification: a proof can only refer to previous statements. However, setting this to java.lang.Integer.MAX_VALUE says, parse this formula with the entire grammar -- which ought to result in the same parse, unless the grammar is ambiguous (new Grammar Rules should be "disjoint" from previous ones.)
messages
- Messages object for error/info messages.symTbl
- Symbol Table (Map).stmtTbl
- Statement Table (Map).formula
- Formula to parse.varHypArray
- VarHyp's for the Formula's Var's.highestSeq
- Max MObj.seq that can be referenced.defaultStmtForRPN
- Default Stmt for output RPN/message.ParseTree parseOneStmt(Messages messages, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl, Stmt stmt)
If used with VarHyp or SyntaxAxiom, simply returns stmt.getExprRPN().
Note: access to symTbl and stmtTbl is required in case the grammar needs to be re-initialized.
messages
- Messages object for error/info messages.symTbl
- Symbol Table (Map).stmtTbl
- Statement Table (Map).stmt
- Stmt in stmtTbl to parse.void parseAllFormulas(Messages messages, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl)
messages
- Messages object for error/info messages.symTbl
- Symbol Table (Map).stmtTbl
- Statement Table (Map).boolean initializeGrammar(Messages messages, java.util.Map<java.lang.String,Sym> symTbl, java.util.Map<java.lang.String,Stmt> stmtTbl)
Normally this is handled automatically. It initializes "the grammar" but does not parse every Stmt in stmtTbl.
The intended use of this function would be to initialize the grammar without parsing every statement (parsing every statement in set.mm requires 8ish seconds!)
messages
- Messages object for error/info messages.symTbl
- Symbol Table (Map).stmtTbl
- Statement Table (Map).