Merge branch 'feature/theory_plugin' into develop

Conflicts:
	de.prob.core/META-INF/MANIFEST.MF
	de.prob2.feature/feature.xml

de.prob.core/META-INF/MANIFEST.MF

@@ -5,7 +5,8 @@ Bundle-SymbolicName: de.prob.core;singleton:=true
 Bundle-Version: 9.3.0.qualifier
 Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)",
  org.rodinp.core;bundle-version="[1.3.1,1.7.0)",
- org.eventb.core;bundle-version="[2.1.0,2.6.0)"
+ org.eventb.core;bundle-version="[2.1.0,2.6.0)",
+ org.eventb.theory.core;bundle-version="2.0.0"
 Bundle-ActivationPolicy: lazy
 Eclipse-BundleShape: dir
 Bundle-Vendor: HHU Düsseldorf STUPS Group

de.prob.core/plugin.xml

@@ -4,6 +4,7 @@
    <extension-point id="de.prob.core.lifecycle" name="Lifecycle Events" schema="schema/de.prob.core.lifecycle.exsd"/>
    <extension-point id="de.prob.core.computation" name="Computation Events" schema="schema/de.prob.core.computation.exsd"/>
    <extension-point id="de.prob.core.animation" name="Animation Events" schema="schema/de.prob.core.animation.exsd"/>
+   <extension-point id="de.prob.translator" name="Translator Extensions" schema="schema/de.prob.translator.exsd"/>
    <extension
          point="de.prob.core.animation">
       <listener

de.prob.core/schema/de.prob.translator.exsd

