Skip to content
Snippets Groups Projects
Commit 3a3c302b authored by Daniel Plagge's avatar Daniel Plagge
Browse files

Removed comparision with old implementation of the translation.

parent f2f95f63
No related branches found
No related tags found
No related merge requests found
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
* Heinrich Heine Universitaet Duesseldorf
* This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.eventb.translator;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedList;
import java.util.List;
import org.eventb.core.ast.BecomesEqualTo;
import org.eventb.core.ast.BecomesMemberOf;
import org.eventb.core.ast.BecomesSuchThat;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.ISimpleVisitor;
import org.eventb.core.ast.Predicate;
import de.be4.classicalb.core.parser.node.AAssignSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesElementOfSubstitution;
import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
import de.prob.eventb.translator.internal.TranslationVisitor;
/**
* @deprecated Use {@link TranslationVisitor} instead
*/
@Deprecated
public class AssignmentVisitor extends SimpleVisitorAdapter implements
ISimpleVisitor {
private PSubstitution sub;
private boolean substitutonSet = false;
public PSubstitution getSubstitution() {
return sub;
}
public void setSub(final PSubstitution sub) {
if (substitutonSet) {
throw new AssertionError("The Visitor must not be used twice!");
}
substitutonSet = true;
this.sub = sub;
}
@Override
public void visitBecomesEqualTo(final BecomesEqualTo assignment) {
final FreeIdentifier[] identifiers = assignment
.getAssignedIdentifiers();
final Expression[] expressions = assignment.getExpressions();
final AAssignSubstitution assignSubstitution = new AAssignSubstitution();
assignSubstitution
.setLhsExpression(createListOfIdentifiers(identifiers));
assignSubstitution
.setRhsExpressions(createListOfExpressions(expressions));
setSub(assignSubstitution);
}
private List<PExpression> createListOfExpressions(
final Expression[] expressions) {
final List<PExpression> list = new ArrayList<PExpression>();
for (Expression e : expressions) {
final ExpressionVisitor visitor = new ExpressionVisitor(
new LinkedList<String>());
e.accept(visitor);
list.add(visitor.getExpression());
}
return list;
}
private List<PExpression> createListOfIdentifiers(
final FreeIdentifier[] identifiers) {
final List<PExpression> res = new ArrayList<PExpression>(
identifiers.length);
for (FreeIdentifier freeIdentifier : identifiers) {
final List<TIdentifierLiteral> list = Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(
freeIdentifier.getName()) });
final AIdentifierExpression expression = new AIdentifierExpression();
expression.setIdentifier(list);
res.add(expression);
}
return res;
}
@Override
public void visitBecomesMemberOf(final BecomesMemberOf assignment) {
final ABecomesElementOfSubstitution becomesElementOfSubstitution = new ABecomesElementOfSubstitution();
final FreeIdentifier[] identifiers = assignment
.getAssignedIdentifiers();
final Expression set = assignment.getSet();
final ExpressionVisitor visitor = new ExpressionVisitor(
new LinkedList<String>());
set.accept(visitor);
becomesElementOfSubstitution
.setIdentifiers(createListOfIdentifiers(identifiers));
becomesElementOfSubstitution.setSet(visitor.getExpression());
setSub(becomesElementOfSubstitution);
}
@Override
public void visitBecomesSuchThat(final BecomesSuchThat assignment) {
final FreeIdentifier[] identifiers = assignment
.getAssignedIdentifiers();
LinkedList<String> list = new LinkedList<String>();
for (FreeIdentifier f : identifiers) {
list.addFirst(f.getName() + "'");
}
final Predicate predicate = assignment.getCondition();
final PredicateVisitor visitor = new PredicateVisitor(list);
predicate.accept(visitor);
final ABecomesSuchSubstitution becomesSuchSubstitution = new ABecomesSuchSubstitution();
becomesSuchSubstitution
.setIdentifiers(createListOfIdentifiers(identifiers));
becomesSuchSubstitution.setPredicate(visitor.getPredicate());
setSub(becomesSuchSubstitution);
}
}
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.eventb.translator; // NOPMD
// high coupling is ok, we only use the AST nodes
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.LinkedList;
import java.util.List;
import org.eventb.core.ast.AssociativeExpression;
import org.eventb.core.ast.AtomicExpression;
import org.eventb.core.ast.BinaryExpression;
import org.eventb.core.ast.BoolExpression;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.ExtendedExpression;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.ISimpleVisitor;
import org.eventb.core.ast.IntegerLiteral;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.QuantifiedExpression;
import org.eventb.core.ast.SetExtension;
import org.eventb.core.ast.UnaryExpression;
import org.eventb.core.ast.extension.IExpressionExtension;
import de.be4.classicalb.core.parser.node.AAddExpression;
import de.be4.classicalb.core.parser.node.ABoolSetExpression;
import de.be4.classicalb.core.parser.node.ABooleanFalseExpression;
import de.be4.classicalb.core.parser.node.ABooleanTrueExpression;
import de.be4.classicalb.core.parser.node.ACardExpression;
import de.be4.classicalb.core.parser.node.ACartesianProductExpression;
import de.be4.classicalb.core.parser.node.ACompositionExpression;
import de.be4.classicalb.core.parser.node.AConvertBoolExpression;
import de.be4.classicalb.core.parser.node.ACoupleExpression;
import de.be4.classicalb.core.parser.node.ADirectProductExpression;
import de.be4.classicalb.core.parser.node.ADivExpression;
import de.be4.classicalb.core.parser.node.ADomainExpression;
import de.be4.classicalb.core.parser.node.ADomainRestrictionExpression;
import de.be4.classicalb.core.parser.node.ADomainSubtractionExpression;
import de.be4.classicalb.core.parser.node.AEmptySetExpression;
import de.be4.classicalb.core.parser.node.AEventBComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AEventBFirstProjectionExpression;
import de.be4.classicalb.core.parser.node.AEventBFirstProjectionV2Expression;
import de.be4.classicalb.core.parser.node.AEventBIdentityExpression;
import de.be4.classicalb.core.parser.node.AEventBSecondProjectionExpression;
import de.be4.classicalb.core.parser.node.AEventBSecondProjectionV2Expression;
import de.be4.classicalb.core.parser.node.AExtendedExprExpression;
import de.be4.classicalb.core.parser.node.AFunctionExpression;
import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
import de.be4.classicalb.core.parser.node.AGeneralUnionExpression;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.AIdentityExpression;
import de.be4.classicalb.core.parser.node.AImageExpression;
import de.be4.classicalb.core.parser.node.AIntegerExpression;
import de.be4.classicalb.core.parser.node.AIntegerSetExpression;
import de.be4.classicalb.core.parser.node.AIntersectionExpression;
import de.be4.classicalb.core.parser.node.AIntervalExpression;
import de.be4.classicalb.core.parser.node.AMaxExpression;
import de.be4.classicalb.core.parser.node.AMinExpression;
import de.be4.classicalb.core.parser.node.AMinusExpression;
import de.be4.classicalb.core.parser.node.AModuloExpression;
import de.be4.classicalb.core.parser.node.AMultiplicationExpression;
import de.be4.classicalb.core.parser.node.ANatural1SetExpression;
import de.be4.classicalb.core.parser.node.ANaturalSetExpression;
import de.be4.classicalb.core.parser.node.AOverwriteExpression;
import de.be4.classicalb.core.parser.node.AParallelProductExpression;
import de.be4.classicalb.core.parser.node.APartialFunctionExpression;
import de.be4.classicalb.core.parser.node.APartialInjectionExpression;
import de.be4.classicalb.core.parser.node.APartialSurjectionExpression;
import de.be4.classicalb.core.parser.node.APow1SubsetExpression;
import de.be4.classicalb.core.parser.node.APowSubsetExpression;
import de.be4.classicalb.core.parser.node.APowerOfExpression;
import de.be4.classicalb.core.parser.node.APredecessorExpression;
import de.be4.classicalb.core.parser.node.AQuantifiedIntersectionExpression;
import de.be4.classicalb.core.parser.node.AQuantifiedUnionExpression;
import de.be4.classicalb.core.parser.node.ARangeExpression;
import de.be4.classicalb.core.parser.node.ARangeRestrictionExpression;
import de.be4.classicalb.core.parser.node.ARangeSubtractionExpression;
import de.be4.classicalb.core.parser.node.ARelationsExpression;
import de.be4.classicalb.core.parser.node.AReverseExpression;
import de.be4.classicalb.core.parser.node.ARingExpression;
import de.be4.classicalb.core.parser.node.ASetExtensionExpression;
import de.be4.classicalb.core.parser.node.ASetSubtractionExpression;
import de.be4.classicalb.core.parser.node.ASuccessorExpression;
import de.be4.classicalb.core.parser.node.ASurjectionRelationExpression;
import de.be4.classicalb.core.parser.node.ATotalBijectionExpression;
import de.be4.classicalb.core.parser.node.ATotalFunctionExpression;
import de.be4.classicalb.core.parser.node.ATotalInjectionExpression;
import de.be4.classicalb.core.parser.node.ATotalRelationExpression;
import de.be4.classicalb.core.parser.node.ATotalSurjectionExpression;
import de.be4.classicalb.core.parser.node.ATotalSurjectionRelationExpression;
import de.be4.classicalb.core.parser.node.AUnaryMinusExpression;
import de.be4.classicalb.core.parser.node.AUnionExpression;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.be4.classicalb.core.parser.node.TIntegerLiteral;
import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
import de.prob.eventb.translator.internal.TranslationVisitor;
// Complexity is actually quite low for a visitor ;-)
/**
* @deprecated Use {@link TranslationVisitor} instead
*/
@Deprecated
public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
// by bendisposto
ISimpleVisitor {
private PExpression e;
private final LinkedList<String> bounds; // NOPMD bendisposto
// we need some abilities of the linked list, using List is not an option
private boolean expressionSet = false;
public ExpressionVisitor(final LinkedList<String> bounds) { // NOPMD
super();
this.bounds = bounds;
}
public PExpression getExpression() {
return e;
}
public void setExpression(final PExpression e) {
if (expressionSet) {
throw new AssertionError("The Visitor must not be used twice!");
}
expressionSet = true;
this.e = e;
}
@Override
public void visitQuantifiedExpression(final QuantifiedExpression expression) {
// QUNION, QINTER, CSET
final int tag = expression.getTag();
final List<ExpressionVisitor> ev = new LinkedList<ExpressionVisitor>();
final BoundIdentDecl[] decls = expression.getBoundIdentDecls();
for (final BoundIdentDecl boundIdentDecl : decls) {
final ExpressionVisitor visitor = new ExpressionVisitor(bounds);
boundIdentDecl.accept(visitor);
ev.add(visitor);
bounds.addFirst(boundIdentDecl.getName());
}
// Collect Subtrees in a list.
final LinkedList<PExpression> list = new LinkedList<PExpression>();
for (final ExpressionVisitor visitor : ev) {
list.add(visitor.getExpression());
}
// Process internal Expression and Predicate
final Predicate predicate = expression.getPredicate();
final PredicateVisitor predicateVisitor = new PredicateVisitor(bounds);
predicate.accept(predicateVisitor);
final PPredicate pr = predicateVisitor.getPredicate();
final ExpressionVisitor expressionVisitor = new ExpressionVisitor(
bounds);
expression.getExpression().accept(expressionVisitor);
final PExpression ex = expressionVisitor.getExpression();
switch (tag) {
case Formula.QUNION:
final AQuantifiedUnionExpression quantifiedUnionExpression = new AQuantifiedUnionExpression();
quantifiedUnionExpression.setExpression(ex);
quantifiedUnionExpression.setPredicates(pr);
quantifiedUnionExpression.setIdentifiers(list);
setExpression(quantifiedUnionExpression);
break;
case Formula.QINTER:
final AQuantifiedIntersectionExpression quantifiedIntersectionExpression = new AQuantifiedIntersectionExpression();
quantifiedIntersectionExpression.setExpression(ex);
quantifiedIntersectionExpression.setPredicates(pr);
quantifiedIntersectionExpression.setIdentifiers(list);
setExpression(quantifiedIntersectionExpression);
break;
case Formula.CSET:
final AEventBComprehensionSetExpression comprehensionSetExpression = new AEventBComprehensionSetExpression();
comprehensionSetExpression.setExpression(ex);
comprehensionSetExpression.setPredicates(pr);
comprehensionSetExpression.setIdentifiers(list);
setExpression(comprehensionSetExpression);
break;
default:
break;
}
for (int i = 0; i < decls.length; i++) {
bounds.remove(0);
}
}
@Override
public void visitAssociativeExpression(
final AssociativeExpression expression) {
// BUNION, BINTER, BCOMP, FCOMP, OVR, PLUS, MUL
final Expression[] children = expression.getChildren();
final LinkedList<ExpressionVisitor> ev = new LinkedList<ExpressionVisitor>();
for (final Expression ex : children) {
final ExpressionVisitor e = new ExpressionVisitor(bounds);
ev.add(e);
ex.accept(e);
}
final int tag = expression.getTag();
switch (tag) {
case Formula.BUNION:
setExpression(recurseBUNION(ev));
break;
case Formula.BINTER:
setExpression(recurseBINTER(ev));
break;
case Formula.BCOMP:
setExpression(recurseBCOMP(ev));
break;
case Formula.FCOMP:
setExpression(recurseFCOMP(ev));
break;
case Formula.OVR:
setExpression(recurseOVR(ev));
break;
case Formula.PLUS:
setExpression(recursePLUS(ev));
break;
case Formula.MUL:
setExpression(recurseMUL(ev));
break;
default:
break;
}
super.visitAssociativeExpression(expression);
}
private PExpression recurseFCOMP(final List<ExpressionVisitor> list) {
final ACompositionExpression r = new ACompositionExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseFCOMP(list.subList(1, list.size())));
}
return r;
}
private PExpression recurseOVR(final List<ExpressionVisitor> list) {
final AOverwriteExpression r = new AOverwriteExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseOVR(list.subList(1, list.size())));
}
return r;
}
private PExpression recursePLUS(final List<ExpressionVisitor> list) {
final AAddExpression r = new AAddExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recursePLUS(list.subList(1, list.size())));
}
return r;
}
private PExpression recurseMUL(final List<ExpressionVisitor> list) {
final AMultiplicationExpression r = new AMultiplicationExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseMUL(list.subList(1, list.size())));
}
return r;
}
private PExpression recurseBUNION(final List<ExpressionVisitor> list) {
final AUnionExpression r = new AUnionExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseBUNION(list.subList(1, list.size())));
}
return r;
}
private PExpression recurseBINTER(final List<ExpressionVisitor> list) {
final AIntersectionExpression r = new AIntersectionExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseBINTER(list.subList(1, list.size())));
}
return r;
}
private PExpression recurseBCOMP(final List<ExpressionVisitor> list) {
final ARingExpression r = new ARingExpression();
if (list.size() == 2) {
r.setLeft(list.get(0).getExpression());
r.setRight(list.get(1).getExpression());
} else {
r.setLeft(list.get(0).getExpression());
r.setRight(recurseBCOMP(list.subList(1, list.size())));
}
return r;
}
@Override
// this long method is far easier to read than smaller ones
public void visitBinaryExpression(final BinaryExpression expression) { // NOPMD
final int tag = expression.getTag();
final ExpressionVisitor visitorLeft = new ExpressionVisitor(bounds);
final ExpressionVisitor visitorRight = new ExpressionVisitor(bounds);
expression.getLeft().accept(visitorLeft);
expression.getRight().accept(visitorRight);
final PExpression exL = visitorLeft.getExpression();
final PExpression exR = visitorRight.getExpression();
switch (tag) {
case Formula.MAPSTO:
final ACoupleExpression coupleExpression = new ACoupleExpression();
coupleExpression.setList(Arrays
.asList(new PExpression[] { exL, exR }));
setExpression(coupleExpression);
break;
case Formula.REL:
final ARelationsExpression relationsExpression = new ARelationsExpression();
relationsExpression.setLeft(exL);
relationsExpression.setRight(exR);
setExpression(relationsExpression);
break;
case Formula.TREL:
final ATotalRelationExpression totalRelationExpression = new ATotalRelationExpression();
totalRelationExpression.setLeft(exL);
totalRelationExpression.setRight(exR);
setExpression(totalRelationExpression);
break;
case Formula.SREL:
final ASurjectionRelationExpression surjectionRelationExpression = new ASurjectionRelationExpression();
surjectionRelationExpression.setLeft(exL);
surjectionRelationExpression.setRight(exR);
setExpression(surjectionRelationExpression);
break;
case Formula.STREL:
final ATotalSurjectionRelationExpression totalSurjectionRelationExpression = new ATotalSurjectionRelationExpression();
totalSurjectionRelationExpression.setLeft(exL);
totalSurjectionRelationExpression.setRight(exR);
setExpression(totalSurjectionRelationExpression);
break;
case Formula.PFUN:
final APartialFunctionExpression partialFunctionExpression = new APartialFunctionExpression();
partialFunctionExpression.setLeft(exL);
partialFunctionExpression.setRight(exR);
setExpression(partialFunctionExpression);
break;
case Formula.TFUN:
final ATotalFunctionExpression totalFunctionExpression = new ATotalFunctionExpression();
totalFunctionExpression.setLeft(exL);
totalFunctionExpression.setRight(exR);
setExpression(totalFunctionExpression);
break;
case Formula.PINJ:
final APartialInjectionExpression partialInjectionExpression = new APartialInjectionExpression();
partialInjectionExpression.setLeft(exL);
partialInjectionExpression.setRight(exR);
setExpression(partialInjectionExpression);
break;
case Formula.TINJ:
final ATotalInjectionExpression totalInjectionExpression = new ATotalInjectionExpression();
totalInjectionExpression.setLeft(exL);
totalInjectionExpression.setRight(exR);
setExpression(totalInjectionExpression);
break;
case Formula.PSUR:
final APartialSurjectionExpression partialSurjectionExpression = new APartialSurjectionExpression();
partialSurjectionExpression.setLeft(exL);
partialSurjectionExpression.setRight(exR);
setExpression(partialSurjectionExpression);
break;
case Formula.TSUR:
final ATotalSurjectionExpression totalSurjectionExpression = new ATotalSurjectionExpression();
totalSurjectionExpression.setLeft(exL);
totalSurjectionExpression.setRight(exR);
setExpression(totalSurjectionExpression);
break;
case Formula.TBIJ:
final ATotalBijectionExpression totalBijectionExpression = new ATotalBijectionExpression();
totalBijectionExpression.setLeft(exL);
totalBijectionExpression.setRight(exR);
setExpression(totalBijectionExpression);
break;
case Formula.SETMINUS:
final ASetSubtractionExpression setSubtractionExpression = new ASetSubtractionExpression();
setSubtractionExpression.setLeft(exL);
setSubtractionExpression.setRight(exR);
setExpression(setSubtractionExpression);
break;
case Formula.CPROD:
final ACartesianProductExpression mulExpression = new ACartesianProductExpression();
mulExpression.setLeft(exL);
mulExpression.setRight(exR);
setExpression(mulExpression);
break;
case Formula.DPROD:
final ADirectProductExpression directProductExpression = new ADirectProductExpression();
directProductExpression.setLeft(exL);
directProductExpression.setRight(exR);
setExpression(directProductExpression);
break;
case Formula.PPROD:
final AParallelProductExpression parallelProductExpression = new AParallelProductExpression();
parallelProductExpression.setLeft(exL);
parallelProductExpression.setRight(exR);
setExpression(parallelProductExpression);
break;
case Formula.DOMRES:
final ADomainRestrictionExpression domainRestrictionExpression = new ADomainRestrictionExpression();
domainRestrictionExpression.setLeft(exL);
domainRestrictionExpression.setRight(exR);
setExpression(domainRestrictionExpression);
break;
case Formula.DOMSUB:
final ADomainSubtractionExpression domainSubtractionExpression = new ADomainSubtractionExpression();
domainSubtractionExpression.setLeft(exL);
domainSubtractionExpression.setRight(exR);
setExpression(domainSubtractionExpression);
break;
case Formula.RANRES:
final ARangeRestrictionExpression rangeRestrictionExpression = new ARangeRestrictionExpression();
rangeRestrictionExpression.setLeft(exL);
rangeRestrictionExpression.setRight(exR);
setExpression(rangeRestrictionExpression);
break;
case Formula.RANSUB:
final ARangeSubtractionExpression rangeSubtractionExpression = new ARangeSubtractionExpression();
rangeSubtractionExpression.setLeft(exL);
rangeSubtractionExpression.setRight(exR);
setExpression(rangeSubtractionExpression);
break;
case Formula.UPTO:
final AIntervalExpression intervalExpression = new AIntervalExpression();
intervalExpression.setLeftBorder(exL);
intervalExpression.setRightBorder(exR);
setExpression(intervalExpression);
break;
case Formula.MINUS:
final AMinusExpression minusExpression = new AMinusExpression();
minusExpression.setLeft(exL);
minusExpression.setRight(exR);
setExpression(minusExpression);
break;
case Formula.DIV:
final ADivExpression divExpression = new ADivExpression();
divExpression.setLeft(exL);
divExpression.setRight(exR);
setExpression(divExpression);
break;
case Formula.MOD:
final AModuloExpression moduloExpression = new AModuloExpression();
moduloExpression.setLeft(exL);
moduloExpression.setRight(exR);
setExpression(moduloExpression);
break;
case Formula.EXPN:
final APowerOfExpression powerOfExpression = new APowerOfExpression();
powerOfExpression.setLeft(exL);
powerOfExpression.setRight(exR);
setExpression(powerOfExpression);
break;
case Formula.FUNIMAGE:
final AFunctionExpression functionExpression = new AFunctionExpression();
functionExpression.setIdentifier(exL);
functionExpression.setParameters(Arrays
.asList(new PExpression[] { exR }));
setExpression(functionExpression);
break;
case Formula.RELIMAGE:
final AImageExpression imageExpression = new AImageExpression();
imageExpression.setLeft(exL);
imageExpression.setRight(exR);
setExpression(imageExpression);
break;
default:
throw new AssertionError("Uncovered Expression");
}
}
@Override
public void visitAtomicExpression(final AtomicExpression expression) { // NOPMD
// by
// bendisposto
final int tag = expression.getTag();
switch (tag) {
case Formula.INTEGER:
setExpression(new AIntegerSetExpression());
break;
case Formula.NATURAL:
setExpression(new ANaturalSetExpression());
break;
case Formula.NATURAL1:
setExpression(new ANatural1SetExpression());
break;
case Formula.BOOL:
setExpression(new ABoolSetExpression());
break;
case Formula.TRUE:
setExpression(new ABooleanTrueExpression());
break;
case Formula.FALSE:
setExpression(new ABooleanFalseExpression());
break;
case Formula.EMPTYSET:
setExpression(new AEmptySetExpression());
break;
case Formula.KPRED:
setExpression(new APredecessorExpression());
break;
case Formula.KSUCC:
setExpression(new ASuccessorExpression());
break;
case Formula.KPRJ1_GEN: // see task#215
setExpression(new AEventBFirstProjectionV2Expression());
break;
case Formula.KPRJ2_GEN:
setExpression(new AEventBSecondProjectionV2Expression());
break;
case Formula.KID_GEN:
setExpression(new AEventBIdentityExpression());
break;
default:
throw new AssertionError("Uncovered Expression " + expression);
}
}
@Override
public void visitBoolExpression(final BoolExpression expression) {
final AConvertBoolExpression convertBoolExpression = new AConvertBoolExpression();
final PredicateVisitor visitor = new PredicateVisitor(bounds);
expression.getPredicate().accept(visitor);
convertBoolExpression.setPredicate(visitor.getPredicate());
setExpression(convertBoolExpression);
}
@Override
public void visitBoundIdentDecl(final BoundIdentDecl boundIdentDecl) {
final List<TIdentifierLiteral> list = Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(
boundIdentDecl.getName()) });
final AIdentifierExpression expression = new AIdentifierExpression();
expression.setIdentifier(list);
setExpression(expression);
}
@Override
public void visitBoundIdentifier(final BoundIdentifier identifierExpression) {
final List<TIdentifierLiteral> list = Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(
bounds.get(identifierExpression.getBoundIndex())) });
final AIdentifierExpression expression = new AIdentifierExpression();
expression.setIdentifier(list);
setExpression(expression);
}
@Override
public void visitFreeIdentifier(final FreeIdentifier identifierExpression) {
final List<TIdentifierLiteral> list = Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(
identifierExpression.getName()) });
final AIdentifierExpression expression = new AIdentifierExpression();
expression.setIdentifier(list);
setExpression(expression);
}
@Override
public void visitIntegerLiteral(final IntegerLiteral expression) {
final BigInteger value = expression.getValue();
final AIntegerExpression integerExpression = new AIntegerExpression();
integerExpression.setLiteral(new TIntegerLiteral(value.toString()));
setExpression(integerExpression);
}
@Override
public void visitSetExtension(final SetExtension expression) {
final Expression[] members = expression.getMembers();
final ASetExtensionExpression setExtensionExpression = new ASetExtensionExpression();
final List<PExpression> list = new ArrayList<PExpression>();
for (final Expression e : members) {
final ExpressionVisitor visitor = new ExpressionVisitor(bounds);
e.accept(visitor);
list.add(visitor.getExpression());
}
setExtensionExpression.setExpressions(list);
setExpression(setExtensionExpression);
}
@Override
public void visitExtendedExpression(ExtendedExpression expression) {
AExtendedExprExpression p = new AExtendedExprExpression();
IExpressionExtension extension = expression.getExtension();
String symbol = extension.getSyntaxSymbol();
p.setIdentifier(new TIdentifierLiteral(symbol));
Expression[] expressions = expression.getChildExpressions();
List<PExpression> childExprs = new ArrayList<PExpression>();
for (Expression e : expressions) {
ExpressionVisitor v = new ExpressionVisitor(bounds);
e.accept(v);
childExprs.add(v.getExpression());
}
p.setExpressions(childExprs);
Predicate[] childPredicates = expression.getChildPredicates();
List<PPredicate> childPreds = new ArrayList<PPredicate>();
for (Predicate pd : childPredicates) {
PredicateVisitor v = new PredicateVisitor(bounds);
pd.accept(v);
childPreds.add(v.getPredicate());
}
p.setPredicates(childPreds);
setExpression(p);
}
@Override
public void visitUnaryExpression(final UnaryExpression expression) { // NOPMD
// by
// bendisposto
final int tag = expression.getTag();
final ExpressionVisitor visitor = new ExpressionVisitor(bounds);
expression.getChild().accept(visitor);
final PExpression exp = visitor.getExpression();
switch (tag) {
case Formula.KCARD:
final ACardExpression cardExpression = new ACardExpression();
cardExpression.setExpression(exp);
setExpression(cardExpression);
break;
case Formula.POW:
final APowSubsetExpression powExpression = new APowSubsetExpression();
powExpression.setExpression(exp);
setExpression(powExpression);
break;
case Formula.POW1:
final APow1SubsetExpression pow1Expression = new APow1SubsetExpression();
pow1Expression.setExpression(exp);
setExpression(pow1Expression);
break;
case Formula.KUNION:
final AGeneralUnionExpression unionExpression = new AGeneralUnionExpression();
unionExpression.setExpression(exp);
setExpression(unionExpression);
break;
case Formula.KINTER:
final AGeneralIntersectionExpression interExpression = new AGeneralIntersectionExpression();
interExpression.setExpression(exp);
setExpression(interExpression);
break;
case Formula.KDOM:
final ADomainExpression domainExpression = new ADomainExpression();
domainExpression.setExpression(exp);
setExpression(domainExpression);
break;
case Formula.KRAN:
final ARangeExpression rangeExpression = new ARangeExpression();
rangeExpression.setExpression(exp);
setExpression(rangeExpression);
break;
case Formula.KPRJ1:
final AEventBFirstProjectionExpression firstProjectionExpression = new AEventBFirstProjectionExpression();
firstProjectionExpression.setExpression(exp);
setExpression(firstProjectionExpression);
break;
case Formula.KPRJ2:
final AEventBSecondProjectionExpression secondProjectionExpression = new AEventBSecondProjectionExpression();
secondProjectionExpression.setExpression(exp);
setExpression(secondProjectionExpression);
break;
case Formula.KID:
final AIdentityExpression identityExpression = new AIdentityExpression();
identityExpression.setExpression(exp);
setExpression(identityExpression);
break;
case Formula.KMIN:
final AMinExpression minExpression = new AMinExpression();
minExpression.setExpression(exp);
setExpression(minExpression);
break;
case Formula.KMAX:
final AMaxExpression maxExpression = new AMaxExpression();
maxExpression.setExpression(exp);
setExpression(maxExpression);
break;
case Formula.CONVERSE:
final AReverseExpression reverseExpression = new AReverseExpression();
reverseExpression.setExpression(exp);
setExpression(reverseExpression);
break;
case Formula.UNMINUS:
final AUnaryMinusExpression unaryExpression = new AUnaryMinusExpression();
unaryExpression.setExpression(exp);
setExpression(unaryExpression);
break;
default:
throw new AssertionError("Uncovered Expression");
}
}
}
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, Heinrich
* Heine Universitaet Duesseldorf This software is licenced under EPL 1.0
* (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.eventb.translator; // NOPMD
// High number of imports because it depends on AST
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
import org.eventb.core.ast.AssociativePredicate;
import org.eventb.core.ast.BinaryPredicate;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.Expression;
import org.eventb.core.ast.ExtendedPredicate;
import org.eventb.core.ast.Formula;
import org.eventb.core.ast.ISimpleVisitor;
import org.eventb.core.ast.LiteralPredicate;
import org.eventb.core.ast.MultiplePredicate;
import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.QuantifiedPredicate;
import org.eventb.core.ast.RelationalPredicate;
import org.eventb.core.ast.SimplePredicate;
import org.eventb.core.ast.UnaryPredicate;
import org.eventb.core.ast.extension.IPredicateExtension;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
import de.be4.classicalb.core.parser.node.AExtendedPredPredicate;
import de.be4.classicalb.core.parser.node.AFalsityPredicate;
import de.be4.classicalb.core.parser.node.AFinitePredicate;
import de.be4.classicalb.core.parser.node.AForallPredicate;
import de.be4.classicalb.core.parser.node.AGreaterEqualPredicate;
import de.be4.classicalb.core.parser.node.AGreaterPredicate;
import de.be4.classicalb.core.parser.node.AImplicationPredicate;
import de.be4.classicalb.core.parser.node.ALessEqualPredicate;
import de.be4.classicalb.core.parser.node.ALessPredicate;
import de.be4.classicalb.core.parser.node.AMemberPredicate;
import de.be4.classicalb.core.parser.node.ANegationPredicate;
import de.be4.classicalb.core.parser.node.ANotEqualPredicate;
import de.be4.classicalb.core.parser.node.ANotMemberPredicate;
import de.be4.classicalb.core.parser.node.ANotSubsetPredicate;
import de.be4.classicalb.core.parser.node.ANotSubsetStrictPredicate;
import de.be4.classicalb.core.parser.node.APartitionPredicate;
import de.be4.classicalb.core.parser.node.ASubsetPredicate;
import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate;
import de.be4.classicalb.core.parser.node.ATruthPredicate;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
import de.prob.eventb.translator.internal.TranslationVisitor;
/**
* @deprecated Use {@link TranslationVisitor} instead
*/
@Deprecated
public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
ISimpleVisitor {
private static final String UNCOVERED_PREDICATE = "Uncovered Predicate";
private PPredicate p;
private final LinkedList<String> bounds; // NOPMD
// we need properties of linked lists, List is not an option
private boolean predicateSet = false;
public PPredicate getPredicate() {
return p;
}
public void setPredicate(final PPredicate p) {
synchronized (bounds) {
if (predicateSet) {
throw new AssertionError("The Visitor must not be used twice!");
}
predicateSet = true;
this.p = p;
}
// public ClassifiedPragma(String name, Node attachedTo, List<String>
// arguments, List<String> warnings, SourcePosition start,
// SourcePosition end) {
// new ClassifiedPragma("discharged", p, proof, Collections.emptyList(),
// new SourcePosition(-1, -1), new SourcePosition(-1, -1));
}
public PredicateVisitor() {
this(null);
}
public PredicateVisitor(LinkedList<String> bounds) {
super();
if (bounds == null) {
this.bounds = new LinkedList<String>();
} else {
this.bounds = bounds;
}
}
@Override
public void visitQuantifiedPredicate(final QuantifiedPredicate predicate) {
final int tag = predicate.getTag();
// Add quantified identifiers to bound list and recursively create
// subtrees representing the identifiers
final List<ExpressionVisitor> ev = new LinkedList<ExpressionVisitor>();
final BoundIdentDecl[] decls = predicate.getBoundIdentDecls();
for (final BoundIdentDecl boundIdentDecl : decls) {
final ExpressionVisitor visitor = new ExpressionVisitor(bounds);
boundIdentDecl.accept(visitor);
ev.add(visitor);
bounds.addFirst(boundIdentDecl.getName());
}
// Collect Subtrees in a list
final LinkedList<PExpression> list = new LinkedList<PExpression>();
for (final ExpressionVisitor visitor : ev) {
list.add(visitor.getExpression());
}
// Recursively analyze the predicate (important, bounds are already set)
final PredicateVisitor predicateVisitor = new PredicateVisitor(bounds);
predicate.getPredicate().accept(predicateVisitor);
switch (tag) {
case Formula.EXISTS:
final AExistsPredicate existentialQuantificationPredicate = new AExistsPredicate();
existentialQuantificationPredicate.setIdentifiers(list);
existentialQuantificationPredicate.setPredicate(predicateVisitor
.getPredicate());
setPredicate(existentialQuantificationPredicate);
break;
case Formula.FORALL:
final AForallPredicate universalQuantificationPredicate = new AForallPredicate();
universalQuantificationPredicate.setIdentifiers(list);
PPredicate pred = predicateVisitor.getPredicate();
if (!(pred instanceof AImplicationPredicate)) {
pred = new AImplicationPredicate(new ATruthPredicate(), pred);
}
universalQuantificationPredicate.setImplication(pred);
setPredicate(universalQuantificationPredicate);
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
// remove quantified identifiers from bound list (leaving scope)
for (int i = 0; i < decls.length; i++) {
bounds.removeFirst();
}
}
@Override
public void visitAssociativePredicate(final AssociativePredicate predicate) {
// {LAND, LOR, LEQV}
final int tag = predicate.getTag();
final Predicate[] children = predicate.getChildren();
if (children.length < 2) {
throw new AssertionError(
"Predicate must have at least 2 subpredicates.");
}
final LinkedList<PredicateVisitor> pv = new LinkedList<PredicateVisitor>();
for (final Predicate pr : children) {
final PredicateVisitor p = new PredicateVisitor(bounds);
pv.add(p);
pr.accept(p);
}
switch (tag) {
case Formula.LOR:
setPredicate(recurseOR(pv));
break;
case Formula.LAND:
setPredicate(recurseAND(pv));
break;
case Formula.LEQV:
setPredicate(recurseEQV(pv));
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
}
private PPredicate recurseOR(final List<PredicateVisitor> list) {
final ADisjunctPredicate r = new ADisjunctPredicate();
if (list.size() == 2) {
r.setLeft(list.get(0).getPredicate());
r.setRight(list.get(1).getPredicate());
} else {
r.setLeft(list.get(0).getPredicate());
r.setRight(recurseOR(list.subList(1, list.size())));
}
return r;
}
private PPredicate recurseAND(final List<PredicateVisitor> list) {
final AConjunctPredicate r = new AConjunctPredicate();
if (list.size() == 2) {
r.setLeft(list.get(0).getPredicate());
r.setRight(list.get(1).getPredicate());
} else {
r.setLeft(list.get(0).getPredicate());
r.setRight(recurseAND(list.subList(1, list.size())));
}
return r;
}
private PPredicate recurseEQV(final List<PredicateVisitor> list) {
final AEquivalencePredicate r = new AEquivalencePredicate();
if (list.size() == 2) {
r.setLeft(list.get(0).getPredicate());
r.setRight(list.get(1).getPredicate());
} else {
r.setLeft(list.get(0).getPredicate());
r.setRight(recurseEQV(list.subList(1, list.size())));
}
return r;
}
@Override
public void visitBinaryPredicate(final BinaryPredicate predicate) {
final int tag = predicate.getTag();
final PredicateVisitor subLeft = new PredicateVisitor(bounds);
predicate.getLeft().accept(subLeft);
final PredicateVisitor subRight = new PredicateVisitor(bounds);
predicate.getRight().accept(subRight);
switch (tag) {
case Formula.LIMP:
final AImplicationPredicate limp = new AImplicationPredicate();
limp.setLeft(subLeft.getPredicate());
limp.setRight(subRight.getPredicate());
setPredicate(limp);
break;
case Formula.LEQV:
final AEquivalencePredicate leqv = new AEquivalencePredicate();
leqv.setLeft(subLeft.getPredicate());
leqv.setRight(subRight.getPredicate());
setPredicate(leqv);
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
}
@Override
public void visitLiteralPredicate(final LiteralPredicate predicate) {
final int tag = predicate.getTag();
switch (tag) {
case Formula.BTRUE:
setPredicate(new ATruthPredicate());
break;
case Formula.BFALSE:
setPredicate(new AFalsityPredicate());
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
}
@Override
public void visitRelationalPredicate(final RelationalPredicate predicate) { // NOPMD
// High complexity is ok
// EQUAL, NOTEQUAL, LT, LE, GT, GE, IN, NOTIN, SUBSET,
// NOTSUBSET, SUBSETEQ, NOTSUBSETEQ
final ExpressionVisitor subLeft = new ExpressionVisitor(bounds);
predicate.getLeft().accept(subLeft);
final ExpressionVisitor subRight = new ExpressionVisitor(bounds);
predicate.getRight().accept(subRight);
final int tag = predicate.getTag();
switch (tag) {
case Formula.EQUAL:
final AEqualPredicate equalPredicate = new AEqualPredicate();
equalPredicate.setLeft(subLeft.getExpression());
equalPredicate.setRight(subRight.getExpression());
setPredicate(equalPredicate);
break;
case Formula.NOTEQUAL:
final ANotEqualPredicate unequalPredicate = new ANotEqualPredicate();
unequalPredicate.setLeft(subLeft.getExpression());
unequalPredicate.setRight(subRight.getExpression());
setPredicate(unequalPredicate);
break;
case Formula.LT:
final ALessPredicate ltPredicate = new ALessPredicate();
ltPredicate.setLeft(subLeft.getExpression());
ltPredicate.setRight(subRight.getExpression());
setPredicate(ltPredicate);
break;
case Formula.LE:
final ALessEqualPredicate lePredicate = new ALessEqualPredicate();
lePredicate.setLeft(subLeft.getExpression());
lePredicate.setRight(subRight.getExpression());
setPredicate(lePredicate);
break;
case Formula.GT:
final AGreaterPredicate gtPredicate = new AGreaterPredicate();
gtPredicate.setLeft(subLeft.getExpression());
gtPredicate.setRight(subRight.getExpression());
setPredicate(gtPredicate);
break;
case Formula.GE:
final AGreaterEqualPredicate gePredicate = new AGreaterEqualPredicate();
gePredicate.setLeft(subLeft.getExpression());
gePredicate.setRight(subRight.getExpression());
setPredicate(gePredicate);
break;
case Formula.IN:
final AMemberPredicate inPredicate = new AMemberPredicate();
inPredicate.setLeft(subLeft.getExpression());
inPredicate.setRight(subRight.getExpression());
setPredicate(inPredicate);
break;
case Formula.NOTIN:
final ANotMemberPredicate ninPredicate = new ANotMemberPredicate();
ninPredicate.setLeft(subLeft.getExpression());
ninPredicate.setRight(subRight.getExpression());
setPredicate(ninPredicate);
break;
case Formula.SUBSET:
final ASubsetStrictPredicate strictSubsetPredicate = new ASubsetStrictPredicate();
strictSubsetPredicate.setLeft(subLeft.getExpression());
strictSubsetPredicate.setRight(subRight.getExpression());
setPredicate(strictSubsetPredicate);
break;
case Formula.NOTSUBSET:
final ANotSubsetStrictPredicate notStrictSubsetPredicate = new ANotSubsetStrictPredicate();
notStrictSubsetPredicate.setLeft(subLeft.getExpression());
notStrictSubsetPredicate.setRight(subRight.getExpression());
setPredicate(notStrictSubsetPredicate);
break;
case Formula.SUBSETEQ:
final ASubsetPredicate subsetPredicate = new ASubsetPredicate();
subsetPredicate.setLeft(subLeft.getExpression());
subsetPredicate.setRight(subRight.getExpression());
setPredicate(subsetPredicate);
break;
case Formula.NOTSUBSETEQ:
final ANotSubsetPredicate notSubsetPredicate = new ANotSubsetPredicate();
notSubsetPredicate.setLeft(subLeft.getExpression());
notSubsetPredicate.setRight(subRight.getExpression());
setPredicate(notSubsetPredicate);
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
}
@Override
public void visitSimplePredicate(final SimplePredicate predicate) {
if (predicate.getTag() != Formula.KFINITE) {
throw new AssertionError(UNCOVERED_PREDICATE);
}
final AFinitePredicate finite = new AFinitePredicate();
final ExpressionVisitor subEx = new ExpressionVisitor(bounds);
predicate.getExpression().accept(subEx);
finite.setSet(subEx.getExpression());
setPredicate(finite);
}
@Override
public void visitUnaryPredicate(final UnaryPredicate predicate) {
if (predicate.getTag() != Formula.NOT) {
throw new AssertionError(UNCOVERED_PREDICATE);
}
final ANegationPredicate negationPredicate = new ANegationPredicate();
final PredicateVisitor sub = new PredicateVisitor(bounds);
predicate.getChild().accept(sub);
negationPredicate.setPredicate(sub.getPredicate());
setPredicate(negationPredicate);
}
@Override
public void visitMultiplePredicate(final MultiplePredicate predicate) {
final Expression[] subs = predicate.getChildren();
final List<PExpression> expressions = new ArrayList<PExpression>(
subs.length);
for (Expression e : subs) {
final ExpressionVisitor sub = new ExpressionVisitor(bounds);
e.accept(sub);
expressions.add(sub.getExpression());
}
final PPredicate result;
if (predicate.getTag() == Formula.KPARTITION) {
if (expressions.size() > 0) {
PExpression set = expressions.remove(0);
result = new APartitionPredicate(set, expressions);
} else {
throw new AssertionError("to few arguments for PARTITION");
}
} else {
throw new AssertionError(UNCOVERED_PREDICATE);
}
setPredicate(result);
}
@Override
public void visitExtendedPredicate(ExtendedPredicate predicate) {
AExtendedPredPredicate p = new AExtendedPredPredicate();
IPredicateExtension extension = predicate.getExtension();
String symbol = extension.getSyntaxSymbol();
// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
// Theories.addOrigin(origin);
p.setIdentifier(new TIdentifierLiteral(symbol));
Expression[] expressions = predicate.getChildExpressions();
List<PExpression> childExprs = new ArrayList<PExpression>();
for (Expression e : expressions) {
ExpressionVisitor v = new ExpressionVisitor(bounds);
e.accept(v);
childExprs.add(v.getExpression());
}
p.setExpressions(childExprs);
Predicate[] childPredicates = predicate.getChildPredicates();
List<PPredicate> childPreds = new ArrayList<PPredicate>();
for (Predicate pd : childPredicates) {
PredicateVisitor v = new PredicateVisitor(bounds);
pd.accept(v);
childPreds.add(v.getPredicate());
}
p.setPredicates(childPreds);
setPredicate(p);
}
}
/**
* (c) 2009 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
* Heinrich Heine Universitaet Duesseldorf
* This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
* */
package de.prob.eventb.translator.internal;
import org.eventb.core.ast.AssociativeExpression;
import org.eventb.core.ast.AssociativePredicate;
import org.eventb.core.ast.AtomicExpression;
import org.eventb.core.ast.BecomesEqualTo;
import org.eventb.core.ast.BecomesMemberOf;
import org.eventb.core.ast.BecomesSuchThat;
import org.eventb.core.ast.BinaryExpression;
import org.eventb.core.ast.BinaryPredicate;
import org.eventb.core.ast.BoolExpression;
import org.eventb.core.ast.BoundIdentDecl;
import org.eventb.core.ast.BoundIdentifier;
import org.eventb.core.ast.ExtendedExpression;
import org.eventb.core.ast.ExtendedPredicate;
import org.eventb.core.ast.FreeIdentifier;
import org.eventb.core.ast.ISimpleVisitor;
import org.eventb.core.ast.IntegerLiteral;
import org.eventb.core.ast.LiteralPredicate;
import org.eventb.core.ast.MultiplePredicate;
import org.eventb.core.ast.QuantifiedExpression;
import org.eventb.core.ast.QuantifiedPredicate;
import org.eventb.core.ast.RelationalPredicate;
import org.eventb.core.ast.SetExtension;
import org.eventb.core.ast.SimplePredicate;
import org.eventb.core.ast.UnaryExpression;
import org.eventb.core.ast.UnaryPredicate;
public class SimpleVisitorAdapter implements ISimpleVisitor {
public void visitAssociativeExpression(
final AssociativeExpression expression) {
// Default implementation does nothing
}
public void visitAssociativePredicate(final AssociativePredicate predicate) {
// Default implementation does nothing
}
public void visitAtomicExpression(final AtomicExpression expression) {
// Default implementation does nothing
}
public void visitBecomesEqualTo(final BecomesEqualTo assignment) {
// Default implementation does nothing
}
public void visitBecomesMemberOf(final BecomesMemberOf assignment) {
// Default implementation does nothing
}
public void visitBecomesSuchThat(final BecomesSuchThat assignment) {
// Default implementation does nothing
}
public void visitBinaryExpression(final BinaryExpression expression) {
// Default implementation does nothing
}
public void visitBinaryPredicate(final BinaryPredicate predicate) {
// Default implementation does nothing
}
public void visitBoolExpression(final BoolExpression expression) {
// Default implementation does nothing
}
public void visitBoundIdentDecl(final BoundIdentDecl boundIdentDecl) {
// Default implementation does nothing
}
public void visitBoundIdentifier(final BoundIdentifier identifierExpression) {
// Default implementation does nothing
}
public void visitFreeIdentifier(final FreeIdentifier identifierExpression) {
// Default implementation does nothing
}
public void visitIntegerLiteral(final IntegerLiteral expression) {
// Default implementation does nothing
}
public void visitLiteralPredicate(final LiteralPredicate predicate) {
// Default implementation does nothing
}
public void visitQuantifiedExpression(final QuantifiedExpression expression) {
// Default implementation does nothing
}
public void visitQuantifiedPredicate(final QuantifiedPredicate predicate) {
// Default implementation does nothing
}
public void visitRelationalPredicate(final RelationalPredicate predicate) {
// Default implementation does nothing
}
public void visitSetExtension(final SetExtension expression) {
// Default implementation does nothing
}
public void visitSimplePredicate(final SimplePredicate predicate) {
// Default implementation does nothing
}
public void visitUnaryExpression(final UnaryExpression expression) {
// Default implementation does nothing
}
public void visitUnaryPredicate(final UnaryPredicate predicate) {
// Default implementation does nothing
}
public void visitMultiplePredicate(final MultiplePredicate predicate) {
// Default implementation does nothing
}
@Override
public void visitExtendedExpression(final ExtendedExpression expression) {
// Default implementation does nothing
}
@Override
public void visitExtendedPredicate(final ExtendedPredicate predicate) {
// Default implementation does nothing
}
}
...@@ -722,76 +722,21 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -722,76 +722,21 @@ public class TranslationVisitor implements ISimpleVisitor {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
p.accept(visitor); p.accept(visitor);
final PPredicate newImp = visitor.getPredicate(); return visitor.getPredicate();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final PredicateVisitor oldVisitor = new PredicateVisitor();
p.accept(oldVisitor);
final PPredicate oldImp = oldVisitor.getPredicate();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
public static PExpression translateExpression(Expression e) { public static PExpression translateExpression(Expression e) {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
e.accept(visitor); e.accept(visitor);
final PExpression newImp = visitor.getExpression(); return visitor.getExpression();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final ExpressionVisitor oldVisitor = new ExpressionVisitor(
new LinkedList<String>());
e.accept(oldVisitor);
final PExpression oldImp = oldVisitor.getExpression();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
public static PSubstitution translateAssignment(Assignment a) { public static PSubstitution translateAssignment(Assignment a) {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
a.accept(visitor); a.accept(visitor);
final PSubstitution newImp = visitor.getSubstitution(); return visitor.getSubstitution();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final AssignmentVisitor oldVisitor = new AssignmentVisitor();
a.accept(oldVisitor);
final PSubstitution oldImp = oldVisitor.getSubstitution();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment