public class TrUtil
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static GenProofStepStmt |
applyClosureProperties(boolean implForm,
GenProofStepStmt[] hyps,
mmj.transforms.WorksheetInfo info,
Assrt assrt,
ParseNode left,
ParseNode right) |
static int[] |
checkConstSubstAndGetVarPositions(ConstSubst constSubst,
ParseNode[] constMap) |
static ParseNode[] |
collectConstSubst(ParseNode originalNode) |
static ProofStepStmt[] |
convertGenToSimpleProofSteps(GenProofStepStmt[] genSteps)
This function converts the array of generalized steps into array of
simple proof steps.
|
static ParseNode |
createAssocBinaryNode(int from,
mmj.transforms.GeneralizedStmt genStmt,
ParseNode left,
ParseNode right) |
static ParseNode |
createBinaryNode(Stmt stmt,
ParseNode left,
ParseNode right)
Creates classical binary node
|
static ParseNode |
createGenBinaryNode(mmj.transforms.GeneralizedStmt genStmt,
ParseNode left,
ParseNode right)
Creates node for generalized statement.
|
static VarHyp |
findOneVarInParseNode(ParseNode input) |
static void |
findVarsInParseNode(ParseNode input,
java.util.Set<VarHyp> res) |
static VarHyp[] |
getHypToVarMap(Assrt assrt) |
static VarHyp[] |
getHypToVarMap(Assrt assrt,
VarHyp paramVar) |
static PropertyTemplate |
getTransformOperationTemplate(Assrt assrt) |
static boolean |
isConstNode(ParseNode node) |
static boolean |
isVarNode(ParseNode node) |
static boolean |
isVarStmt(Stmt stmt) |
public static boolean isVarNode(ParseNode node)
public static boolean isVarStmt(Stmt stmt)
public static boolean isConstNode(ParseNode node)
public static ParseNode createBinaryNode(Stmt stmt, ParseNode left, ParseNode right)
stmt
- the statementleft
- the first (left) noderight
- the second (right) nodepublic static ParseNode createGenBinaryNode(mmj.transforms.GeneralizedStmt genStmt, ParseNode left, ParseNode right)
genStmt
- the statementleft
- the first (left) noderight
- the second (right) nodepublic static ParseNode createAssocBinaryNode(int from, mmj.transforms.GeneralizedStmt genStmt, ParseNode left, ParseNode right)
public static int[] checkConstSubstAndGetVarPositions(ConstSubst constSubst, ParseNode[] constMap)
public static void findVarsInParseNode(ParseNode input, java.util.Set<VarHyp> res)
public static PropertyTemplate getTransformOperationTemplate(Assrt assrt)
public static ProofStepStmt[] convertGenToSimpleProofSteps(GenProofStepStmt[] genSteps)
genSteps
- steps in generalized formpublic static GenProofStepStmt applyClosureProperties(boolean implForm, GenProofStepStmt[] hyps, mmj.transforms.WorksheetInfo info, Assrt assrt, ParseNode left, ParseNode right)