added export of type parameters and data type definitions

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, true);
+		notifyUserOnce();
+	}
 }

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

@@ -4,18 +4,25 @@ 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.FreeIdentifier;
 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;
@@ -31,14 +38,15 @@ public class Theories {
 			.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 {
@@ -49,19 +57,69 @@ public class Theories {
 
 	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();
 	}
@@ -80,20 +138,13 @@ public class Theories {
 		prologOutput.openList();
 		ISCOperatorArgument[] operatorArguments = opDef.getOperatorArguments();
 		for (ISCOperatorArgument argument : operatorArguments) {
-			FreeIdentifier identifier = argument.getIdentifier(ff);
-			te.add(identifier);
-			String arg = identifier.getName();
-			Expression type = identifier.getType().toExpression(ff);
-			prologOutput.openTerm("argument");
-			prologOutput.printAtom(arg);
-			printExpression(ff, te, prologOutput, type);
-			prologOutput.closeTerm();
+			printTypedIdentifier("argument", argument, ff, prologOutput);
 		}
 		prologOutput.closeList();
 
 		// WD Condition
 		Predicate wdCondition = opDef.getWDCondition(ff, te);
-		printPredicate(ff, te, prologOutput, wdCondition);
+		printPredicate(prologOutput, wdCondition);
 
 		// Direct Definitions
 		prologOutput.openList();
@@ -110,7 +161,7 @@ public class Theories {
 					.getRecursiveDefinitionCases();
 			for (ISCRecursiveDefinitionCase c : recursiveDefinitionCases) {
 				Expression ex = c.getExpression(ff, te);
-				printExpression(ff, te, prologOutput, ex);
+				printExpression(prologOutput, ex);
 			}
 		}
 		prologOutput.closeList();
@@ -127,18 +178,32 @@ public class Theories {
 
 			if (scFormula instanceof Predicate) {
 				Predicate pp = (Predicate) scFormula;
-				printPredicate(ff, te, prologOutput, pp);
+				printPredicate(prologOutput, pp);
 			}
 			if (scFormula instanceof Expression) {
 				Expression pp = (Expression) scFormula;
-				printExpression(ff, te, prologOutput, pp);
+				printExpression(prologOutput, pp);
 			}
 
 		}
 	}
 
-	private static void printExpression(FormulaFactory ff, ITypeEnvironment te,
-			IPrologTermOutput prologOutput, Expression 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);
@@ -147,8 +212,8 @@ public class Theories {
 		ex.apply(pv);
 	}
 
-	private static void printPredicate(FormulaFactory ff, ITypeEnvironment te,
-			IPrologTermOutput prologOutput, Predicate pp) {
+	private static void printPredicate(IPrologTermOutput prologOutput,
+			Predicate pp) {
 		PredicateVisitor visitor = new PredicateVisitor(
 				new LinkedList<String>());
 		pp.accept(visitor);