Skip to content
Snippets Groups Projects
Commit 24e5cdb7 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

Merge branch 'develop' into rodin3

parents 210a02ca b7efcd85
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 244 additions and 1586 deletions
build.gradle
+ 1
− 1
View file @ 24e5cdb7
...@@ -36,7 +36,7 @@ project(':de.prob.core') { ...@@ -36,7 +36,7 @@ project(':de.prob.core') {
} }
def parser_version = '2.4.21-SNAPSHOT' def parser_version = '2.4.22-SNAPSHOT'
dependencies { dependencies {
compile group: "de.prob", name: "answerparser", version: parser_version , changing: true compile group: "de.prob", name: "answerparser", version: parser_version , changing: true
......
de.prob.core/.classpath
+ 8
− 8
View file @ 24e5cdb7
...@@ -4,17 +4,17 @@ ...@@ -4,17 +4,17 @@
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/> <classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/> <classpathentry kind="src" path="src"/>
<classpathentry kind="output" path="bin"/> <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/answerparser-2.4.22-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.21-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.21-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-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/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/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/ltlparser-2.4.22-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.21-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.21-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.21-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.21-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/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/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/> <classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
......
de.prob.core/META-INF/MANIFEST.MF
+ 8
− 8
View file @ 24e5cdb7
...@@ -118,14 +118,14 @@ Bundle-Activator: de.prob.core.internal.Activator ...@@ -118,14 +118,14 @@ Bundle-Activator: de.prob.core.internal.Activator
Eclipse-BuddyPolicy: registered Eclipse-BuddyPolicy: registered
Bundle-RequiredExecutionEnvironment: JavaSE-1.6 Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ClassPath: ., Bundle-ClassPath: .,
lib/dependencies/unicode-2.4.21-SNAPSHOT.jar, lib/dependencies/unicode-2.4.22-SNAPSHOT.jar,
lib/dependencies/theorymapping-2.4.21-SNAPSHOT.jar, lib/dependencies/theorymapping-2.4.22-SNAPSHOT.jar,
lib/dependencies/prologlib-2.4.21-SNAPSHOT.jar, lib/dependencies/prologlib-2.4.22-SNAPSHOT.jar,
lib/dependencies/parserbase-2.4.21-SNAPSHOT.jar, lib/dependencies/parserbase-2.4.22-SNAPSHOT.jar,
lib/dependencies/ltlparser-2.4.21-SNAPSHOT.jar, lib/dependencies/ltlparser-2.4.22-SNAPSHOT.jar,
lib/dependencies/cliparser-2.4.21-SNAPSHOT.jar, lib/dependencies/cliparser-2.4.22-SNAPSHOT.jar,
lib/dependencies/bparser-2.4.21-SNAPSHOT.jar, lib/dependencies/bparser-2.4.22-SNAPSHOT.jar,
lib/dependencies/answerparser-2.4.21-SNAPSHOT.jar, lib/dependencies/answerparser-2.4.22-SNAPSHOT.jar,
lib/dependencies/jgrapht-0.8.3.jar, lib/dependencies/jgrapht-0.8.3.jar,
lib/dependencies/commons-codec-1.6.jar, lib/dependencies/commons-codec-1.6.jar,
lib/dependencies/commons-lang-2.6.jar, lib/dependencies/commons-lang-2.6.jar,
......
de.prob.core/src/de/prob/eventb/translator/AssignmentVisitor.java deleted 100644 → 0
+ 0
− 129
View file @ 210a02ca
/**
* (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);
}
}
de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java deleted 100644 → 0
+ 0
− 738
View file @ 210a02ca
This diff is collapsed.
de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java deleted 100644 → 0
+ 0
− 453
View file @ 210a02ca
/**
* (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);
}
}
de.prob.core/src/de/prob/eventb/translator/internal/SimpleVisitorAdapter.java deleted 100644 → 0
+ 0
− 157
View file @ 210a02ca
/**
* (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
}
}
de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java
+ 227
− 92
View file @ 24e5cdb7
...@@ -6,26 +6,63 @@ ...@@ -6,26 +6,63 @@
package de.prob.eventb.translator.internal; package de.prob.eventb.translator.internal;
import java.util.*; import java.util.ArrayList;
import java.util.Arrays;
import org.eventb.core.ast.*; 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.be4.classicalb.core.parser.node.*;
import de.prob.eventb.translator.*;
/** /**
* The global SuppressWarnings annotation is used because the deprecated code is * This visitor on an Event-B AST generates an AST in ProB's format.
* used to check if this new implementation computes the same results as the old
* code.
*
* That should be removed after a while.
* *
* @author plagge * @author plagge
*/ */
@SuppressWarnings("deprecation")
public class TranslationVisitor implements ISimpleVisitor { public class TranslationVisitor implements ISimpleVisitor {
private static final String UNCOVERED_PREDICATE = "Uncovered Predicate"; 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<PPredicate> predicates = new LookupStack<PPredicate>();
private final LookupStack<PExpression> expressions = new LookupStack<PExpression>(); private final LookupStack<PExpression> expressions = new LookupStack<PExpression>();
private final LookupStack<PSubstitution> substitutions = new LookupStack<PSubstitution>(); private final LookupStack<PSubstitution> substitutions = new LookupStack<PSubstitution>();
...@@ -62,7 +99,100 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -62,7 +99,100 @@ public class TranslationVisitor implements ISimpleVisitor {
default: default:
throw new AssertionError(UNCOVERED_PREDICATE); 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) { private PExpression recurseFCOMP(final List<PExpression> list) {
...@@ -188,7 +318,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -188,7 +318,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default: default:
throw new AssertionError("Uncovered Expression " + expression); throw new AssertionError("Uncovered Expression " + expression);
} }
expressions.push(result); pushExpression(expression, result);
} }
@Override @Override
...@@ -313,7 +443,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -313,7 +443,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default: default:
throw new AssertionError("Uncovered Expression"); throw new AssertionError("Uncovered Expression");
} }
expressions.push(result); pushExpression(expression, result);
} }
@Override @Override
...@@ -337,7 +467,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -337,7 +467,7 @@ public class TranslationVisitor implements ISimpleVisitor {
@Override @Override
public void visitBoolExpression(final BoolExpression expression) { public void visitBoolExpression(final BoolExpression expression) {
final PPredicate pred = getPredicate(expression.getPredicate()); final PPredicate pred = getPredicate(expression.getPredicate());
expressions.push(new AConvertBoolExpression(pred)); pushExpression(expression, new AConvertBoolExpression(pred));
} }
@Override @Override
...@@ -357,19 +487,20 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -357,19 +487,20 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitBoundIdentifier(final BoundIdentifier identifierExpression) { public void visitBoundIdentifier(final BoundIdentifier identifierExpression) {
final String name = boundVariables.get(identifierExpression final String name = boundVariables.get(identifierExpression
.getBoundIndex()); .getBoundIndex());
expressions.push(createIdentifierExpression(name)); pushExpression(identifierExpression, createIdentifierExpression(name));
} }
@Override @Override
public void visitFreeIdentifier(final FreeIdentifier identifierExpression) { public void visitFreeIdentifier(final FreeIdentifier identifierExpression) {
expressions.push(createIdentifierExpression(identifierExpression pushExpression(identifierExpression,
.getName())); createIdentifierExpression(identifierExpression.getName()));
} }
@Override @Override
public void visitIntegerLiteral(final IntegerLiteral expression) { public void visitIntegerLiteral(final IntegerLiteral expression) {
final String value = expression.getValue().toString(); final String value = expression.getValue().toString();
expressions.push(new AIntegerExpression(new TIntegerLiteral(value))); pushExpression(expression, new AIntegerExpression(new TIntegerLiteral(
value)));
} }
@Override @Override
...@@ -392,28 +523,30 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -392,28 +523,30 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitQuantifiedExpression(final QuantifiedExpression expression) { public void visitQuantifiedExpression(final QuantifiedExpression expression) {
// Add quantified identifiers to bound list and recursively create // Add quantified identifiers to bound list and recursively create
// subtrees representing the identifiers // subtrees representing the identifiers
int originalBoundSize = boundVariables.size(); final int originalBoundSize = boundVariables.size();
final List<PExpression> list = getSubExpressions(expression final BoundIdentDecl[] decls = expression.getBoundIdentDecls();
.getBoundIdentDecls()); final List<PExpression> list = getSubExpressions(decls);
final PPredicate pr = getPredicate(expression.getPredicate()); final PPredicate pr = getPredicate(expression.getPredicate());
final PExpression ex = getExpression(expression.getExpression()); final PExpression ex = getExpression(expression.getExpression());
boundVariables.shrinkToSize(originalBoundSize); boundVariables.shrinkToSize(originalBoundSize);
final PPredicate pred = addTypesToPredicate(pr, decls);
final PExpression result; final PExpression result;
switch (expression.getTag()) { switch (expression.getTag()) {
case Formula.QUNION: case Formula.QUNION:
result = new AQuantifiedUnionExpression(list, pr, ex); result = new AQuantifiedUnionExpression(list, pred, ex);
break; break;
case Formula.QINTER: case Formula.QINTER:
result = new AQuantifiedIntersectionExpression(list, pr, ex); result = new AQuantifiedIntersectionExpression(list, pred, ex);
break; break;
case Formula.CSET: case Formula.CSET:
result = new AEventBComprehensionSetExpression(list, ex, pr); result = new AEventBComprehensionSetExpression(list, ex, pred);
break; break;
default: default:
throw new AssertionError(UNCOVERED_PREDICATE); throw new AssertionError(UNCOVERED_PREDICATE);
} }
expressions.push(result); pushExpression(expression, result);
} }
@Override @Override
...@@ -421,8 +554,8 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -421,8 +554,8 @@ public class TranslationVisitor implements ISimpleVisitor {
// Add quantified identifiers to bound list and recursively create // Add quantified identifiers to bound list and recursively create
// subtrees representing the identifiers // subtrees representing the identifiers
int originalBoundSize = boundVariables.size(); int originalBoundSize = boundVariables.size();
final List<PExpression> list = getSubExpressions(predicate final BoundIdentDecl[] decls = predicate.getBoundIdentDecls();
.getBoundIdentDecls()); final List<PExpression> list = getSubExpressions(decls);
// Recursively analyze the predicate (important, bounds are already set) // Recursively analyze the predicate (important, bounds are already set)
final PPredicate pred = getPredicate(predicate.getPredicate()); final PPredicate pred = getPredicate(predicate.getPredicate());
boundVariables.shrinkToSize(originalBoundSize); boundVariables.shrinkToSize(originalBoundSize);
...@@ -430,11 +563,22 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -430,11 +563,22 @@ public class TranslationVisitor implements ISimpleVisitor {
final PPredicate result; final PPredicate result;
switch (predicate.getTag()) { switch (predicate.getTag()) {
case Formula.EXISTS: case Formula.EXISTS:
result = new AExistsPredicate(list, pred); result = new AExistsPredicate(list,
addTypesToPredicate(pred, decls));
break; break;
case Formula.FORALL: case Formula.FORALL:
final PPredicate impl = pred instanceof AImplicationPredicate ? pred final PPredicate left;
: new AImplicationPredicate(new ATruthPredicate(), pred); 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); result = new AForallPredicate(list, impl);
break; break;
default: default:
...@@ -443,6 +587,51 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -443,6 +587,51 @@ public class TranslationVisitor implements ISimpleVisitor {
predicates.push(result); 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 @Override
public void visitRelationalPredicate(final RelationalPredicate predicate) { public void visitRelationalPredicate(final RelationalPredicate predicate) {
// EQUAL, NOTEQUAL, LT, LE, GT, GE, IN, NOTIN, SUBSET, // EQUAL, NOTEQUAL, LT, LE, GT, GE, IN, NOTIN, SUBSET,
...@@ -497,7 +686,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -497,7 +686,7 @@ public class TranslationVisitor implements ISimpleVisitor {
public void visitSetExtension(final SetExtension expression) { public void visitSetExtension(final SetExtension expression) {
final Expression[] members = expression.getMembers(); final Expression[] members = expression.getMembers();
final List<PExpression> list = getSubExpressions(members); final List<PExpression> list = getSubExpressions(members);
expressions.push(new ASetExtensionExpression(list)); pushExpression(expression, new ASetExtensionExpression(list));
} }
@Override @Override
...@@ -512,6 +701,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -512,6 +701,7 @@ public class TranslationVisitor implements ISimpleVisitor {
predicates.push(result); predicates.push(result);
} }
@SuppressWarnings("deprecation")
@Override @Override
public void visitUnaryExpression(final UnaryExpression expression) { public void visitUnaryExpression(final UnaryExpression expression) {
final PExpression exp = getExpression(expression.getChild()); final PExpression exp = getExpression(expression.getChild());
...@@ -562,7 +752,7 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -562,7 +752,7 @@ public class TranslationVisitor implements ISimpleVisitor {
default: default:
throw new AssertionError("Uncovered Expression"); throw new AssertionError("Uncovered Expression");
} }
expressions.push(result); pushExpression(expression, result);
} }
@Override @Override
...@@ -601,8 +791,8 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -601,8 +791,8 @@ public class TranslationVisitor implements ISimpleVisitor {
.getChildExpressions()); .getChildExpressions());
List<PPredicate> childPreds = getSubPredicates(expression List<PPredicate> childPreds = getSubPredicates(expression
.getChildPredicates()); .getChildPredicates());
expressions.push(new AExtendedExprExpression(new TIdentifierLiteral( pushExpression(expression, new AExtendedExprExpression(
symbol), childExprs, childPreds)); new TIdentifierLiteral(symbol), childExprs, childPreds));
} }
@Override @Override
...@@ -722,76 +912,21 @@ public class TranslationVisitor implements ISimpleVisitor { ...@@ -722,76 +912,21 @@ public class TranslationVisitor implements ISimpleVisitor {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
p.accept(visitor); p.accept(visitor);
final PPredicate newImp = visitor.getPredicate(); return visitor.getPredicate();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final PredicateVisitor oldVisitor = new PredicateVisitor();
p.accept(oldVisitor);
final PPredicate oldImp = oldVisitor.getPredicate();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
public static PExpression translateExpression(Expression e) { public static PExpression translateExpression(Expression e) {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
e.accept(visitor); e.accept(visitor);
final PExpression newImp = visitor.getExpression(); return visitor.getExpression();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final ExpressionVisitor oldVisitor = new ExpressionVisitor(
new LinkedList<String>());
e.accept(oldVisitor);
final PExpression oldImp = oldVisitor.getExpression();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
public static PSubstitution translateAssignment(Assignment a) { public static PSubstitution translateAssignment(Assignment a) {
// Create a visitor and use it to translate the predicate // Create a visitor and use it to translate the predicate
final TranslationVisitor visitor = new TranslationVisitor(); final TranslationVisitor visitor = new TranslationVisitor();
a.accept(visitor); a.accept(visitor);
final PSubstitution newImp = visitor.getSubstitution(); return visitor.getSubstitution();
// Use the old visitor to check if the implementation of the new visitor
// is correct.
final AssignmentVisitor oldVisitor = new AssignmentVisitor();
a.accept(oldVisitor);
final PSubstitution oldImp = oldVisitor.getSubstitution();
// Compare both results. If there are differences, throw an exception
final String expected = oldImp.toString();
final String actual = newImp.toString();
if (!expected.equals(actual)) {
throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ actual);
}
// TODO[DP, 13.8.2013]: Remove call to old implementation after a test
// phase
return newImp;
} }
} }
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment