diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index f211375fe8992d8e05ebe484a15c3a0138a380e2..e1cf9ef6e6d4630ea3dbbbc24da03219d65c3db5 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/de.prob.core/META-INF/MANIFEST.MF
@@ -5,8 +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.theory.core;bundle-version="2.0.0"
+ org.eventb.core;bundle-version="[2.1.0,2.6.0)"
+REENABLE-FOR-THEORY-PLUGIN: org.eventb.theory.core;bundle-version="2.0.0"
Bundle-ActivationPolicy: lazy
Eclipse-BundleShape: dir
Bundle-Vendor: HHU Düsseldorf STUPS Group
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 42adb93f88fd442fd85330044324823d624752f8..96a04d1a9eb4ae1667be87ccca45209656782dbe 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
@@ -628,7 +628,8 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
String symbol = extension.getSyntaxSymbol();
Object origin = extension.getOrigin();
- Theories.addOrigin(origin);
+ // 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/PredicateVisitor.java b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
index ae555f67f2c389ea58b1baffd121343b6e6a2e49..035811a2be35d24c8b52eb576e29a7dc5b5c37b0 100644
--- a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
+++ b/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
@@ -419,7 +419,10 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
IPredicateExtension extension = predicate.getExtension();
String symbol = extension.getSyntaxSymbol();
Object origin = extension.getOrigin();
- Theories.addOrigin(origin);
+
+ // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+
+ // Theories.addOrigin(origin);
p.setIdentifier(new TIdentifierLiteral(symbol));
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 f7d97a361db5cabddcae12a6e27dda56d32c4ea2..a74d82914e8f220539a04cf6a36eff7a0025293a 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -1,225 +1,198 @@
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;
+// FIXME THEORY-PLUGIN re-enable when the theory plugin was released
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);
- }
+// 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);
+// }
}
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 b3452f62fcf927a86ffe747d2ad429250f09bd4e..43ea5792f26eee7de07938f106ef26696642a2c8 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,11 +144,13 @@ public abstract class EventBTranslator implements ITranslator {
pout.openList();
printProofInformation(refinementChainTranslators, contextTranslators,
pout);
- try {
- Theories.translate(pout);
- } catch (RodinDBException e) {
- e.printStackTrace();
- }
+ // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
+
+ // try {
+ // Theories.translate(pout);
+ // } catch (RodinDBException e) {
+ // e.printStackTrace();
+ // }
pout.closeList();
pout.printVariable("_Error");
pout.closeTerm();
diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml
index 75393d998567f0c9a60c50ea08c1fbe06580feca..0a5cf75cc320b93f7871e7778fef57d9636958fd 100644
--- a/de.prob2.feature/feature.xml
+++ b/de.prob2.feature/feature.xml
@@ -232,16 +232,15 @@ litigation.
<import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/>
<import plugin="org.eclipse.core.databinding.beans" version="1.1.1" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.7.0" match="compatible"/>
+ <import plugin="de.prob.core" version="9.3.0" match="equivalent"/>
<import plugin="org.eventb.core" version="2.1.0"/>
<import plugin="org.rodinp.core" version="1.3.1"/>
+ <import plugin="de.prob.ui" version="7.3.0" match="equivalent"/>
<import plugin="org.eclipse.core.resources" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.expressions" version="3.4.101" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/>
- <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