diff --git a/de.prob.core/src/de/prob/eventb/translator/AssignmentVisitor.java b/de.prob.core/src/de/prob/eventb/translator/AssignmentVisitor.java deleted file mode 100644 index e8a27f81a6032b317c658c82321e8a64e6b5362d..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/eventb/translator/AssignmentVisitor.java +++ /dev/null @@ -1,129 +0,0 @@ -/** - * (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); - - } -} diff --git a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java deleted file mode 100644 index 810f101003238e6cabb94e4f3504956201f535f0..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java +++ /dev/null @@ -1,738 +0,0 @@ -/** - * (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"); - } - } -} diff --git a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java deleted file mode 100644 index a4c8e75bb629b52048bf7b055cec3f68b2157ba6..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java +++ /dev/null @@ -1,453 +0,0 @@ -/** - * (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); - } - -} diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/SimpleVisitorAdapter.java b/de.prob.core/src/de/prob/eventb/translator/internal/SimpleVisitorAdapter.java deleted file mode 100644 index b6b186285f102b1336e76d5686360313ec31dfef..0000000000000000000000000000000000000000 --- a/de.prob.core/src/de/prob/eventb/translator/internal/SimpleVisitorAdapter.java +++ /dev/null @@ -1,157 +0,0 @@ -/** - * (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 - } - -} diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java index 1c6801c97f5e9da610531a5f9d8834dd3641504d..7e52b68531f0acf77f3ca1fbb0551158259be442 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java @@ -722,76 +722,21 @@ public class TranslationVisitor implements ISimpleVisitor { // Create a visitor and use it to translate the predicate final TranslationVisitor visitor = new TranslationVisitor(); p.accept(visitor); - final PPredicate newImp = 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; + return visitor.getPredicate(); } public static PExpression translateExpression(Expression e) { // Create a visitor and use it to translate the predicate final TranslationVisitor visitor = new TranslationVisitor(); e.accept(visitor); - final PExpression newImp = 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; + return visitor.getExpression(); } public static PSubstitution translateAssignment(Assignment a) { // Create a visitor and use it to translate the predicate final TranslationVisitor visitor = new TranslationVisitor(); a.accept(visitor); - final PSubstitution newImp = 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; + return visitor.getSubstitution(); } }