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

Re-enable theory plugin in snapshot

parent 996bf355
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
build.gradle
+ 1
− 1
View file @ ada21367
......@@ -6,7 +6,7 @@ project.ext{
targetRepositories = ["http://download.eclipse.org/releases/indigo/",
"http://rodin-b-sharp.sourceforge.net/updates",
"http://rodin-b-sharp.sourceforge.net/core-updates"
// , "http://www.stups.uni-duesseldorf.de/ProB/buildlibs/theory/"
, "http://www.stups.uni-duesseldorf.de/ProB/buildlibs/theory/"
]
groupID = "de.prob"
......
de.prob.core/META-INF/MANIFEST.MF
+ 2
− 2
View file @ ada21367
......@@ -5,8 +5,8 @@ Bundle-SymbolicName: de.prob.core;singleton:=true
Bundle-Version: 9.4.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.5.0,2.6.0)"
REENABLE-FOR-THEORY-PLUGIN: org.eventb.theory.core;bundle-version="2.0.0"
org.eventb.core;bundle-version="[2.5.0,2.6.0)",
org.eventb.theory.core;bundle-version="[2.0.0,3.0.0)";resolution:=optional
Bundle-ActivationPolicy: lazy
Eclipse-BundleShape: dir
Bundle-Vendor: HHU Dusseldorf STUPS Group
......
de.prob.core/src/de/prob/eventb/translator/Theories.java
+ 313
− 319
View file @ ada21367
......@@ -8,33 +8,29 @@ import de.prob.prolog.output.IPrologTermOutput;
public class Theories {
private static final String PROB_THEORY_MAPPING_SUFFIX = "ptm";
public static void translate(IEventBProject project, IPrologTermOutput pout) {
}
// public static void translate(IEventBProject project, IPrologTermOutput
// pout)
// throws TranslationFailedException {
// try {
// final IRodinProject rProject = project.getRodinProject();
// final IDeployedTheoryRoot[] theories = rProject
// .getRootElementsOfType(IDeployedTheoryRoot.ELEMENT_TYPE);
// for (IDeployedTheoryRoot theory : theories) {
// savePrintTranslation(theory, pout);
// }
// final ITheoryPathRoot[] theoryPaths = rProject
// .getRootElementsOfType(ITheoryPathRoot.ELEMENT_TYPE);
// for (ITheoryPathRoot theoryPath : theoryPaths) {
// for (IAvailableTheoryProject ap : theoryPath
// .getAvailableTheoryProjects()) {
// for (IAvailableTheory at : ap.getTheories()) {
// savePrintTranslation(at.getDeployedTheory(), pout);
// }
// }
// }
// } catch (RodinDBException e) {
// throw new TranslationFailedException(e);
// }
// }
public static void translate(IEventBProject project, IPrologTermOutput pout)
throws TranslationFailedException {
try {
final IRodinProject rProject = project.getRodinProject();
final IDeployedTheoryRoot[] theories = rProject
.getRootElementsOfType(IDeployedTheoryRoot.ELEMENT_TYPE);
for (IDeployedTheoryRoot theory : theories) {
savePrintTranslation(theory, pout);
}
final ITheoryPathRoot[] theoryPaths = rProject
.getRootElementsOfType(ITheoryPathRoot.ELEMENT_TYPE);
for (ITheoryPathRoot theoryPath : theoryPaths) {
for (IAvailableTheoryProject ap : theoryPath
.getAvailableTheoryProjects()) {
for (IAvailableTheory at : ap.getTheories()) {
savePrintTranslation(at.getDeployedTheory(), pout);
}
}
}
} catch (RodinDBException e) {
throw new TranslationFailedException(e);
}
}
/**
* We currently write the translated theory into a PrologTerm object because
......@@ -44,297 +40,295 @@ public class Theories {
*
* @throws TranslationFailedException
*/
// private static void savePrintTranslation(IDeployedTheoryRoot theory,
// IPrologTermOutput opto) throws RodinDBException,
// TranslationFailedException {
//
// final StructuredPrologOutput pto = new StructuredPrologOutput();
// printTranslation(theory, pto);
// pto.fullstop();
// final PrologTerm result = pto.getSentences().get(0);
// opto.printTerm(result);
// }
//
// private static void printTranslation(IDeployedTheoryRoot theory,
// StructuredPrologOutput pto) throws RodinDBException,
// TranslationFailedException {
// pto.openTerm("theory");
// printIdentifiers(theory.getSCTypeParameters(), pto);
// printDataTypes(theory, pto);
// printOperatorDefs(theory, pto);
// printAxiomaticDefs(theory, pto);
// findProBMappingFile(theory, pto);
// pto.closeTerm();
// }
//
// private static void findProBMappingFile(IDeployedTheoryRoot theory,
// IPrologTermOutput pto) throws TranslationFailedException {
// final String theoryName = theory.getComponentName();
// final IPath path = new Path(theoryName + "."
// + PROB_THEORY_MAPPING_SUFFIX);
// final IProject project = theory.getRodinProject().getProject();
// final Collection<OperatorMapping> mappings;
// if (project.exists(path)) {
// final IFile file = project.getFile(path);
// mappings = readMappingFile(file, theory);
// } else {
// mappings = Collections.emptyList();
// }
// printMappings(mappings, pto);
// }
//
// private static Collection<OperatorMapping> readMappingFile(IFile file,
// IDeployedTheoryRoot theory) throws TranslationFailedException {
// try {
// final InputStream input = file.getContents();
// final String name = theory.getComponentName();
// final Reader reader = new InputStreamReader(input);
// return TheoryMappingParser.parseTheoryMapping(name, reader);
// } catch (CoreException e) {
// throw new TranslationFailedException(e);
// } catch (TheoryMappingException e) {
// throw new TranslationFailedException(e);
// } catch (IOException e) {
// throw new TranslationFailedException(e);
// }
// }
//
// private static void printMappings(Collection<OperatorMapping> mappings,
// IPrologTermOutput pto) {
// pto.openList();
// // Currently, we support only one kind of operator mapping, just tagging
// // an operator to indicate that an optimized ProB implementation should
// // be used. We do not invest any effort in preparing future kinds of
// // other operator mappings.
// for (OperatorMapping mapping : mappings) {
// pto.openTerm("tag");
// pto.printAtom(mapping.getOperatorName());
// pto.printAtom(mapping.getSpec());
// pto.closeTerm();
// }
// pto.closeList();
// }
//
// private static void printIdentifiers(ISCIdentifierElement[] identifiers,
// IPrologTermOutput pto) throws RodinDBException {
// pto.openList();
// for (ISCIdentifierElement identifier : identifiers) {
// pto.printAtom(identifier.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
// printOperatorArguments(opDef.getOperatorArguments(), prologOutput, ff);
//
// // 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 printOperatorArguments(ISCOperatorArgument[] arguments,
// IPrologTermOutput prologOutput, final FormulaFactory ff)
// throws RodinDBException {
// prologOutput.openList();
// for (ISCOperatorArgument argument : arguments) {
// printTypedIdentifier("argument", argument, ff, prologOutput);
// }
// prologOutput.closeList();
// }
//
// 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());
// Type type = id.getType(ff);
// printType(type, 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 void printAxiomaticDefs(IDeployedTheoryRoot theory,
// IPrologTermOutput pto) throws RodinDBException {
// FormulaFactory ff = theory.getFormulaFactory();
// ITypeEnvironment te = theory.getTypeEnvironment(ff);
// pto.openList();
// for (final ISCAxiomaticDefinitionsBlock block : theory
// .getSCAxiomaticDefinitionsBlocks()) {
// printAxiomaticDefBlock(block, ff, te, pto);
// }
// pto.closeList();
// }
//
// private static void printAxiomaticDefBlock(
// ISCAxiomaticDefinitionsBlock block, FormulaFactory ff,
// ITypeEnvironment te, IPrologTermOutput pto) throws RodinDBException {
// pto.openTerm("axiomatic_def_block");
// pto.printAtom(block.getLabel());
// printIdentifiers(block.getAxiomaticTypeDefinitions(), pto);
// printAxiomaticOperators(block.getAxiomaticOperatorDefinitions(), ff,
// pto);
// printAxioms(block.getAxiomaticDefinitionAxioms(), ff, te, pto);
// pto.closeTerm();
// }
//
// private static void printAxiomaticOperators(
// ISCAxiomaticOperatorDefinition[] axdefs, FormulaFactory ff,
// IPrologTermOutput pto) throws RodinDBException {
// pto.openList();
// for (final ISCAxiomaticOperatorDefinition opdef : axdefs) {
// pto.openTerm("opdef");
// pto.printAtom(opdef.getLabel()); // The label seems to be the
// // operator name
// printOperatorArguments(opdef.getOperatorArguments(), pto, ff);
// pto.openList();
// // WD condition missing
// pto.closeList();
// pto.closeTerm();
// }
// pto.closeList();
// }
//
// private static void printAxioms(ISCAxiomaticDefinitionAxiom[] axioms,
// FormulaFactory ff, ITypeEnvironment te, IPrologTermOutput pto)
// throws RodinDBException {
// pto.openList();
// for (ISCAxiomaticDefinitionAxiom axiom : axioms) {
// printPredicate(pto, axiom.getPredicate(ff, te));
// }
// pto.closeList();
// }
public static void touch() throws NoClassDefFoundError {}
// public static void touch() throws NoClassDefFoundError {
// // Just some dummy code to check if the theory plugin is installed
// @SuppressWarnings("unused")
// String extension = DatabaseUtilities.DEPLOYED_THEORY_FILE_EXTENSION;
// }
private static void savePrintTranslation(IDeployedTheoryRoot theory,
IPrologTermOutput opto) throws RodinDBException,
TranslationFailedException {
final StructuredPrologOutput pto = new StructuredPrologOutput();
printTranslation(theory, pto);
pto.fullstop();
final PrologTerm result = pto.getSentences().get(0);
opto.printTerm(result);
}
private static void printTranslation(IDeployedTheoryRoot theory,
StructuredPrologOutput pto) throws RodinDBException,
TranslationFailedException {
pto.openTerm("theory");
printIdentifiers(theory.getSCTypeParameters(), pto);
printDataTypes(theory, pto);
printOperatorDefs(theory, pto);
printAxiomaticDefs(theory, pto);
findProBMappingFile(theory, pto);
pto.closeTerm();
}
private static void findProBMappingFile(IDeployedTheoryRoot theory,
IPrologTermOutput pto) throws TranslationFailedException {
final String theoryName = theory.getComponentName();
final IPath path = new Path(theoryName + "."
+ PROB_THEORY_MAPPING_SUFFIX);
final IProject project = theory.getRodinProject().getProject();
final Collection<OperatorMapping> mappings;
if (project.exists(path)) {
final IFile file = project.getFile(path);
mappings = readMappingFile(file, theory);
} else {
mappings = Collections.emptyList();
}
printMappings(mappings, pto);
}
private static Collection<OperatorMapping> readMappingFile(IFile file,
IDeployedTheoryRoot theory) throws TranslationFailedException {
try {
final InputStream input = file.getContents();
final String name = theory.getComponentName();
final Reader reader = new InputStreamReader(input);
return TheoryMappingParser.parseTheoryMapping(name, reader);
} catch (CoreException e) {
throw new TranslationFailedException(e);
} catch (TheoryMappingException e) {
throw new TranslationFailedException(e);
} catch (IOException e) {
throw new TranslationFailedException(e);
}
}
private static void printMappings(Collection<OperatorMapping> mappings,
IPrologTermOutput pto) {
pto.openList();
// Currently, we support only one kind of operator mapping, just tagging
// an operator to indicate that an optimized ProB implementation should
// be used. We do not invest any effort in preparing future kinds of
// other operator mappings.
for (OperatorMapping mapping : mappings) {
pto.openTerm("tag");
pto.printAtom(mapping.getOperatorName());
pto.printAtom(mapping.getSpec());
pto.closeTerm();
}
pto.closeList();
}
private static void printIdentifiers(ISCIdentifierElement[] identifiers,
IPrologTermOutput pto) throws RodinDBException {
pto.openList();
for (ISCIdentifierElement identifier : identifiers) {
pto.printAtom(identifier.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
printOperatorArguments(opDef.getOperatorArguments(), prologOutput, ff);
// 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 printOperatorArguments(ISCOperatorArgument[] arguments,
IPrologTermOutput prologOutput, final FormulaFactory ff)
throws RodinDBException {
prologOutput.openList();
for (ISCOperatorArgument argument : arguments) {
printTypedIdentifier("argument", argument, ff, prologOutput);
}
prologOutput.closeList();
}
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());
Type type = id.getType(ff);
printType(type, 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 void printAxiomaticDefs(IDeployedTheoryRoot theory,
IPrologTermOutput pto) throws RodinDBException {
FormulaFactory ff = theory.getFormulaFactory();
ITypeEnvironment te = theory.getTypeEnvironment(ff);
pto.openList();
for (final ISCAxiomaticDefinitionsBlock block : theory
.getSCAxiomaticDefinitionsBlocks()) {
printAxiomaticDefBlock(block, ff, te, pto);
}
pto.closeList();
}
private static void printAxiomaticDefBlock(
ISCAxiomaticDefinitionsBlock block, FormulaFactory ff,
ITypeEnvironment te, IPrologTermOutput pto) throws RodinDBException {
pto.openTerm("axiomatic_def_block");
pto.printAtom(block.getLabel());
printIdentifiers(block.getAxiomaticTypeDefinitions(), pto);
printAxiomaticOperators(block.getAxiomaticOperatorDefinitions(), ff,
pto);
printAxioms(block.getAxiomaticDefinitionAxioms(), ff, te, pto);
pto.closeTerm();
}
private static void printAxiomaticOperators(
ISCAxiomaticOperatorDefinition[] axdefs, FormulaFactory ff,
IPrologTermOutput pto) throws RodinDBException {
pto.openList();
for (final ISCAxiomaticOperatorDefinition opdef : axdefs) {
pto.openTerm("opdef");
pto.printAtom(opdef.getLabel()); // The label seems to be the
// operator name
printOperatorArguments(opdef.getOperatorArguments(), pto, ff);
pto.openList();
// WD condition missing
pto.closeList();
pto.closeTerm();
}
pto.closeList();
}
private static void printAxioms(ISCAxiomaticDefinitionAxiom[] axioms,
FormulaFactory ff, ITypeEnvironment te, IPrologTermOutput pto)
throws RodinDBException {
pto.openList();
for (ISCAxiomaticDefinitionAxiom axiom : axioms) {
printPredicate(pto, axiom.getPredicate(ff, te));
}
pto.closeList();
}
public static void touch() throws NoClassDefFoundError {
// Just some dummy code to check if the theory plugin is installed
@SuppressWarnings("unused")
String extension = DatabaseUtilities.DEPLOYED_THEORY_FILE_EXTENSION;
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment