diff --git a/de.prob.core/.classpath b/de.prob.core/.classpath
index bb1ae0592818db067d6599e1a8f034a51349b613..0c07df9acec38ff19ac4da7324df32c2f1dc510e 100644
--- a/de.prob.core/.classpath
+++ b/de.prob.core/.classpath
@@ -1,23 +1,21 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
+ <classpathentry kind="src" path="src"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xmlpull-1.1.3.1.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xpp3_min-1.1.4c.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/xstream-1.4.3.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/commons-lang-2.6.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jgrapht-0.8.3.jar"/>
<classpathentry exported="true" kind="lib" path="lib/dependencies/jsr305-1.3.9.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.8-SNAPSHOT.jar"/>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.8-SNAPSHOT.jar"/>
- <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/answerparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/bparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/unicode-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar"/>
+ <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
- <classpathentry kind="src" path="src"/>
- <classpathentry kind="src" path="test"/>
- <classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/4"/>
<classpathentry kind="output" path="bin"/>
</classpath>
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index e1cf9ef6e6d4630ea3dbbbc24da03219d65c3db5..39ced3dd508fa9a2c36c9c774901ec4167a1b852 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -115,8 +115,14 @@ Bundle-Activator: de.prob.core.internal.Activator
Eclipse-BuddyPolicy: registered
Bundle-RequiredExecutionEnvironment: JavaSE-1.6
Bundle-ClassPath: .,
+ lib/dependencies/ltlparser-2.4.12-SNAPSHOT.jar,
+ lib/dependencies/unicode-2.4.12-SNAPSHOT.jar,
+ lib/dependencies/prologlib-2.4.12-SNAPSHOT.jar,
+ lib/dependencies/cliparser-2.4.12-SNAPSHOT.jar,
+ lib/dependencies/answerparser-2.4.12-SNAPSHOT.jar,
+ lib/dependencies/parserbase-2.4.12-SNAPSHOT.jar,
lib/dependencies/answerparser-2.4.8-SNAPSHOT.jar,
- lib/dependencies/bparser-2.4.8-SNAPSHOT.jar,
+ lib/dependencies/bparser-2.4.12-SNAPSHOT.jar,
lib/dependencies/cliparser-2.4.8-SNAPSHOT.jar,
lib/dependencies/commons-lang-2.6.jar,
lib/dependencies/jgrapht-0.8.3.jar,
diff --git a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
index 96a04d1a9eb4ae1667be87ccca45209656782dbe..ca9b3232e135a28b232e25574da973447e34dd32 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
@@ -626,10 +626,6 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
IExpressionExtension extension = expression.getExtension();
String symbol = extension.getSyntaxSymbol();
- Object origin = extension.getOrigin();
-
- // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
- // Theories.addOrigin(origin);
p.setIdentifier(new TIdentifierLiteral(symbol));
Expression[] expressions = expression.getChildExpressions();
diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
index a74d82914e8f220539a04cf6a36eff7a0025293a..58c6cafaa0df8e772a89f2a92b7b7b773ba569a9 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -1,198 +1,212 @@
package de.prob.eventb.translator;
+import java.util.LinkedList;
-// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+import org.eventb.core.IEventBProject;
+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.IRodinProject;
+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);
-// }
+ public static void translate(IEventBProject project, IPrologTermOutput pout)
+ throws RodinDBException {
+ final IRodinProject rProject = project.getRodinProject();
+ final IDeployedTheoryRoot[] theories = rProject
+ .getRootElementsOfType(IDeployedTheoryRoot.ELEMENT_TYPE);
+ for (IDeployedTheoryRoot theory : theories) {
+ printTranslation(theory, pout);
+ }
+ }
+
+ 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);
+ }
}
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 43ea5792f26eee7de07938f106ef26696642a2c8..dd69c0da5768e348f2f1818aa211b64c955a78e6 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
@@ -144,13 +144,11 @@ public abstract class EventBTranslator implements ITranslator {
pout.openList();
printProofInformation(refinementChainTranslators, contextTranslators,
pout);
- // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
-
- // try {
- // Theories.translate(pout);
- // } catch (RodinDBException e) {
- // e.printStackTrace();
- // }
+ try {
+ Theories.translate(project, pout);
+ } catch (RodinDBException e) {
+ e.printStackTrace();
+ }
pout.closeList();
pout.printVariable("_Error");
pout.closeTerm();
diff --git a/de.prob.ui/.classpath b/de.prob.ui/.classpath
index f67843181ee95a7771d0edd1009be1faaed415b0..100092b255b1ad1a077f31d3e5931b134f6f5f45 100644
--- a/de.prob.ui/.classpath
+++ b/de.prob.ui/.classpath
@@ -1,10 +1,10 @@
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
- <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
<classpathentry exported="true" kind="lib" path="lib/apache_xmlrpc.jar"/>
<classpathentry exported="true" kind="lib" path="lib/ws_commons.jar"/>
<classpathentry kind="output" path="bin"/>
+ <classpathentry exported="true" kind="lib" path="lib/dependencies/commons-codec-1.6.jar"/>
</classpath>