diff --git a/build.gradle b/build.gradle
index 748ce6adc591ca7c3b9c66a49fd337911fe3ef9e..5c43d9f0721e4b2d6296971d7b6c0810b722c625 100644
--- a/build.gradle
+++ b/build.gradle
@@ -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"
diff --git a/de.prob.core/META-INF/MANIFEST.MF b/de.prob.core/META-INF/MANIFEST.MF
index 0aad54fe970deda71d5ab57eba0266a3837cdc32..1013502daf8f1a93fac673999f87dc02410025cb 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.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
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 1d1940b4f3827037e47ff673ab7ee0a481e10d78..033df8ea5817b974f22b7e9044fe7d7e4010ca60 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -8,34 +8,30 @@ 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
* the translation is currently very unstable and erroneous. Writing in a
@@ -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;
+ }
}