+<?xml version='1.0' encoding='UTF-8'?>
+<!-- Schema file written by PDE -->
+<schema targetNamespace="de.prob.core" xmlns="http://www.w3.org/2001/XMLSchema">
+<annotation>
+      <appInfo>
+         <meta.schema plugin="de.prob.core" id="de.prob.translator" name="Translator Extensions"/>
+      </appInfo>
+      <documentation>
+         [Enter description of this extension point.]
+      </documentation>
+   </annotation>
+
+   <element name="extension">
+      <annotation>
+         <appInfo>
+            <meta.element />
+         </appInfo>
+      </annotation>
+      <complexType>
+         <sequence minOccurs="0" maxOccurs="unbounded">
+            <element ref="translator"/>
+         </sequence>
+         <attribute name="point" type="string" use="required">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="id" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="name" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+               <appInfo>
+                  <meta.attribute translatable="true"/>
+               </appInfo>
+            </annotation>
+         </attribute>
+      </complexType>
+   </element>
+
+   <element name="translator">
+      <complexType>
+         <attribute name="name" type="string">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+            </annotation>
+         </attribute>
+         <attribute name="class" type="string" use="required">
+            <annotation>
+               <documentation>
+                  
+               </documentation>
+               <appInfo>
+                  <meta.attribute kind="java" basedOn=":de.prob.core.translator.IExternalTranslator"/>
+               </appInfo>
+            </annotation>
+         </attribute>
+      </complexType>
+   </element>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="since"/>
+      </appInfo>
+      <documentation>
+         [Enter the first release in which this extension point appears.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="examples"/>
+      </appInfo>
+      <documentation>
+         [Enter extension point usage example here.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="apiinfo"/>
+      </appInfo>
+      <documentation>
+         [Enter API information here.]
+      </documentation>
+   </annotation>
+
+   <annotation>
+      <appInfo>
+         <meta.section type="implementation"/>
+      </appInfo>
+      <documentation>
+         [Enter information about supplied implementation of this extension point.]
+      </documentation>
+   </annotation>
+
+
+</schema>

de.prob.core/src/de/prob/core/translator/IExternalTranslator.java

+package de.prob.core.translator;
+
+import de.prob.prolog.output.PrologTermOutput;
+
+public interface IExternalTranslator {
+	public void writeProlog(PrologTermOutput pto);
+}

de.prob.core/src/de/prob/core/translator/TranslationFailedException.java

@@ -18,8 +18,12 @@ public class TranslationFailedException extends ProBException {
 
 	public TranslationFailedException(final String component,
 			final String details) {
-		super("Translation of " + component + " failed\n" + details);
-		notifyUserOnce();
+		this(component, details, null);
 	}
 
+	public TranslationFailedException(final String component,
+			final String details, Throwable e) {
+		super("Translation of " + component + " failed\n" + details, e, false);
+		notifyUserOnce();
+	}
 }

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

@@ -66,14 +66,13 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 	private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
 	private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
 	private final FormulaFactory ff;
-
-	// Confined in the thread calling the factory method
 	private ITypeEnvironment te;
 
 	public static ContextTranslator create(final ISCContext context)
 			throws TranslationFailedException {
 		ContextTranslator contextTranslator = new ContextTranslator(context);
 		try {
+			(new TheoryTranslator()).translate();
 			contextTranslator.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: ";
@@ -90,11 +89,20 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 	 * contains errors)
 	 * 
 	 * @param context
+	 * @throws TranslationFailedException
 	 * @throws RodinDBException
 	 */
-	private ContextTranslator(final ISCContext context) {
+	private ContextTranslator(final ISCContext context)
+			throws TranslationFailedException {
 		this.context = context;
-		ff = FormulaFactory.getDefault();
+		ff = ((ISCContextRoot) context).getFormulaFactory();
+		try {
+			te = ((ISCContextRoot) context).getTypeEnvironment(ff);
+		} catch (RodinDBException e) {
+			final String message = "A Rodin exception occured during translation process. Original Exception: ";
+			throw new TranslationFailedException(context.getComponentName(),
+					message + e.getLocalizedMessage());
+		}
 	}
 
 	private void translate() throws RodinDBException {
@@ -102,7 +110,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			ISCContextRoot context_root = (ISCContextRoot) context;
 			Assert.isTrue(context_root.getRodinFile().isConsistent());
 			te = context_root.getTypeEnvironment(ff);
-			collectProofInfo(context_root);
 		} else if (context instanceof ISCInternalContext) {
 			ISCInternalContext context_internal = (ISCInternalContext) context;
 
@@ -124,9 +131,9 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			ISCMachineRoot machine_root = (ISCMachineRoot) context_internal
 					.getRoot();
 			Assert.isTrue(machine_root.getRodinFile().isConsistent());
-			te = machine_root.getTypeEnvironment(ff);
 		}
 		translateContext();
+
 	}
 
 	private void collectProofInfo(ISCContextRoot context_root)
@@ -313,7 +320,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			final PredicateVisitor visitor = new PredicateVisitor(
 					new LinkedList<String>());
 			element.getPredicate(ff, te).accept(visitor);
-
 			final PPredicate predicate = visitor.getPredicate();
 			list.add(predicate);
 			labelMapping.put(predicate, element);

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

@@ -20,6 +20,7 @@ import org.eventb.core.ast.BoolExpression;
 import org.eventb.core.ast.BoundIdentDecl;
 import org.eventb.core.ast.BoundIdentifier;
 import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedExpression;
 import org.eventb.core.ast.Formula;
 import org.eventb.core.ast.FreeIdentifier;
 import org.eventb.core.ast.ISimpleVisitor;
@@ -28,6 +29,7 @@ import org.eventb.core.ast.Predicate;
 import org.eventb.core.ast.QuantifiedExpression;
 import org.eventb.core.ast.SetExtension;
 import org.eventb.core.ast.UnaryExpression;
+import org.eventb.core.ast.extension.IExpressionExtension;
 
 import de.be4.classicalb.core.parser.node.AAddExpression;
 import de.be4.classicalb.core.parser.node.ABoolSetExpression;
@@ -50,6 +52,7 @@ import de.be4.classicalb.core.parser.node.AEventBFirstProjectionV2Expression;
 import de.be4.classicalb.core.parser.node.AEventBIdentityExpression;
 import de.be4.classicalb.core.parser.node.AEventBSecondProjectionExpression;
 import de.be4.classicalb.core.parser.node.AEventBSecondProjectionV2Expression;
+import de.be4.classicalb.core.parser.node.AExtendedExprExpression;
 import de.be4.classicalb.core.parser.node.AFunctionExpression;
 import de.be4.classicalb.core.parser.node.AGeneralIntersectionExpression;
 import de.be4.classicalb.core.parser.node.AGeneralUnionExpression;
@@ -112,7 +115,6 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
 	// we need some abilities of the linked list, using List is not an option
 	private boolean expressionSet = false;
 
-	@SuppressWarnings("unused")
 	private ExpressionVisitor() { // we want to prevent clients from calling
 		// the default constructor
 		super();
@@ -157,15 +159,14 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
 			list.add(visitor.getExpression());
 		}
 
-		// Process internal Expression and Predcate
+		// Process internal Expression and Predicate
 		final Predicate predicate = expression.getPredicate();
 		final PredicateVisitor predicateVisitor = new PredicateVisitor(bounds);
 		predicate.accept(predicateVisitor);
 
 		final PPredicate pr = predicateVisitor.getPredicate();
 
-		final ExpressionVisitor expressionVisitor = new ExpressionVisitor(
-				bounds);
+		final ExpressionVisitor expressionVisitor = new ExpressionVisitor();
 		expression.getExpression().accept(expressionVisitor);
 
 		final PExpression ex = expressionVisitor.getExpression();
@@ -619,6 +620,40 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
 		setExpression(setExtensionExpression);
 	}
 
+	@Override
+	public void visitExtendedExpression(ExtendedExpression expression) {
+		AExtendedExprExpression p = new AExtendedExprExpression();
+
+		IExpressionExtension extension = expression.getExtension();
+		String symbol = extension.getSyntaxSymbol();
+		Object origin = extension.getOrigin();
+
+		Theories.addOrigin(origin);
+
+		p.setIdentifier(new TIdentifierLiteral(symbol));
+		Expression[] expressions = expression.getChildExpressions();
+		List<PExpression> childExprs = new ArrayList<PExpression>();
+		for (Expression e : expressions) {
+			ExpressionVisitor v = new ExpressionVisitor(
+					new LinkedList<String>());
+			e.accept(v);
+			childExprs.add(v.getExpression());
+		}
+		p.setExpressions(childExprs);
+
+		Predicate[] childPredicates = expression.getChildPredicates();
+		List<PPredicate> childPreds = new ArrayList<PPredicate>();
+		for (Predicate pd : childPredicates) {
+			PredicateVisitor v = new PredicateVisitor(null);
+			pd.accept(v);
+			childPreds.add(v.getPredicate());
+		}
+		p.setPredicates(childPreds);
+
+		setExpression(p);
+
+	}
+
 	@SuppressWarnings("deprecation")
 	@Override
 	public void visitUnaryExpression(final UnaryExpression expression) { // NOPMD

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

@@ -15,6 +15,7 @@ import org.eventb.core.ast.AssociativePredicate;
 import org.eventb.core.ast.BinaryPredicate;
 import org.eventb.core.ast.BoundIdentDecl;
 import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.ExtendedPredicate;
 import org.eventb.core.ast.Formula;
 import org.eventb.core.ast.ISimpleVisitor;
 import org.eventb.core.ast.LiteralPredicate;
@@ -24,12 +25,14 @@ import org.eventb.core.ast.QuantifiedPredicate;
 import org.eventb.core.ast.RelationalPredicate;
 import org.eventb.core.ast.SimplePredicate;
 import org.eventb.core.ast.UnaryPredicate;
+import org.eventb.core.ast.extension.IPredicateExtension;
 
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
 import de.be4.classicalb.core.parser.node.AEqualPredicate;
 import de.be4.classicalb.core.parser.node.AEquivalencePredicate;
 import de.be4.classicalb.core.parser.node.AExistsPredicate;
+import de.be4.classicalb.core.parser.node.AExtendedPredPredicate;
 import de.be4.classicalb.core.parser.node.AFalsityPredicate;
 import de.be4.classicalb.core.parser.node.AFinitePredicate;
 import de.be4.classicalb.core.parser.node.AForallPredicate;
@@ -50,6 +53,7 @@ import de.be4.classicalb.core.parser.node.ASubsetStrictPredicate;
 import de.be4.classicalb.core.parser.node.ATruthPredicate;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PPredicate;
+import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.prob.eventb.translator.internal.SimpleVisitorAdapter;
 
 public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
@@ -76,12 +80,19 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
 			predicateSet = true;
 			this.p = p;
 		}
-		//public ClassifiedPragma(String name, Node attachedTo, List<String> arguments, List<String> warnings, SourcePosition start, SourcePosition end) {
+		// public ClassifiedPragma(String name, Node attachedTo, List<String>
+		// arguments, List<String> warnings, SourcePosition start,
+		// SourcePosition end) {
 
-    //     new ClassifiedPragma("discharged", p, proof, Collections.emptyList(), new SourcePosition(-1, -1), new SourcePosition(-1, -1));
+		// new ClassifiedPragma("discharged", p, proof, Collections.emptyList(),
+		// new SourcePosition(-1, -1), new SourcePosition(-1, -1));
 	}
 
-	public PredicateVisitor(final LinkedList<String> bounds) {
+	public PredicateVisitor() {
+		this(null);
+	}
+
+	public PredicateVisitor(LinkedList<String> bounds) {
 		super();
 		if (bounds == null) {
 			this.bounds = new LinkedList<String>();
@@ -90,10 +101,6 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
 		}
 	}
 
-	public PredicateVisitor() {
-		this(null);
-	}
-
 	@Override
 	public void visitQuantifiedPredicate(final QuantifiedPredicate predicate) {
 		final int tag = predicate.getTag();
@@ -406,4 +413,34 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
 		setPredicate(result);
 	}
 
+	@Override
+	public void visitExtendedPredicate(ExtendedPredicate predicate) {
+		AExtendedPredPredicate p = new AExtendedPredPredicate();
+		IPredicateExtension extension = predicate.getExtension();
+		String symbol = extension.getSyntaxSymbol();
+		Object origin = extension.getOrigin();
+		Theories.addOrigin(origin);
+
+		p.setIdentifier(new TIdentifierLiteral(symbol));
+
+		Expression[] expressions = predicate.getChildExpressions();
+		List<PExpression> childExprs = new ArrayList<PExpression>();
+		for (Expression e : expressions) {
+			ExpressionVisitor v = new ExpressionVisitor(bounds);
+			e.accept(v);
+			childExprs.add(v.getExpression());
+		}
+		p.setExpressions(childExprs);
+
+		Predicate[] childPredicates = predicate.getChildPredicates();
+		List<PPredicate> childPreds = new ArrayList<PPredicate>();
+		for (Predicate pd : childPredicates) {
+			PredicateVisitor v = new PredicateVisitor(bounds);
+			pd.accept(v);
+			childPreds.add(v.getPredicate());
+		}
+		p.setPredicates(childPreds);
+		setPredicate(p);
+	}
+
 }

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

+package de.prob.eventb.translator;
+
+import java.util.LinkedList;
+import java.util.Map;
+import java.util.TreeMap;
+
+import org.eventb.core.ISCIdentifierElement;
+import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.Formula;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.ast.Predicate;
+import org.eventb.core.ast.Type;
+import org.eventb.theory.core.IDeployedTheoryRoot;
+import org.eventb.theory.core.IFormulaExtensionsSource;
+import org.eventb.theory.core.ISCConstructorArgument;
+import org.eventb.theory.core.ISCDatatypeConstructor;
+import org.eventb.theory.core.ISCDatatypeDefinition;
+import org.eventb.theory.core.ISCDirectOperatorDefinition;
+import org.eventb.theory.core.ISCNewOperatorDefinition;
+import org.eventb.theory.core.ISCOperatorArgument;
+import org.eventb.theory.core.ISCRecursiveDefinitionCase;
+import org.eventb.theory.core.ISCRecursiveOperatorDefinition;
+import org.eventb.theory.core.ISCTypeArgument;
+import org.eventb.theory.core.ISCTypeParameter;
+import org.rodinp.core.RodinDBException;
+
+import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
+import de.prob.prolog.output.IPrologTermOutput;
+
+public class Theories {
+
+	private static Map<String, IDeployedTheoryRoot> theories = new TreeMap<String, IDeployedTheoryRoot>();
+
+	public static final ITypeEnvironment global_te = FormulaFactory
+			.getDefault().makeTypeEnvironment();
+
+	public static void addOrigin(Object origin) {
+		if (origin instanceof ISCNewOperatorDefinition) {
+			final IDeployedTheoryRoot theory = (IDeployedTheoryRoot) ((ISCNewOperatorDefinition) origin)
+					.getParent();
+			final String name = theory.getElementName();
+			theories.put(name, theory);
+		} else {
+			System.out.println("Did not register origin: "
+					+ origin.getClass().getName());
+		}
+	}
+
+	public static void translate(IPrologTermOutput pto) throws RodinDBException {
+		for (IDeployedTheoryRoot theory : theories.values()) {
+			printTranslation(theory, pto);
+		}
+	}
+
+	private static void printTranslation(IDeployedTheoryRoot theory,
+			IPrologTermOutput pto) throws RodinDBException {
+		pto.openTerm("theory");
+		printTypeParameters(theory, pto);
+		printDataTypes(theory, pto);
+		printOperatorDefs(theory, pto);
+		pto.closeTerm();
+	}
+
+	private static void printTypeParameters(IFormulaExtensionsSource theory,
+			IPrologTermOutput pto) throws RodinDBException {
+		pto.openList();
+		for (ISCTypeParameter parameter : theory.getSCTypeParameters()) {
+			pto.printAtom(parameter.getIdentifierString());
+		}
+		pto.closeList();
+	}
+
+	private static void printDataTypes(IDeployedTheoryRoot theory,
+			IPrologTermOutput pto) throws RodinDBException {
+		final FormulaFactory ff = theory.getFormulaFactory();
+		pto.openList();
+		for (ISCDatatypeDefinition def : theory.getSCDatatypeDefinitions()) {
+			printDataType(def, ff, pto);
+		}
+		pto.closeList();
+	}
+
+	private static void printDataType(ISCDatatypeDefinition def,
+			FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
+		pto.openTerm("datatype");
+		pto.printAtom(def.getIdentifierString());
+		pto.openList();
+		for (ISCTypeArgument arg : def.getTypeArguments()) {
+			printType(arg.getSCGivenType(ff), ff, pto);
+		}
+		pto.closeList();
+		pto.openList();
+		for (ISCDatatypeConstructor cons : def.getConstructors()) {
+			printConstructor(cons, ff, pto);
+		}
+		pto.closeList();
+		pto.closeTerm();
+
+	}
+
+	private static void printConstructor(ISCDatatypeConstructor cons,
+			FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
+		pto.openTerm("constructor");
+		pto.printAtom(cons.getIdentifierString());
+		pto.openList();
+		for (ISCConstructorArgument arg : cons.getConstructorArguments()) {
+			printTypedIdentifier("destructor", arg, ff, pto);
+		}
+		pto.closeList();
+		pto.closeTerm();
+
+	}
+
+	private static void printOperatorDefs(IDeployedTheoryRoot theory,
+			IPrologTermOutput pto) throws RodinDBException {
+		pto.openList();
+		for (ISCNewOperatorDefinition opdef : theory
+				.getSCNewOperatorDefinitions()) {
+			printOperator(opdef, theory, pto);
+		}
+		pto.closeList();
+	}
+
+	private static void printOperator(ISCNewOperatorDefinition opDef,
+			IDeployedTheoryRoot theory, IPrologTermOutput prologOutput)
+			throws RodinDBException {
+
+		prologOutput.openTerm("operator");
+		prologOutput.printAtom(opDef.getLabel());
+
+		final FormulaFactory ff = theory.getFormulaFactory();
+		final ITypeEnvironment te = theory.getTypeEnvironment(ff);
+
+		// Arguments
+		prologOutput.openList();
+		ISCOperatorArgument[] operatorArguments = opDef.getOperatorArguments();
+		for (ISCOperatorArgument argument : operatorArguments) {
+			printTypedIdentifier("argument", argument, ff, prologOutput);
+		}
+		prologOutput.closeList();
+
+		// WD Condition
+		Predicate wdCondition = opDef.getWDCondition(ff, te);
+		printPredicate(prologOutput, wdCondition);
+
+		// Direct Definitions
+		prologOutput.openList();
+		processDefinitions(ff, te, prologOutput,
+				opDef.getDirectOperatorDefinitions());
+		prologOutput.closeList();
+
+		// Recursive Definitions
+		prologOutput.openList();
+		ISCRecursiveOperatorDefinition[] definitions = opDef
+				.getRecursiveOperatorDefinitions();
+		for (ISCRecursiveOperatorDefinition definition : definitions) {
+			ISCRecursiveDefinitionCase[] recursiveDefinitionCases = definition
+					.getRecursiveDefinitionCases();
+			for (ISCRecursiveDefinitionCase c : recursiveDefinitionCases) {
+				Expression ex = c.getExpression(ff, te);
+				printExpression(prologOutput, ex);
+			}
+		}
+		prologOutput.closeList();
+
+		prologOutput.closeTerm();
+	}
+
+	private static void processDefinitions(FormulaFactory ff,
+			ITypeEnvironment te, IPrologTermOutput prologOutput,
+			ISCDirectOperatorDefinition[] directOperatorDefinitions)
+			throws RodinDBException {
+		for (ISCDirectOperatorDefinition def : directOperatorDefinitions) {
+			Formula<?> scFormula = def.getSCFormula(ff, te);
+
+			if (scFormula instanceof Predicate) {
+				Predicate pp = (Predicate) scFormula;
+				printPredicate(prologOutput, pp);
+			}
+			if (scFormula instanceof Expression) {
+				Expression pp = (Expression) scFormula;
+				printExpression(prologOutput, pp);
+			}
+
+		}
+	}
+
+	private static void printTypedIdentifier(final String functor,
+			final ISCIdentifierElement id, final FormulaFactory ff,
+			final IPrologTermOutput pto) throws RodinDBException {
+		pto.openTerm(functor);
+		pto.printAtom(id.getIdentifierString());
+		printType(id.getType(ff), ff, pto);
+		pto.closeTerm();
+	}
+
+	private static void printType(final Type type, final FormulaFactory ff,
+			final IPrologTermOutput pto) {
+		printExpression(pto, type.toExpression(ff));
+	}
+
+	private static void printExpression(IPrologTermOutput prologOutput,
+			Expression pp) {
+		ExpressionVisitor visitor = new ExpressionVisitor(
+				new LinkedList<String>());
+		pp.accept(visitor);
+		PExpression ex = visitor.getExpression();
+		ASTProlog pv = new ASTProlog(prologOutput, null);
+		ex.apply(pv);
+	}
+
+	private static void printPredicate(IPrologTermOutput prologOutput,
+			Predicate pp) {
+		PredicateVisitor visitor = new PredicateVisitor(
+				new LinkedList<String>());
+		pp.accept(visitor);
+		PPredicate predicate = visitor.getPredicate();
+		ASTProlog pv = new ASTProlog(prologOutput, null);
+		predicate.apply(pv);
+	}
+
+}

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

+package de.prob.eventb.translator;
+
+import org.eclipse.core.runtime.IConfigurationElement;
+import org.eclipse.core.runtime.IExtension;
+import org.eclipse.core.runtime.IExtensionPoint;
+import org.eclipse.core.runtime.IExtensionRegistry;
+import org.eclipse.core.runtime.Platform;
+
+public class TheoryTranslator {
+
+	public void translate() {
+		final IExtensionRegistry extensionRegistry = Platform
+				.getExtensionRegistry();
+		final IExtensionPoint extensionPoint = extensionRegistry
+				.getExtensionPoint("org.eventb.theory.core.deployedElements");
+		for (final IExtension extension : extensionPoint.getExtensions()) {
+			for (final IConfigurationElement configurationElement : extension
+					.getConfigurationElements()) {
+				System.out.println(configurationElement.getAttribute("name"));
+			}
+		}
+	}
+}

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

@@ -33,6 +33,7 @@ public class TranslatorFactory {
 	 */
 	public static void translate(final IEventBRoot root,
 			final IPrologTermOutput pto) throws TranslationFailedException {
+		
 		if (root instanceof IMachineRoot) {
 			final ISCMachineRoot scRoot = ((IMachineRoot) root)
 					.getSCMachineRoot();

de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java

@@ -27,6 +27,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.Theories;
 import de.prob.prolog.output.IPrologTermOutput;
 
 public abstract class EventBTranslator implements ITranslator {
@@ -143,6 +144,11 @@ public abstract class EventBTranslator implements ITranslator {
 		pout.openList();
 		printProofInformation(refinementChainTranslators, contextTranslators,
 				pout);
+		try {
+			Theories.translate(pout);
+		} catch (RodinDBException e) {
+			e.printStackTrace();
+		}
 		pout.closeList();
 		pout.printVariable("_Error");
 		pout.closeTerm();

de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java

@@ -77,13 +77,13 @@ public class ModelTranslator extends AbstractComponentTranslator {
 
 	private final ISCMachineRoot machine;
 	private final AEventBModelParseUnit model = new AEventBModelParseUnit();
-	private final FormulaFactory ff = FormulaFactory.getDefault();;
+	private final FormulaFactory ff;
+	private final ITypeEnvironment te;
 	private final IMachineRoot origin;
 	private final List<DischargedProof> proofs = new ArrayList<DischargedProof>();
 	// private final List<String> depContext = new ArrayList<String>();
 
 	// Confined in the thread calling the factory method
-	private ITypeEnvironment te;
 	private String refines;
 	private boolean broken = false;
 
@@ -137,9 +137,18 @@ public class ModelTranslator extends AbstractComponentTranslator {
 	// ###############################################################################################################################################################
 	// Implementation
 
-	private ModelTranslator(final ISCMachineRoot currentMachine) {
-		this.machine = currentMachine;
+	private ModelTranslator(final ISCMachineRoot machine)
+			throws TranslationFailedException {
+		this.machine = machine;
 		origin = machine.getMachineRoot();
+		ff = ((ISCMachineRoot) machine).getFormulaFactory();
+		try {
+			te = ((ISCMachineRoot) machine).getTypeEnvironment(ff);
+		} catch (RodinDBException e) {
+			final String message = "A Rodin exception occured during translation process. Original Exception: ";
+			throw new TranslationFailedException(machine.getComponentName(),
+					message + e.getLocalizedMessage());
+		}
 	}
 
 	private void translate() throws RodinDBException,
@@ -151,8 +160,6 @@ public class ModelTranslator extends AbstractComponentTranslator {
 		broken = !machine.isAccurate(); // isAccurate() is not transitive, we
 		// need to collect the information also
 		// for the events
-		te = machine.getTypeEnvironment(ff);
-
 		translateMachine();
 
 		// Check for fully discharged Invariants and Events

de.prob2.feature/feature.xml

@@ -241,6 +241,7 @@ litigation.
       <import plugin="de.prob.core" version="9.3.0" match="equivalent"/>
       <import plugin="de.prob.ui" version="7.3.0" match="equivalent"/>
       <import plugin="de.bmotionstudio.gef.editor" version="5.4.0" match="equivalent"/>
+      <import plugin="org.eventb.theory.core" version="1.3.0" match="greaterOrEqual"/>
    </requires>
 
    <plugin
@@ -279,4 +280,11 @@ litigation.
          fragment="true"
          unpack="false"/>
 
+   <plugin
+         id="de.prob.theory"
+         download-size="0"
+         install-size="0"
+         version="0.0.0"
+         unpack="false"/>
+
 </feature>