From 103260fc5f7a45e26730d699f62094f58b55cd87 Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Mon, 25 Feb 2013 14:18:38 +0100
Subject: [PATCH] Now using the TranslationVisitor, comparing with old version
---
.../eventb/translator/ContextTranslator.java | 6 ++-
.../translator/internal/ModelTranslator.java | 6 ++-
.../internal/TranslationVisitor.java | 39 ++++++++++++++++++-
3 files changed, 47 insertions(+), 4 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index 1aac0111..ed06174c 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -31,6 +31,7 @@ import org.eventb.core.ISCExtendsContext;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IConfidence;
import org.rodinp.core.IAttributeType;
import org.rodinp.core.IInternalElement;
@@ -61,6 +62,7 @@ import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.internal.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
+import de.prob.eventb.translator.internal.TranslationVisitor;
public final class ContextTranslator extends AbstractComponentTranslator {
@@ -382,8 +384,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
if (element.isTheorem() == theorems) {
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
- element.getPredicate(ff, te).accept(visitor);
+ final Predicate p = element.getPredicate(ff, te);
+ p.accept(visitor);
final PPredicate predicate = visitor.getPredicate();
+ TranslationVisitor.checkNewImplementation(p, predicate);
list.add(predicate);
labelMapping.put(predicate, element);
proofspragmas.add(new ClassifiedPragma("discharged", predicate,
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index 9677a309..5aaacd2a 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -430,6 +430,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
// + guardPredicate);
guardPredicate.accept(visitor);
final PPredicate predicate = visitor.getPredicate();
+ TranslationVisitor
+ .checkNewImplementation(guardPredicate, predicate);
if (guard.isTheorem()) {
theoremsList.add(predicate);
} else {
@@ -533,8 +535,10 @@ public class ModelTranslator extends AbstractComponentTranslator {
if (!isDefinedInAbstraction(evPredicate)) {
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
- evPredicate.getPredicate(ff, te).accept(visitor);
+ Predicate p = evPredicate.getPredicate(ff, te);
+ p.accept(visitor);
final PPredicate predicate = visitor.getPredicate();
+ TranslationVisitor.checkNewImplementation(p, predicate);
list.add(predicate);
labelMapping.put(predicate, evPredicate);
}
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 24f3ab26..29021e9d 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
@@ -328,8 +328,8 @@ public class TranslationVisitor implements ISimpleVisitor {
}
public void visitBinaryPredicate(final BinaryPredicate predicate) {
- final PPredicate right = getPredicate(predicate.getLeft());
- final PPredicate left = getPredicate(predicate.getRight());
+ final PPredicate left = getPredicate(predicate.getLeft());
+ final PPredicate right = getPredicate(predicate.getRight());
final PPredicate result;
switch (predicate.getTag()) {
case Formula.LIMP:
@@ -676,4 +676,39 @@ public class TranslationVisitor implements ISimpleVisitor {
}
}
+
+ public PPredicate getPredicate() {
+ assertExactStacksize(predicates);
+ return predicates.pop();
+ }
+
+ public PExpression getExpression() {
+ assertExactStacksize(expressions);
+ return expressions.pop();
+ }
+
+ public PSubstitution getSubstitution() {
+ assertExactStacksize(substitutions);
+ return substitutions.pop();
+ }
+
+ private void assertExactStacksize(LookupStack<?> stack) {
+ if (stack.size() != 1) {
+ throw new AssertionError(
+ "Exactly one element on the stack expected, but were "
+ + predicates.size());
+
+ }
+ }
+
+ public static void checkNewImplementation(Predicate p, PPredicate predicate) {
+ TranslationVisitor visitor = new TranslationVisitor();
+ p.accept(visitor);
+ final String expected = predicate.toString();
+ final String actual = visitor.getPredicate().toString();
+ if (!expected.equals(actual)) {
+ throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+ + actual);
+ }
+ }
}
--
GitLab