public class CommutativeTransformation extends Transformation
Modifier and Type | Field and Description |
---|---|
CommutativeInfo |
comInfo |
eqInfo, MORE_COMPLEX_TRANSFORMATION, NOTHING_TO_TRANSFORM, originalNode, trManager
Constructor and Description |
---|
CommutativeTransformation(TransformationManager trManager,
ParseNode originalNode,
mmj.transforms.GeneralizedStmt comProp) |
Modifier and Type | Method and Description |
---|---|
ParseNode |
getCanonicalNode(mmj.transforms.WorksheetInfo info) |
GenProofStepStmt |
transformMeToTarget(Transformation target,
mmj.transforms.WorksheetInfo info)
This function should construct derivation step sequence from this
Transformation.originalNode to target's
Transformation.originalNode |
checkTransformationNecessary, toString
public final CommutativeInfo comInfo
public CommutativeTransformation(TransformationManager trManager, ParseNode originalNode, mmj.transforms.GeneralizedStmt comProp)
public ParseNode getCanonicalNode(mmj.transforms.WorksheetInfo info)
getCanonicalNode
in class Transformation
info
- the information about previous statementsTransformation.originalNode
public GenProofStepStmt transformMeToTarget(Transformation target, mmj.transforms.WorksheetInfo info)
Transformation
Transformation.originalNode
to target's
Transformation.originalNode
transformMeToTarget
in class Transformation
target
- the target transformationinfo
- the information about work sheetTransformation.originalNode
is equal to target
Transformation.originalNode
. Could returns null it this
and target are equal.