diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 19b5b62d17480bed9c3f25d0175bd4f9c014e861..f211375fe8992d8e05ebe484a15c3a0138a380e2 100644
--- a/de.prob.core/META-INF/MANIFEST.MF
+++ b/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
diff --git a/de.prob.core/plugin.xml b/de.prob.core/plugin.xml
index 2d7b472c3f23462dc53c415d78961b70f7940e2f..b84a1eaef2043d86514040b1a698b95d501b759d 100644
--- a/de.prob.core/plugin.xml
+++ b/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
diff --git a/de.prob.core/schema/de.prob.translator.exsd b/de.prob.core/schema/de.prob.translator.exsd
new file mode 100644
index 0000000000000000000000000000000000000000..90efcf3ea4b5913068fc906cd4a9206a2d2860b1
--- /dev/null
+++ b/de.prob.core/schema/de.prob.translator.exsd
@@ -0,0 +1,109 @@
+<?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>
diff --git a/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java b/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java
new file mode 100644
index 0000000000000000000000000000000000000000..d01511727a1c9d8cd430d91b88066da528ecce67
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/IExternalTranslator.java
@@ -0,0 +1,7 @@
+package de.prob.core.translator;
+
+import de.prob.prolog.output.PrologTermOutput;
+
+public interface IExternalTranslator {
+ public void writeProlog(PrologTermOutput pto);
+}
diff --git a/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java b/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java
index bb5a1fb6e8b3b20d2032f27880866b171dbffd1a..f1edb0bdac9c2b72b6e03aaaa3948f0a5c6d4f60 100644
--- a/de.prob.core/src/de/prob/core/translator/TranslationFailedException.java
+++ b/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();
+ }
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index 340c94557f3d396764624d39a1ab2a831fc80e26..9ea99009688c58a066ad0add611d91b1e6a429a6 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/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);
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 49af627156fefc608f681e454c9291c95f2d0803..42adb93f88fd442fd85330044324823d624752f8 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+++ b/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
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 7094ecabecf5f2ed6abe1799ca4bca63ff594463..ae555f67f2c389ea58b1baffd121343b6e6a2e49 100644
--- a/de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
+++ b/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) {
-
- // new ClassifiedPragma("discharged", p, proof, Collections.emptyList(), new SourcePosition(-1, -1), new SourcePosition(-1, -1));
+ // 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));
}
- 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);
+ }
+
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
new file mode 100644
index 0000000000000000000000000000000000000000..f7d97a361db5cabddcae12a6e27dda56d32c4ea2
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -0,0 +1,225 @@
+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);
+ }
+
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java b/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java
new file mode 100644
index 0000000000000000000000000000000000000000..d31ff06a2e8cfe0f759cd5a3e1390ad44bc49ea0
--- /dev/null
+++ b/de.prob.core/src/de/prob/eventb/translator/TheoryTranslator.java
@@ -0,0 +1,23 @@
+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"));
+ }
+ }
+ }
+}
diff --git a/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java b/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java
index 0e9a5d1af765473e700a8e24a4306f0caa3d2441..8f7d0c95826235ae17633361922c7237640c9396 100644
--- a/de.prob.core/src/de/prob/eventb/translator/TranslatorFactory.java
+++ b/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();
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 54eb566182fa3856b663293d6f4072e46f81e82b..b3452f62fcf927a86ffe747d2ad429250f09bd4e 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
@@ -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();
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index ba6f53a2ec7b4238cc99f87f50a16c33226f7132..d9fdf6fbb66e8880d7577915fe8fc80d36a17c87 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/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
diff --git a/de.prob2.feature/feature.xml b/de.prob2.feature/feature.xml
index 23cc601c78975e5722e4c177c12239d4cc50c08e..75393d998567f0c9a60c50ea08c1fbe06580feca 100644
--- a/de.prob2.feature/feature.xml
+++ b/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>