Skip to content
Snippets Groups Projects
Commit b5822082 authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

- removed theory plugin dependency (undo this when the plugin is available through an update site) 

- Code is still there, just uncomment it later
parent 3ae437ae
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 207 additions and 229 deletions
de.prob.core/META-INF/MANIFEST.MF
+ 2
− 2
View file @ b5822082
...@@ -5,8 +5,8 @@ Bundle-SymbolicName: de.prob.core;singleton:=true ...@@ -5,8 +5,8 @@ Bundle-SymbolicName: de.prob.core;singleton:=true
Bundle-Version: 9.3.0.qualifier Bundle-Version: 9.3.0.qualifier
Require-Bundle: org.eclipse.core.runtime;bundle-version="[3.5.0,4.0.0)", 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.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" REENABLE-FOR-THEORY-PLUGIN: org.eventb.theory.core;bundle-version="2.0.0"
Bundle-ActivationPolicy: lazy Bundle-ActivationPolicy: lazy
Eclipse-BundleShape: dir Eclipse-BundleShape: dir
Bundle-Vendor: HHU Düsseldorf STUPS Group Bundle-Vendor: HHU Düsseldorf STUPS Group
......
de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+ 2
− 1
View file @ b5822082
...@@ -628,7 +628,8 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD ...@@ -628,7 +628,8 @@ public class ExpressionVisitor extends SimpleVisitorAdapter implements // NOPMD
String symbol = extension.getSyntaxSymbol(); String symbol = extension.getSyntaxSymbol();
Object origin = extension.getOrigin(); 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)); p.setIdentifier(new TIdentifierLiteral(symbol));
Expression[] expressions = expression.getChildExpressions(); Expression[] expressions = expression.getChildExpressions();
......
de.prob.core/src/de/prob/eventb/translator/PredicateVisitor.java
+ 4
− 1
View file @ b5822082
...@@ -419,7 +419,10 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD ...@@ -419,7 +419,10 @@ public class PredicateVisitor extends SimpleVisitorAdapter implements // NOPMD
IPredicateExtension extension = predicate.getExtension(); IPredicateExtension extension = predicate.getExtension();
String symbol = extension.getSyntaxSymbol(); String symbol = extension.getSyntaxSymbol();
Object origin = extension.getOrigin(); 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)); p.setIdentifier(new TIdentifierLiteral(symbol));
......
de.prob.core/src/de/prob/eventb/translator/Theories.java
+ 190
− 217
View file @ b5822082
package de.prob.eventb.translator; package de.prob.eventb.translator;
import java.util.LinkedList;
import java.util.Map;
import java.util.TreeMap;
import org.eventb.core.ISCIdentifierElement; // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
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 { public class Theories {
private static Map<String, IDeployedTheoryRoot> theories = new TreeMap<String, IDeployedTheoryRoot>(); // private static Map<String, IDeployedTheoryRoot> theories = new TreeMap<String, IDeployedTheoryRoot>();
//
public static final ITypeEnvironment global_te = FormulaFactory // public static final ITypeEnvironment global_te = FormulaFactory
.getDefault().makeTypeEnvironment(); // .getDefault().makeTypeEnvironment();
//
public static void addOrigin(Object origin) { // public static void addOrigin(Object origin) {
if (origin instanceof ISCNewOperatorDefinition) { // if (origin instanceof ISCNewOperatorDefinition) {
final IDeployedTheoryRoot theory = (IDeployedTheoryRoot) ((ISCNewOperatorDefinition) origin) // final IDeployedTheoryRoot theory = (IDeployedTheoryRoot) ((ISCNewOperatorDefinition) origin)
.getParent(); // .getParent();
final String name = theory.getElementName(); // final String name = theory.getElementName();
theories.put(name, theory); // theories.put(name, theory);
} else { // } else {
System.out.println("Did not register origin: " // System.out.println("Did not register origin: "
+ origin.getClass().getName()); // + origin.getClass().getName());
} // }
} // }
//
public static void translate(IPrologTermOutput pto) throws RodinDBException { // public static void translate(IPrologTermOutput pto) throws RodinDBException {
for (IDeployedTheoryRoot theory : theories.values()) { // for (IDeployedTheoryRoot theory : theories.values()) {
printTranslation(theory, pto); // printTranslation(theory, pto);
} // }
} // }
//
private static void printTranslation(IDeployedTheoryRoot theory, // private static void printTranslation(IDeployedTheoryRoot theory,
IPrologTermOutput pto) throws RodinDBException { // IPrologTermOutput pto) throws RodinDBException {
pto.openTerm("theory"); // pto.openTerm("theory");
printTypeParameters(theory, pto); // printTypeParameters(theory, pto);
printDataTypes(theory, pto); // printDataTypes(theory, pto);
printOperatorDefs(theory, pto); // printOperatorDefs(theory, pto);
pto.closeTerm(); // pto.closeTerm();
} // }
//
private static void printTypeParameters(IFormulaExtensionsSource theory, // private static void printTypeParameters(IFormulaExtensionsSource theory,
IPrologTermOutput pto) throws RodinDBException { // IPrologTermOutput pto) throws RodinDBException {
pto.openList(); // pto.openList();
for (ISCTypeParameter parameter : theory.getSCTypeParameters()) { // for (ISCTypeParameter parameter : theory.getSCTypeParameters()) {
pto.printAtom(parameter.getIdentifierString()); // pto.printAtom(parameter.getIdentifierString());
} // }
pto.closeList(); // pto.closeList();
} // }
//
private static void printDataTypes(IDeployedTheoryRoot theory, // private static void printDataTypes(IDeployedTheoryRoot theory,
IPrologTermOutput pto) throws RodinDBException { // IPrologTermOutput pto) throws RodinDBException {
final FormulaFactory ff = theory.getFormulaFactory(); // final FormulaFactory ff = theory.getFormulaFactory();
pto.openList(); // pto.openList();
for (ISCDatatypeDefinition def : theory.getSCDatatypeDefinitions()) { // for (ISCDatatypeDefinition def : theory.getSCDatatypeDefinitions()) {
printDataType(def, ff, pto); // printDataType(def, ff, pto);
} // }
pto.closeList(); // pto.closeList();
} // }
//
private static void printDataType(ISCDatatypeDefinition def, // private static void printDataType(ISCDatatypeDefinition def,
FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException { // FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
pto.openTerm("datatype"); // pto.openTerm("datatype");
pto.printAtom(def.getIdentifierString()); // pto.printAtom(def.getIdentifierString());
pto.openList(); // pto.openList();
for (ISCTypeArgument arg : def.getTypeArguments()) { // for (ISCTypeArgument arg : def.getTypeArguments()) {
printType(arg.getSCGivenType(ff), ff, pto); // printType(arg.getSCGivenType(ff), ff, pto);
} // }
pto.closeList(); // pto.closeList();
pto.openList(); // pto.openList();
for (ISCDatatypeConstructor cons : def.getConstructors()) { // for (ISCDatatypeConstructor cons : def.getConstructors()) {
printConstructor(cons, ff, pto); // printConstructor(cons, ff, pto);
} // }
pto.closeList(); // pto.closeList();
pto.closeTerm(); // pto.closeTerm();
//
} // }
//
private static void printConstructor(ISCDatatypeConstructor cons, // private static void printConstructor(ISCDatatypeConstructor cons,
FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException { // FormulaFactory ff, IPrologTermOutput pto) throws RodinDBException {
pto.openTerm("constructor"); // pto.openTerm("constructor");
pto.printAtom(cons.getIdentifierString()); // pto.printAtom(cons.getIdentifierString());
pto.openList(); // pto.openList();
for (ISCConstructorArgument arg : cons.getConstructorArguments()) { // for (ISCConstructorArgument arg : cons.getConstructorArguments()) {
printTypedIdentifier("destructor", arg, ff, pto); // printTypedIdentifier("destructor", arg, ff, pto);
} // }
pto.closeList(); // pto.closeList();
pto.closeTerm(); // pto.closeTerm();
//
} // }
//
private static void printOperatorDefs(IDeployedTheoryRoot theory, // private static void printOperatorDefs(IDeployedTheoryRoot theory,
IPrologTermOutput pto) throws RodinDBException { // IPrologTermOutput pto) throws RodinDBException {
pto.openList(); // pto.openList();
for (ISCNewOperatorDefinition opdef : theory // for (ISCNewOperatorDefinition opdef : theory
.getSCNewOperatorDefinitions()) { // .getSCNewOperatorDefinitions()) {
printOperator(opdef, theory, pto); // printOperator(opdef, theory, pto);
} // }
pto.closeList(); // pto.closeList();
} // }
//
private static void printOperator(ISCNewOperatorDefinition opDef, // private static void printOperator(ISCNewOperatorDefinition opDef,
IDeployedTheoryRoot theory, IPrologTermOutput prologOutput) // IDeployedTheoryRoot theory, IPrologTermOutput prologOutput)
throws RodinDBException { // throws RodinDBException {
//
prologOutput.openTerm("operator"); // prologOutput.openTerm("operator");
prologOutput.printAtom(opDef.getLabel()); // prologOutput.printAtom(opDef.getLabel());
//
final FormulaFactory ff = theory.getFormulaFactory(); // final FormulaFactory ff = theory.getFormulaFactory();
final ITypeEnvironment te = theory.getTypeEnvironment(ff); // final ITypeEnvironment te = theory.getTypeEnvironment(ff);
//
// Arguments // // Arguments
prologOutput.openList(); // prologOutput.openList();
ISCOperatorArgument[] operatorArguments = opDef.getOperatorArguments(); // ISCOperatorArgument[] operatorArguments = opDef.getOperatorArguments();
for (ISCOperatorArgument argument : operatorArguments) { // for (ISCOperatorArgument argument : operatorArguments) {
printTypedIdentifier("argument", argument, ff, prologOutput); // printTypedIdentifier("argument", argument, ff, prologOutput);
} // }
prologOutput.closeList(); // prologOutput.closeList();
//
// WD Condition // // WD Condition
Predicate wdCondition = opDef.getWDCondition(ff, te); // Predicate wdCondition = opDef.getWDCondition(ff, te);
printPredicate(prologOutput, wdCondition); // printPredicate(prologOutput, wdCondition);
//
// Direct Definitions // // Direct Definitions
prologOutput.openList(); // prologOutput.openList();
processDefinitions(ff, te, prologOutput, // processDefinitions(ff, te, prologOutput,
opDef.getDirectOperatorDefinitions()); // opDef.getDirectOperatorDefinitions());
prologOutput.closeList(); // prologOutput.closeList();
//
// Recursive Definitions // // Recursive Definitions
prologOutput.openList(); // prologOutput.openList();
ISCRecursiveOperatorDefinition[] definitions = opDef // ISCRecursiveOperatorDefinition[] definitions = opDef
.getRecursiveOperatorDefinitions(); // .getRecursiveOperatorDefinitions();
for (ISCRecursiveOperatorDefinition definition : definitions) { // for (ISCRecursiveOperatorDefinition definition : definitions) {
ISCRecursiveDefinitionCase[] recursiveDefinitionCases = definition // ISCRecursiveDefinitionCase[] recursiveDefinitionCases = definition
.getRecursiveDefinitionCases(); // .getRecursiveDefinitionCases();
for (ISCRecursiveDefinitionCase c : recursiveDefinitionCases) { // for (ISCRecursiveDefinitionCase c : recursiveDefinitionCases) {
Expression ex = c.getExpression(ff, te); // Expression ex = c.getExpression(ff, te);
printExpression(prologOutput, ex); // printExpression(prologOutput, ex);
} // }
} // }
prologOutput.closeList(); // prologOutput.closeList();
//
prologOutput.closeTerm(); // prologOutput.closeTerm();
} // }
//
private static void processDefinitions(FormulaFactory ff, // private static void processDefinitions(FormulaFactory ff,
ITypeEnvironment te, IPrologTermOutput prologOutput, // ITypeEnvironment te, IPrologTermOutput prologOutput,
ISCDirectOperatorDefinition[] directOperatorDefinitions) // ISCDirectOperatorDefinition[] directOperatorDefinitions)
throws RodinDBException { // throws RodinDBException {
for (ISCDirectOperatorDefinition def : directOperatorDefinitions) { // for (ISCDirectOperatorDefinition def : directOperatorDefinitions) {
Formula<?> scFormula = def.getSCFormula(ff, te); // Formula<?> scFormula = def.getSCFormula(ff, te);
//
if (scFormula instanceof Predicate) { // if (scFormula instanceof Predicate) {
Predicate pp = (Predicate) scFormula; // Predicate pp = (Predicate) scFormula;
printPredicate(prologOutput, pp); // printPredicate(prologOutput, pp);
} // }
if (scFormula instanceof Expression) { // if (scFormula instanceof Expression) {
Expression pp = (Expression) scFormula; // Expression pp = (Expression) scFormula;
printExpression(prologOutput, pp); // printExpression(prologOutput, pp);
} // }
//
} // }
} // }
//
private static void printTypedIdentifier(final String functor, // private static void printTypedIdentifier(final String functor,
final ISCIdentifierElement id, final FormulaFactory ff, // final ISCIdentifierElement id, final FormulaFactory ff,
final IPrologTermOutput pto) throws RodinDBException { // final IPrologTermOutput pto) throws RodinDBException {
pto.openTerm(functor); // pto.openTerm(functor);
pto.printAtom(id.getIdentifierString()); // pto.printAtom(id.getIdentifierString());
printType(id.getType(ff), ff, pto); // printType(id.getType(ff), ff, pto);
pto.closeTerm(); // pto.closeTerm();
} // }
//
private static void printType(final Type type, final FormulaFactory ff, // private static void printType(final Type type, final FormulaFactory ff,
final IPrologTermOutput pto) { // final IPrologTermOutput pto) {
printExpression(pto, type.toExpression(ff)); // printExpression(pto, type.toExpression(ff));
} // }
//
private static void printExpression(IPrologTermOutput prologOutput, // private static void printExpression(IPrologTermOutput prologOutput,
Expression pp) { // Expression pp) {
ExpressionVisitor visitor = new ExpressionVisitor( // ExpressionVisitor visitor = new ExpressionVisitor(
new LinkedList<String>()); // new LinkedList<String>());
pp.accept(visitor); // pp.accept(visitor);
PExpression ex = visitor.getExpression(); // PExpression ex = visitor.getExpression();
ASTProlog pv = new ASTProlog(prologOutput, null); // ASTProlog pv = new ASTProlog(prologOutput, null);
ex.apply(pv); // ex.apply(pv);
} // }
//
private static void printPredicate(IPrologTermOutput prologOutput, // private static void printPredicate(IPrologTermOutput prologOutput,
Predicate pp) { // Predicate pp) {
PredicateVisitor visitor = new PredicateVisitor( // PredicateVisitor visitor = new PredicateVisitor(
new LinkedList<String>()); // new LinkedList<String>());
pp.accept(visitor); // pp.accept(visitor);
PPredicate predicate = visitor.getPredicate(); // PPredicate predicate = visitor.getPredicate();
ASTProlog pv = new ASTProlog(prologOutput, null); // ASTProlog pv = new ASTProlog(prologOutput, null);
predicate.apply(pv); // predicate.apply(pv);
} // }
} }
de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+ 7
− 5
View file @ b5822082
...@@ -144,11 +144,13 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -144,11 +144,13 @@ public abstract class EventBTranslator implements ITranslator {
pout.openList(); pout.openList();
printProofInformation(refinementChainTranslators, contextTranslators, printProofInformation(refinementChainTranslators, contextTranslators,
pout); pout);
try { // FIXME THEORY-PLUGIN re-enable when the theory plugin was released
Theories.translate(pout);
} catch (RodinDBException e) { // try {
e.printStackTrace(); // Theories.translate(pout);
} // } catch (RodinDBException e) {
// e.printStackTrace();
// }
pout.closeList(); pout.closeList();
pout.printVariable("_Error"); pout.printVariable("_Error");
pout.closeTerm(); pout.closeTerm();
......
de.prob2.feature/feature.xml
+ 2
− 3
View file @ b5822082
...@@ -232,16 +232,15 @@ litigation. ...@@ -232,16 +232,15 @@ litigation.
<import plugin="org.eclipse.jface.databinding" version="1.2.1" match="compatible"/> <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.core.databinding.beans" version="1.1.1" match="compatible"/>
<import plugin="org.eclipse.gef" version="3.7.0" 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.eventb.core" version="2.1.0"/>
<import plugin="org.rodinp.core" version="1.3.1"/> <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.resources" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.core.expressions" version="3.4.101" 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.gef" version="3.5.0" match="compatible"/>
<import plugin="org.eclipse.ui.navigator" version="3.5.0" match="greaterOrEqual"/> <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="de.bmotionstudio.gef.editor" version="5.4.0" match="equivalent"/>
<import plugin="org.eventb.theory.core" version="1.3.0" match="greaterOrEqual"/>
</requires> </requires>
<plugin <plugin
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment