From f74c520097c4e8557fe0efd3a6b765a4bb90d78b Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 19 Dec 2012 13:10:15 +0100
Subject: [PATCH] try to add unit pragmas to the translation, infrastructural
 work

---
 .../prob/eventb/translator/UnitPragmaTranslator.java |  7 +++++++
 .../translator/internal/EventBContextTranslator.java | 12 ++++++++----
 .../translator/internal/EventBMachineTranslator.java | 11 ++++++++++-
 .../eventb/translator/internal/EventBTranslator.java |  2 ++
 4 files changed, 27 insertions(+), 5 deletions(-)
 create mode 100644 de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java

diff --git a/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java b/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java
new file mode 100644
index 00000000..4148c8bc
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java
@@ -0,0 +1,7 @@
+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 ae640ff9..e5c3d34b 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,6 +17,7 @@ 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 {
@@ -51,13 +52,16 @@ public final class EventBContextTranslator extends EventBTranslator {
 
 	private void constructTranslation(final IPrologTermOutput pto)
 			throws TranslationFailedException {
-		List<ContextTranslator> translators = new ArrayList<ContextTranslator>();
-//		translators.add(ContextTranslator.create(context));
+		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(translators, new ArrayList<String>(), root);
+			collectContexts(contextTranslators, new ArrayList<String>(), root);
 		}
-		printProlog(new ArrayList<ModelTranslator>(), translators, pto);
+		printProlog(new ArrayList<ModelTranslator>(), contextTranslators,
+				unitPragmaTranslators, 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 b6ee12f4..dc7b0189 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,6 +16,7 @@ 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;
@@ -64,7 +65,8 @@ public final class EventBMachineTranslator extends EventBTranslator {
 		List<ISCMachineRoot> roots = collectRefinementChain();
 		final List<ModelTranslator> mchTranslators = getModelTranslators(roots);
 		final List<ContextTranslator> ctxTranslators = getContextTranslators(roots);
-		printProlog(mchTranslators, ctxTranslators, pto);
+		final List<UnitPragmaTranslator> unitPragmaTranslators = getUnitPragmaTranslators(roots);
+		printProlog(mchTranslators, ctxTranslators, unitPragmaTranslators, pto);
 	}
 
 	private List<ISCMachineRoot> collectRefinementChain()
@@ -97,6 +99,13 @@ 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 {
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 5f015c24..c733ac66 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
@@ -25,6 +25,7 @@ import de.prob.core.translator.ITranslator;
 import de.prob.core.translator.TranslationFailedException;
 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 {
@@ -127,6 +128,7 @@ 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);
-- 
GitLab