Skip to content
Snippets Groups Projects
Commit 0eaf49d1 authored by Daniel Plagge's avatar Daniel Plagge
Browse files

Now all deployed theories are translated

parent d2d5a23d
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
de.prob.core/.classpath
+ 9
− 11
View file @ 0eaf49d1
<?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>
de.prob.core/META-INF/MANIFEST.MF
+ 7
− 1
View file @ 0eaf49d1
......@@ -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,
......
de.prob.core/src/de/prob/eventb/translator/ExpressionVisitor.java
+ 0
− 4
View file @ 0eaf49d1
......@@ -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();
......
de.prob.core/src/de/prob/eventb/translator/Theories.java
+ 204
− 190
View file @ 0eaf49d1
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);
}
}
de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+ 5
− 7
View file @ 0eaf49d1
......@@ -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();
......
de.prob.ui/.classpath
+ 1
− 1
View file @ 0eaf49d1
<?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>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment