From 967dbd5f9655fe954865f6cbf026130a23a7eec8 Mon Sep 17 00:00:00 2001
From: Daniel Plagge <plagge@cs.uni-duesseldorf.de>
Date: Tue, 8 Jan 2013 07:29:27 +0100
Subject: [PATCH] Getting Type Environment now from the model or context, not
using the default. Introduced two distinct constructors for ContextTranslator
to handle ISCContextRoot and ISCInternalContext properly.
---
.../eventb/translator/ContextTranslator.java | 124 ++++++++++++------
.../internal/EventBMachineTranslator.java | 18 ++-
2 files changed, 94 insertions(+), 48 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 e65b7464..87595710 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -15,6 +15,7 @@ import java.util.Map;
import org.eclipse.core.runtime.Assert;
import org.eventb.core.IContextRoot;
+import org.eventb.core.IEventBRoot;
import org.eventb.core.IExtendsContext;
import org.eventb.core.ILabeledElement;
import org.eventb.core.IPOSequent;
@@ -28,11 +29,11 @@ import org.eventb.core.ISCContext;
import org.eventb.core.ISCContextRoot;
import org.eventb.core.ISCExtendsContext;
import org.eventb.core.ISCInternalContext;
-import org.eventb.core.ISCMachineRoot;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.seqprover.IConfidence;
import org.rodinp.core.IAttributeType;
+import org.rodinp.core.IInternalElement;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.IRodinProject;
@@ -71,17 +72,70 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
private final List<IPragma> pragmas = new ArrayList<IPragma>();
- public static ContextTranslator create(final ISCContext context)
+ private final IEventBRoot root;
+ private final FormulaFactory ff;
+ private final ITypeEnvironment te;
+
+ public static ContextTranslator create(final ISCContextRoot context)
+ throws TranslationFailedException {
+ try {
+ assertConsistentModel(context);
+ final FormulaFactory ff = context.getFormulaFactory();
+ final ITypeEnvironment te = context.getTypeEnvironment(ff);
+ final ContextTranslator translator = new ContextTranslator(context,
+ ff, te, context);
+ translator.translate();
+ return translator;
+ } catch (RodinDBException e) {
+ throw createTranslationFailedException(context, e);
+ }
+ }
+
+ public static ContextTranslator create(final ISCInternalContext context,
+ final FormulaFactory ff, final ITypeEnvironment te)
throws TranslationFailedException {
- ContextTranslator contextTranslator = new ContextTranslator(context);
+ final IEventBRoot root = getRootContext(context);
+ final ContextTranslator translator = new ContextTranslator(context, ff,
+ te, root);
try {
- contextTranslator.translate();
+ assertConsistentModel(context.getRoot());
+ translator.translate();
} catch (RodinDBException e) {
- final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
- throw new TranslationFailedException(context.getComponentName(),
- message + e.getLocalizedMessage());
+ throw createTranslationFailedException(context, e);
}
- return contextTranslator;
+ return translator;
+ }
+
+ private static IEventBRoot getRootContext(ISCInternalContext context) {
+ try {
+ String elementName = context.getElementName();
+ IRodinProject rodinProject = context.getRodinProject();
+ IRodinFile rodinFile = rodinProject.getRodinFile(elementName
+ + ".bcc");
+ if (rodinFile.exists()) {
+ final IInternalElement element = rodinFile.getRoot();
+ if (element instanceof IEventBRoot) {
+ return (IEventBRoot) element;
+ }
+ }
+ } catch (Exception e) {
+ // We do not guarantee to include proof infos. If something goes
+ // wrong, we ignore the Proof info.
+ }
+ return null;
+ }
+
+ private static TranslationFailedException createTranslationFailedException(
+ final ISCContext context, RodinDBException e)
+ throws TranslationFailedException {
+ final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
+ return new TranslationFailedException(context.getComponentName(),
+ message + e.getLocalizedMessage());
+ }
+
+ private static boolean assertConsistentModel(IInternalElement machine_root)
+ throws RodinDBException {
+ return Assert.isTrue(machine_root.getRodinFile().isConsistent());
}
/**
@@ -91,41 +145,27 @@ public final class ContextTranslator extends AbstractComponentTranslator {
* contains errors)
*
* @param context
+ * The context to translate
+ * @param ff
+ * The FormulaFactory needed to extract the predicates
+ * @param te
+ * The TypeEnvironment needed to extract the predicates
+ * @param root
+ * the root to access the proofs
* @throws TranslationFailedException
- * @throws RodinDBException
*/
- private ContextTranslator(final ISCContext context)
- throws TranslationFailedException {
+ private ContextTranslator(final ISCContext context,
+ final FormulaFactory ff, final ITypeEnvironment te,
+ final IEventBRoot root) throws TranslationFailedException {
this.context = context;
+ this.ff = ff;
+ this.te = te;
+ this.root = root;
}
private void translate() throws RodinDBException {
- if (context instanceof ISCContextRoot) {
- ISCContextRoot context_root = (ISCContextRoot) context;
- Assert.isTrue(context_root.getRodinFile().isConsistent());
- } else if (context instanceof ISCInternalContext) {
- ISCInternalContext context_internal = (ISCInternalContext) context;
-
- try {
-
- String elementName = context_internal.getElementName();
- IRodinProject rodinProject = context_internal.getRodinProject();
- IRodinFile rodinFile = rodinProject.getRodinFile(elementName
- + ".bcc");
- if (rodinFile.exists()) {
- ISCContextRoot root = (ISCContextRoot) rodinFile.getRoot();
- collectProofInfo(root);
- }
- } catch (Exception e) {
- // We do not guarantee to include proof infos. If something goes
- // wrong, we ignore the Proof info.
- }
-
- ISCMachineRoot machine_root = (ISCMachineRoot) context_internal
- .getRoot();
- Assert.isTrue(machine_root.getRodinFile().isConsistent());
- }
translateContext();
+ collectProofInfo();
collectPragmas();
}
@@ -148,8 +188,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
}
- private void collectProofInfo(ISCContextRoot origin)
- throws RodinDBException {
+ private void collectProofInfo() throws RodinDBException {
+ if (root != null) {
+ collectProofInfo(root);
+ }
+ }
+
+ private void collectProofInfo(IEventBRoot origin) throws RodinDBException {
IPSRoot proofStatus = origin.getPSRoot();
IPSStatus[] statuses = proofStatus.getStatuses();
@@ -334,8 +379,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
final PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>());
- final FormulaFactory ff = FormulaFactory.getDefault();
- final ITypeEnvironment te = ff.makeTypeEnvironment();
element.getPredicate(ff, te).accept(visitor);
final PPredicate predicate = visitor.getPredicate();
list.add(predicate);
@@ -352,7 +395,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
public List<IPragma> getPragmas() {
- // TODO Auto-generated method stub
return pragmas;
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
index 1b9e5fb6..845e660e 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBMachineTranslator.java
@@ -11,6 +11,8 @@ import java.util.List;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.RodinDBException;
@@ -103,12 +105,13 @@ public final class EventBMachineTranslator extends EventBTranslator {
final List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
final List<String> processed = new ArrayList<String>();
- for (ISCMachineRoot m : models) {
- ISCInternalContext[] seenContexts;
+ for (final ISCMachineRoot m : models) {
try {
- seenContexts = m.getSCSeenContexts();
- for (ISCInternalContext seenContext : seenContexts) {
- collectContexts(translators, processed, seenContext);
+ final FormulaFactory ff = m.getFormulaFactory();
+ final ITypeEnvironment te = m.getTypeEnvironment(ff);
+ final ISCInternalContext[] seenContexts = m.getSCSeenContexts();
+ for (final ISCInternalContext seenContext : seenContexts) {
+ collectContexts(translators, processed, seenContext, ff, te);
}
} catch (RodinDBException e) {
throw new TranslationFailedException(e);
@@ -118,12 +121,13 @@ public final class EventBMachineTranslator extends EventBTranslator {
}
private void collectContexts(final List<ContextTranslator> translatorMap,
- final List<String> processed, final ISCInternalContext context)
+ final List<String> processed, final ISCInternalContext context,
+ final FormulaFactory ff, final ITypeEnvironment te)
throws TranslationFailedException {
String name = context.getElementName();
if (!processed.contains(name)) {
processed.add(name);
- translatorMap.add(ContextTranslator.create(context));
+ translatorMap.add(ContextTranslator.create(context, ff, te));
}
}
--
GitLab