infrastructure for translation of unit pragmas

de.prob.core/src/de/prob/core/translator/pragmas/IPragma.java

+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public interface IPragma {
+
+	void output(IPrologTermOutput pout);
+
+}

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;
 	}

de.prob.core/src/de/prob/eventb/translator/UnitPragmaTranslator.java

-package de.prob.eventb.translator;
-
-import de.prob.core.translator.ITranslator;
-
-public class UnitPragmaTranslator implements ITranslator {
-
-}

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,

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 {

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();

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;