diff --git a/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java b/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java
new file mode 100644
index 0000000000000000000000000000000000000000..8f166ba9eb6b292cac18d69d1dfd90f5d2c78d6a
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java
@@ -0,0 +1,9 @@
+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public interface IPragma {
+
+ void output(IPrologTermOutput pout);
+
+}
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 ad5b33afb304accdbaa9f275db0e8a47d91b6707..62fb49e49dde23f2d56b267667e0184f5c607a6e 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -53,6 +53,7 @@ import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.prob.core.translator.TranslationFailedException;
+import de.prob.core.translator.pragmas.IPragma;
import de.prob.eventb.translator.internal.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
@@ -65,6 +66,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
+ private final List<IPragma> pragmas = new ArrayList<IPragma>();
public static ContextTranslator create(final ISCContext context)
throws TranslationFailedException {
@@ -110,6 +112,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
if (rodinFile.exists()) {
ISCContextRoot root = (ISCContextRoot) rodinFile.getRoot();
collectProofInfo(root);
+ collectPragmas(root);
}
} catch (Exception e) {
// We do not guarantee to include proof infos. If something goes
@@ -124,6 +127,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
+ private void collectPragmas(ISCContextRoot origin) {
+ // TODO
+ }
+
private void collectProofInfo(ISCContextRoot origin)
throws RodinDBException {
@@ -327,6 +334,11 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return proofs;
}
+ public List<IPragma> getPragmas() {
+ // TODO Auto-generated method stub
+ return pragmas;
+ }
+
public List<ClassifiedPragma> getProofspragmas() {
return proofspragmas;
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java b/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java
deleted file mode 100644
index 4148c8bcaba817abac471fc9a6b1e687c88927b7..0000000000000000000000000000000000000000
--- a/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java
+++ /dev/null
@@ -1,7 +0,0 @@
-package de.prob.eventb.translator;
-
-import de.prob.core.translator.ITranslator;
-
-public class UnitPragmaTranslator implements ITranslator {
-
-}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
index e5c3d34b48bf2ecca49162be37a6bb0fa003e456..075270d4ae253ae3aef71dafd9d877e1ee61a433 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBContextTranslator.java
@@ -17,7 +17,6 @@ import org.rodinp.core.RodinDBException;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.ContextTranslator;
-import de.prob.eventb.translator.UnitPragmaTranslator;
import de.prob.prolog.output.IPrologTermOutput;
public final class EventBContextTranslator extends EventBTranslator {
@@ -53,15 +52,14 @@ public final class EventBContextTranslator extends EventBTranslator {
private void constructTranslation(final IPrologTermOutput pto)
throws TranslationFailedException {
List<ContextTranslator> contextTranslators = new ArrayList<ContextTranslator>();
- List<UnitPragmaTranslator> unitPragmaTranslators = new ArrayList<UnitPragmaTranslator>();
// translators.add(ContextTranslator.create(context));
if (context instanceof ISCContextRoot) {
ISCContextRoot root = (ISCContextRoot) context;
collectContexts(contextTranslators, new ArrayList<String>(), root);
}
- printProlog(new ArrayList<ModelTranslator>(), contextTranslators,
- unitPragmaTranslators, pto);
+
+ printProlog(new ArrayList<ModelTranslator>(), contextTranslators, pto);
}
private void collectContexts(final List<ContextTranslator> translatorMap,
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 dc7b01890c43d07b15238966f619dc50bfea9398..1b9e5fb6179714c13da881ffcedb401ac70ef529 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
@@ -16,7 +16,6 @@ import org.rodinp.core.RodinDBException;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.ContextTranslator;
-import de.prob.eventb.translator.UnitPragmaTranslator;
import de.prob.eventb.translator.flow.FlowAnalysis;
import de.prob.logging.Logger;
import de.prob.prolog.output.IPrologTermOutput;
@@ -65,8 +64,7 @@ public final class EventBMachineTranslator extends EventBTranslator {
List<ISCMachineRoot> roots = collectRefinementChain();
final List<ModelTranslator> mchTranslators = getModelTranslators(roots);
final List<ContextTranslator> ctxTranslators = getContextTranslators(roots);
- final List<UnitPragmaTranslator> unitPragmaTranslators = getUnitPragmaTranslators(roots);
- printProlog(mchTranslators, ctxTranslators, unitPragmaTranslators, pto);
+ printProlog(mchTranslators, ctxTranslators, pto);
}
private List<ISCMachineRoot> collectRefinementChain()
@@ -99,18 +97,12 @@ public final class EventBMachineTranslator extends EventBTranslator {
return mchTranslators;
}
- private List<UnitPragmaTranslator> getUnitPragmaTranslators(
- final List<ISCMachineRoot> roots) throws TranslationFailedException {
- final List<UnitPragmaTranslator> translators = new ArrayList<UnitPragmaTranslator>();
- // TODO: do something brilliant
- return translators;
- }
-
private List<ContextTranslator> getContextTranslators(
final List<ISCMachineRoot> models)
throws TranslationFailedException {
final List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
final List<String> processed = new ArrayList<String>();
+
for (ISCMachineRoot m : models) {
ISCInternalContext[] seenContexts;
try {
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
index 723d413d96db5ae8983e7f8763bf8023d9d2bb23..4cf7538db93dfea3df0b9355063386031bca3f3a 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
@@ -23,9 +23,9 @@ import de.be4.classicalb.core.parser.node.AEventBModelParseUnit;
import de.be4.classicalb.core.parser.node.Node;
import de.prob.core.translator.ITranslator;
import de.prob.core.translator.TranslationFailedException;
+import de.prob.core.translator.pragmas.IPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.ContextTranslator;
-import de.prob.eventb.translator.UnitPragmaTranslator;
import de.prob.prolog.output.IPrologTermOutput;
public abstract class EventBTranslator implements ITranslator {
@@ -113,6 +113,24 @@ public abstract class EventBTranslator implements ITranslator {
printFlowInformation(pout);
}
+ private void printPragmaContents(
+ Collection<ModelTranslator> refinementChainTranslators,
+ Collection<ContextTranslator> contextTranslators,
+ IPrologTermOutput pout) {
+ ArrayList<IPragma> pragmas = new ArrayList<IPragma>();
+
+ for (ContextTranslator contextTranslator : contextTranslators) {
+ pragmas.addAll(contextTranslator.getPragmas());
+ }
+ for (ModelTranslator modelTranslator : refinementChainTranslators) {
+ pragmas.addAll(modelTranslator.getPragmas());
+ }
+
+ for (IPragma pragma : pragmas) {
+ pragma.output(pout);
+ }
+ }
+
protected abstract void printFlowInformation(final IPrologTermOutput pout);
private ASTProlog createAstVisitor(
@@ -128,7 +146,6 @@ public abstract class EventBTranslator implements ITranslator {
protected void printProlog(
final Collection<ModelTranslator> refinementChainTranslators,
final Collection<ContextTranslator> contextTranslators,
- final Collection<UnitPragmaTranslator> unitPragmaTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
final ASTProlog prolog = createAstVisitor(refinementChainTranslators,
contextTranslators, pout);
@@ -149,6 +166,8 @@ public abstract class EventBTranslator implements ITranslator {
// } catch (RodinDBException e) {
// e.printStackTrace();
// }
+ printPragmaContents(refinementChainTranslators, contextTranslators,
+ pout);
pout.closeList();
pout.printVariable("_Error");
pout.closeTerm();
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 ead67da6ba447b4f830418088f54eb34069a3bf7..fd794beadb03366ee8b2fb99b9a0b8ee16273a51 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
@@ -67,6 +67,7 @@ import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.PWitness;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.core.translator.TranslationFailedException;
+import de.prob.core.translator.pragmas.IPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.AssignmentVisitor;
import de.prob.eventb.translator.ExpressionVisitor;
@@ -81,6 +82,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final ITypeEnvironment te;
private final IMachineRoot origin;
private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
+ private final List<IPragma> pragmas = new ArrayList<IPragma>();
+
// private final List<String> depContext = new ArrayList<String>();
// Confined in the thread calling the factory method
@@ -117,6 +120,10 @@ public class ModelTranslator extends AbstractComponentTranslator {
return Collections.unmodifiableList(proofs);
}
+ public List<IPragma> getPragmas() {
+ return Collections.unmodifiableList(pragmas);
+ }
+
public AEventBModelParseUnit getModelAST() {
if (broken) {
final String message = "The machine contains Rodin Problems. Please fix it before animating";
@@ -164,6 +171,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
// Check for fully discharged Invariants and Events
collectProofInfo();
+
+ // Collect Pragmas, Units, etc.
+ collectPragmas();
+ }
+
+ private void collectPragmas() {
+ // TODO
}
private void collectProofInfo() throws RodinDBException {
@@ -179,7 +193,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
EProofStatus pstatus = EProofStatus.UNPROVEN;
- if (!broken && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
+ if (!broken
+ && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
pstatus = EProofStatus.REVIEWED;
if (!broken && confidence == IConfidence.DISCHARGED_MAX)
pstatus = EProofStatus.PROVEN;