diff --git a/build.gradle b/build.gradle
index 24f66e2bc24719026909713ddf3a8f4c1c133131..5b7abb90cfca99441b7f6e763917304110c42ed0 100644
--- a/build.gradle
+++ b/build.gradle
@@ -36,7 +36,7 @@ project(':de.prob.core') {
}
- def parser_version = '2.4.21-SNAPSHOT'
+ def parser_version = '2.4.22-SNAPSHOT'
dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index 4fb87835bb61211c6f13c42745fc6dcf2a166ef5..5004b8808efadf10e19fa4e2470fc73ccdd87d92 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -4,17 +4,17 @@
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="bin"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.21-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.22-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.4.21-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.21-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/theorymapping-2.4.22-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.22-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 47a9e11897f2221bbb4a5bd469bd580c3a108d1f..f909299e5350c0dd7344b7c0f9de8f1aaa2ec559 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -118,14 +118,14 @@ Bundle-Activator: de.prob.core.internal.Activator
Eclipse-BuddyPolicy: registered
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ClassPath: .,
- lib/dependencies/unicode-2.4.21-SNAPSHOT.jar,
- lib/dependencies/theorymapping-2.4.21-SNAPSHOT.jar,
- lib/dependencies/prologlib-2.4.21-SNAPSHOT.jar,
- lib/dependencies/parserbase-2.4.21-SNAPSHOT.jar,
- lib/dependencies/ltlparser-2.4.21-SNAPSHOT.jar,
- lib/dependencies/cliparser-2.4.21-SNAPSHOT.jar,
- lib/dependencies/bparser-2.4.21-SNAPSHOT.jar,
- lib/dependencies/answerparser-2.4.21-SNAPSHOT.jar,
+ lib/dependencies/unicode-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/theorymapping-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/prologlib-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/parserbase-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/ltlparser-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/cliparser-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/bparser-2.4.22-SNAPSHOT.jar,
+ lib/dependencies/answerparser-2.4.22-SNAPSHOT.jar,
lib/dependencies/jgrapht-0.8.3.jar,
lib/dependencies/commons-codec-1.6.jar,
lib/dependencies/commons-lang-2.6.jar,
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..87d6fb7f4339bed2e99ffa60a56dff9a71875350 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
@@ -6,26 +6,63 @@
package de.prob.eventb.translator.internal;
-import java.util.*;
-
-import org.eventb.core.ast.*;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+
+import org.eventb.core.ast.Assignment;
+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.BooleanType;
+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.ExtendedPredicate;
+import org.eventb.core.ast.Formula;
+import org.eventb.core.ast.FreeIdentifier;
+import org.eventb.core.ast.GivenType;
+import org.eventb.core.ast.ISimpleVisitor;
+import org.eventb.core.ast.IntegerLiteral;
+import org.eventb.core.ast.IntegerType;
+import org.eventb.core.ast.LiteralPredicate;
+import org.eventb.core.ast.MultiplePredicate;
+import org.eventb.core.ast.ParametricType;
+import org.eventb.core.ast.PowerSetType;
+import org.eventb.core.ast.Predicate;
+import org.eventb.core.ast.ProductType;
+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.Type;
+import org.eventb.core.ast.UnaryExpression;
+import org.eventb.core.ast.UnaryPredicate;
+import org.eventb.core.ast.extension.IExpressionExtension;
import de.be4.classicalb.core.parser.node.*;
-import de.prob.eventb.translator.*;
/**
- * The global SuppressWarnings annotation is used because the deprecated code is
- * used to check if this new implementation computes the same results as the old
- * code.
- *
- * That should be removed after a while.
+ * This visitor on an Event-B AST generates an AST in ProB's format.
*
* @author plagge
*/
-@SuppressWarnings("deprecation")
public class TranslationVisitor implements ISimpleVisitor {
private static final String UNCOVERED_PREDICATE = "Uncovered Predicate";
+ private static final int[] EXTRA_TYPE_CONSTRUCTS = new int[] {
+ Formula.EMPTYSET, Formula.KPRJ1_GEN, Formula.KPRJ2_GEN,
+ Formula.KID_GEN };
+
private final LookupStack<PPredicate> predicates = new LookupStack<PPredicate>();
private final LookupStack<PExpression> expressions = new LookupStack<PExpression>();
private final LookupStack<PSubstitution> substitutions = new LookupStack<PSubstitution>();
@@ -62,7 +99,100 @@ public class TranslationVisitor implements ISimpleVisitor {
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
- expressions.push(result);
+ pushExpression(expression, result);
+ }
+
+ /**
+ * Push an expression on the stack. The original (not translated) expression
+ * is needed to check whether the expression should wrapped by a typeof(...)
+ * operator.
+ *
+ * @param original
+ * @param translated
+ */
+ private void pushExpression(Expression original, PExpression translated) {
+ final PExpression toPush;
+ if (original.getType() != null && shouldHaveExtraTypeInfo(original)) {
+ toPush = new ATypeofExpression(translated,
+ translateType(original.getType()));
+ } else {
+ toPush = translated;
+ }
+ expressions.push(toPush);
+ }
+
+ /**
+ * Check if this expression needs additional type information in the
+ * translation. This can be the e.g. case for {} or id
+ *
+ * @see #EXTRA_TYPE_CONSTRUCTS
+ * @param original
+ * @return <code>true</code> if the
+ */
+ private boolean shouldHaveExtraTypeInfo(Expression original) {
+ if (original instanceof ExtendedExpression) {
+ // We always wrap extended expressions
+ return true;
+ } else {
+ // Look into the list of constructs that need type information.
+ // A linear search shouldn't be problematic (or is maybe the fastest
+ // solution) because there are only a few elements.
+ int tag = original.getTag();
+ for (int i = 0; i < EXTRA_TYPE_CONSTRUCTS.length; i++) {
+ if (EXTRA_TYPE_CONSTRUCTS[i] == tag)
+ return true;
+ }
+ return false;
+ }
+ }
+
+ /**
+ * Translate a Event-B type to a corresponding ProB AST.
+ *
+ * This could theoretically directly be done by using
+ * {@link Type#toExpression(org.eventb.core.ast.FormulaFactory)} and
+ * translating that expression, but then we would need a formula factory.
+ *
+ * @param type
+ * the type to translate, never <code>null</code>
+ * @return the translated expression, never <code>null</code>
+ * @throws AssertionError
+ * if a type is encountered that cannot be translated
+ */
+ private PExpression translateType(Type type) {
+ final PExpression result;
+ if (type instanceof BooleanType) {
+ result = new ABoolSetExpression();
+ } else if (type instanceof GivenType) {
+ final String name = ((GivenType) type).getName();
+ result = createIdentifierExpression(name);
+ } else if (type instanceof IntegerType) {
+ result = new AIntegerSetExpression();
+ } else if (type instanceof PowerSetType) {
+ final Type a = ((PowerSetType) type).getBaseType();
+ result = new APowSubsetExpression(translateType(a));
+ } else if (type instanceof ProductType) {
+ final Type a = ((ProductType) type).getLeft();
+ final Type b = ((ProductType) type).getRight();
+ result = new ACartesianProductExpression(translateType(a),
+ translateType(b));
+ } else if (type instanceof ParametricType) {
+ final ParametricType pt = (ParametricType) type;
+ final IExpressionExtension ext = pt.getExprExtension();
+ final Type[] params = pt.getTypeParameters();
+ final List<PExpression> list = new ArrayList<PExpression>();
+ for (final Type param : params) {
+ list.add(translateType(param));
+ }
+ result = new AExtendedExprExpression(new TIdentifierLiteral(
+ ext.getSyntaxSymbol()), list,
+ Collections.<PPredicate> emptyList());
+ } else {
+ throw new AssertionError(
+ "Don't know how to handle the Event-B type of class "
+ + type.getClass().getCanonicalName());
+ }
+ return result;
}
private PExpression recurseFCOMP(final List<PExpression> list) {
@@ -188,7 +318,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default:
throw new AssertionError("Uncovered Expression " + expression);
}
- expressions.push(result);
+ pushExpression(expression, result);
}
@Override
@@ -313,7 +443,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default:
throw new AssertionError("Uncovered Expression");
}
- expressions.push(result);
+ pushExpression(expression, result);
}
@Override
@@ -337,7 +467,7 @@ public class TranslationVisitor implements ISimpleVisitor {
@Override
public void visitBoolExpression(final BoolExpression expression) {
final PPredicate pred = getPredicate(expression.getPredicate());
- expressions.push(new AConvertBoolExpression(pred));
+ pushExpression(expression, new AConvertBoolExpression(pred));
}
@Override
@@ -357,19 +487,20 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitBoundIdentifier(final BoundIdentifier identifierExpression) {
final String name = boundVariables.get(identifierExpression
.getBoundIndex());
- expressions.push(createIdentifierExpression(name));
+ pushExpression(identifierExpression, createIdentifierExpression(name));
}
@Override
public void visitFreeIdentifier(final FreeIdentifier identifierExpression) {
- expressions.push(createIdentifierExpression(identifierExpression
- .getName()));
+ pushExpression(identifierExpression,
+ createIdentifierExpression(identifierExpression.getName()));
}
@Override
public void visitIntegerLiteral(final IntegerLiteral expression) {
final String value = expression.getValue().toString();
- expressions.push(new AIntegerExpression(new TIntegerLiteral(value)));
+ pushExpression(expression, new AIntegerExpression(new TIntegerLiteral(
+ value)));
}
@Override
@@ -392,28 +523,30 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitQuantifiedExpression(final QuantifiedExpression expression) {
// Add quantified identifiers to bound list and recursively create
// subtrees representing the identifiers
- int originalBoundSize = boundVariables.size();
- final List<PExpression> list = getSubExpressions(expression
- .getBoundIdentDecls());
+ final int originalBoundSize = boundVariables.size();
+ final BoundIdentDecl[] decls = expression.getBoundIdentDecls();
+ final List<PExpression> list = getSubExpressions(decls);
final PPredicate pr = getPredicate(expression.getPredicate());
final PExpression ex = getExpression(expression.getExpression());
boundVariables.shrinkToSize(originalBoundSize);
+ final PPredicate pred = addTypesToPredicate(pr, decls);
+
final PExpression result;
switch (expression.getTag()) {
case Formula.QUNION:
- result = new AQuantifiedUnionExpression(list, pr, ex);
+ result = new AQuantifiedUnionExpression(list, pred, ex);
break;
case Formula.QINTER:
- result = new AQuantifiedIntersectionExpression(list, pr, ex);
+ result = new AQuantifiedIntersectionExpression(list, pred, ex);
break;
case Formula.CSET:
- result = new AEventBComprehensionSetExpression(list, ex, pr);
+ result = new AEventBComprehensionSetExpression(list, ex, pred);
break;
default:
throw new AssertionError(UNCOVERED_PREDICATE);
}
- expressions.push(result);
+ pushExpression(expression, result);
}
@Override
@@ -421,8 +554,8 @@ public class TranslationVisitor implements ISimpleVisitor {
// Add quantified identifiers to bound list and recursively create
// subtrees representing the identifiers
int originalBoundSize = boundVariables.size();
- final List<PExpression> list = getSubExpressions(predicate
- .getBoundIdentDecls());
+ final BoundIdentDecl[] decls = predicate.getBoundIdentDecls();
+ final List<PExpression> list = getSubExpressions(decls);
// Recursively analyze the predicate (important, bounds are already set)
final PPredicate pred = getPredicate(predicate.getPredicate());
boundVariables.shrinkToSize(originalBoundSize);
@@ -430,11 +563,22 @@ public class TranslationVisitor implements ISimpleVisitor {
final PPredicate result;
switch (predicate.getTag()) {
case Formula.EXISTS:
- result = new AExistsPredicate(list, pred);
+ result = new AExistsPredicate(list,
+ addTypesToPredicate(pred, decls));
break;
case Formula.FORALL:
- final PPredicate impl = pred instanceof AImplicationPredicate ? pred
- : new AImplicationPredicate(new ATruthPredicate(), pred);
+ final PPredicate left;
+ final PPredicate right;
+ if (pred instanceof AImplicationPredicate) {
+ final AImplicationPredicate i = (AImplicationPredicate) pred;
+ left = addTypesToPredicate(i.getLeft(), decls);
+ right = i.getRight();
+ } else {
+ left = addTypesToPredicate(null, decls);
+ right = pred;
+ }
+ final PPredicate impl = new AImplicationPredicate(
+ left != null ? left : new ATruthPredicate(), right);
result = new AForallPredicate(list, impl);
break;
default:
@@ -443,6 +587,51 @@ public class TranslationVisitor implements ISimpleVisitor {
predicates.push(result);
}
+ /**
+ * If we have declarations of x and y with types S resp. T, add the type
+ * information to the original predicate P. The result would be
+ * <code>x:S & (y:T & P)</code>.
+ *
+ * If decls is empty, the original predicate is returned unmodified.
+ *
+ * An alternative approach to this would be adding the type information
+ * directly to the identifiers with an oftype expression. The AST allows
+ * this because it expects expressions in the list of declarations. But the
+ * type checker must be adapted. The approach here makes (arguably) stronger
+ * modifications to the structure of the AST.
+ *
+ * @param predicate
+ * the original predicate, <code>null</code> if no original
+ * predicate is used.
+ * @param decls
+ * a list of declarations, never <code>null</code>
+ * @return the original predicate plus type information, <code>null</code>
+ * if no original predicate is given and decls is empty
+ */
+ private PPredicate addTypesToPredicate(PPredicate predicate,
+ BoundIdentDecl[] decls) {
+ for (int i = decls.length; i > 0; i--) {
+ final BoundIdentDecl decl = decls[i - 1];
+ final Type type = decl.getType();
+ // I've encountered null types. Maybe that was a bug but just to be
+ // sure (in most cases, missing type information won't hurt):
+ if (type != null) {
+ // put a translation of the identifier on the stack ...
+ decl.accept(this);
+ // ... and take it
+ final PExpression expr = expressions.pop();
+ // construct "expr:type"
+ final PPredicate member = new AMemberPredicate(expr,
+ translateType(type));
+ // and P := "expr:type & P", if no P is given (predicate is
+ // null), just "expr:type"
+ predicate = predicate == null ? member
+ : new AConjunctPredicate(member, predicate);
+ }
+ }
+ return predicate;
+ }
+
@Override
public void visitRelationalPredicate(final RelationalPredicate predicate) {
// EQUAL, NOTEQUAL, LT, LE, GT, GE, IN, NOTIN, SUBSET,
@@ -497,7 +686,7 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitSetExtension(final SetExtension expression) {
final Expression[] members = expression.getMembers();
final List<PExpression> list = getSubExpressions(members);
- expressions.push(new ASetExtensionExpression(list));
+ pushExpression(expression, new ASetExtensionExpression(list));
}
@Override
@@ -512,6 +701,7 @@ public class TranslationVisitor implements ISimpleVisitor {
predicates.push(result);
}
+ @SuppressWarnings("deprecation")
@Override
public void visitUnaryExpression(final UnaryExpression expression) {
final PExpression exp = getExpression(expression.getChild());
@@ -562,7 +752,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default:
throw new AssertionError("Uncovered Expression");
}
- expressions.push(result);
+ pushExpression(expression, result);
}
@Override
@@ -601,8 +791,8 @@ public class TranslationVisitor implements ISimpleVisitor {
.getChildExpressions());
List<PPredicate> childPreds = getSubPredicates(expression
.getChildPredicates());
- expressions.push(new AExtendedExprExpression(new TIdentifierLiteral(
- symbol), childExprs, childPreds));
+ pushExpression(expression, new AExtendedExprExpression(
+ new TIdentifierLiteral(symbol), childExprs, childPreds));
}
@Override
@@ -722,76 +912,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();
}
}