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 0000000000000000000000000000000000000000..4148c8bcaba817abac471fc9a6b1e687c88927b7 --- /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 ae640ff98a9c1d84b2014b850b42db0f3c2058f3..e5c3d34b48bf2ecca49162be37a6bb0fa003e456 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 b6ee12f4e13e3fbabecdd6b9ea25020a3f8b907f..dc7b01890c43d07b15238966f619dc50bfea9398 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 5f015c247dc4809b9e830aae1c0c822fa1381f11..c733ac66be081a602bdf356dfcf302db1319d811 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);