Commit ce1a74f1 authored by Daniel Plagge's avatar Daniel Plagge
Browse files

Added handling for missing theory plugin

parent 161c9162
...@@ -14,6 +14,7 @@ import org.eventb.core.ast.FormulaFactory; ...@@ -14,6 +14,7 @@ import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment; import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.ast.Predicate; import org.eventb.core.ast.Predicate;
import org.eventb.core.ast.Type; import org.eventb.core.ast.Type;
import org.eventb.theory.core.DatabaseUtilities;
import org.eventb.theory.core.IAvailableTheory; import org.eventb.theory.core.IAvailableTheory;
import org.eventb.theory.core.IAvailableTheoryProject; import org.eventb.theory.core.IAvailableTheoryProject;
import org.eventb.theory.core.IDeployedTheoryRoot; import org.eventb.theory.core.IDeployedTheoryRoot;
...@@ -36,6 +37,7 @@ import org.rodinp.core.RodinDBException; ...@@ -36,6 +37,7 @@ import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.PExpression; import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate; import de.be4.classicalb.core.parser.node.PPredicate;
import de.prob.core.translator.TranslationFailedException;
import de.prob.prolog.output.IPrologTermOutput; import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.output.StructuredPrologOutput; import de.prob.prolog.output.StructuredPrologOutput;
import de.prob.prolog.term.PrologTerm; import de.prob.prolog.term.PrologTerm;
...@@ -44,22 +46,26 @@ public class Theories { ...@@ -44,22 +46,26 @@ public class Theories {
private static final String PROB_THEORY_MAPPING_SUFFIX = "ptm"; 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 RodinDBException { throws TranslationFailedException {
final IRodinProject rProject = project.getRodinProject(); try {
final IDeployedTheoryRoot[] theories = rProject final IRodinProject rProject = project.getRodinProject();
.getRootElementsOfType(IDeployedTheoryRoot.ELEMENT_TYPE); final IDeployedTheoryRoot[] theories = rProject
for (IDeployedTheoryRoot theory : theories) { .getRootElementsOfType(IDeployedTheoryRoot.ELEMENT_TYPE);
savePrintTranslation(theory, pout); for (IDeployedTheoryRoot theory : theories) {
} savePrintTranslation(theory, pout);
final ITheoryPathRoot[] theoryPaths = rProject }
.getRootElementsOfType(ITheoryPathRoot.ELEMENT_TYPE); final ITheoryPathRoot[] theoryPaths = rProject
for (ITheoryPathRoot theoryPath : theoryPaths) { .getRootElementsOfType(ITheoryPathRoot.ELEMENT_TYPE);
for (IAvailableTheoryProject ap : theoryPath for (ITheoryPathRoot theoryPath : theoryPaths) {
.getAvailableTheoryProjects()) { for (IAvailableTheoryProject ap : theoryPath
for (IAvailableTheory at : ap.getTheories()) { .getAvailableTheoryProjects()) {
savePrintTranslation(at.getDeployedTheory(), pout); for (IAvailableTheory at : ap.getTheories()) {
savePrintTranslation(at.getDeployedTheory(), pout);
}
} }
} }
} catch (RodinDBException e) {
throw new TranslationFailedException(e);
} }
} }
...@@ -323,4 +329,10 @@ public class Theories { ...@@ -323,4 +329,10 @@ public class Theories {
} }
pto.closeList(); 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;
}
} }
...@@ -16,7 +16,6 @@ import org.eventb.core.IEventBRoot; ...@@ -16,7 +16,6 @@ import org.eventb.core.IEventBRoot;
import org.eventb.core.ISCInternalContext; import org.eventb.core.ISCInternalContext;
import org.eventb.core.ISCMachineRoot; import org.eventb.core.ISCMachineRoot;
import org.rodinp.core.IInternalElement; import org.rodinp.core.IInternalElement;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.Node; import de.be4.classicalb.core.parser.node.Node;
...@@ -29,6 +28,7 @@ import de.prob.prolog.output.IPrologTermOutput; ...@@ -29,6 +28,7 @@ import de.prob.prolog.output.IPrologTermOutput;
public abstract class EventBTranslator implements ITranslator { public abstract class EventBTranslator implements ITranslator {
protected final IEventBProject project; protected final IEventBProject project;
private boolean theoryIsUsed;
protected EventBTranslator(final IEventBRoot root) { protected EventBTranslator(final IEventBRoot root) {
this.project = root.getEventBProject(); this.project = root.getEventBProject();
...@@ -41,7 +41,7 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -41,7 +41,7 @@ public abstract class EventBTranslator implements ITranslator {
this.project = ((ISCMachineRoot) ctx.getRoot()).getEventBProject(); this.project = ((ISCMachineRoot) ctx.getRoot()).getEventBProject();
} }
private LabelPositionPrinter createPrinter( private LabelPositionPrinter createLabelPrositionPrinter(
final Collection<AbstractComponentTranslator> translators) final Collection<AbstractComponentTranslator> translators)
throws TranslationFailedException { throws TranslationFailedException {
LabelPositionPrinter printer = new LabelPositionPrinter(); LabelPositionPrinter printer = new LabelPositionPrinter();
...@@ -53,14 +53,21 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -53,14 +53,21 @@ public abstract class EventBTranslator implements ITranslator {
return printer; return printer;
} }
private void printModels( private Collection<Node> translateModels(
final Collection<? extends AbstractComponentTranslator> refinementChainTranslators, final Collection<? extends AbstractComponentTranslator> refinementChainTranslators) {
Collection<Node> nodes = new ArrayList<Node>();
for (final AbstractComponentTranslator translator : refinementChainTranslators) {
nodes.add(translator.getAST());
theoryIsUsed |= translator.isTheoryUsed();
}
return nodes;
}
private void printModels(final Collection<Node> nodes,
final IPrologTermOutput pout, final ASTProlog prolog) { final IPrologTermOutput pout, final ASTProlog prolog) {
pout.openList(); pout.openList();
for (final Node node : nodes) {
for (final AbstractComponentTranslator translateor : refinementChainTranslators) { node.apply(prolog);
final Node modelAST = translateor.getAST();
modelAST.apply(prolog);
} }
pout.closeList(); pout.closeList();
} }
...@@ -126,19 +133,27 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -126,19 +133,27 @@ public abstract class EventBTranslator implements ITranslator {
Collection<AbstractComponentTranslator> translators = new ArrayList<AbstractComponentTranslator>(); Collection<AbstractComponentTranslator> translators = new ArrayList<AbstractComponentTranslator>();
translators.addAll(refinementChainTranslators); translators.addAll(refinementChainTranslators);
translators.addAll(contextTranslators); translators.addAll(contextTranslators);
return new ASTProlog(pout, createPrinter(translators)); return new ASTProlog(pout, createLabelPrositionPrinter(translators));
} }
protected void printProlog( protected void printProlog(
final Collection<? extends AbstractComponentTranslator> refinementChainTranslators, final Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
final Collection<? extends AbstractComponentTranslator> contextTranslators, final Collection<? extends AbstractComponentTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException { final IPrologTermOutput pout) throws TranslationFailedException {
theoryIsUsed = false;
Collection<Node> machineNodes = translateModels(refinementChainTranslators);
Collection<Node> contextNodes = translateModels(contextTranslators);
if (theoryIsUsed) {
checkIfTheoriesAvailable();
}
final ASTProlog prolog = createAstVisitor(refinementChainTranslators, final ASTProlog prolog = createAstVisitor(refinementChainTranslators,
contextTranslators, pout); contextTranslators, pout);
pout.openTerm("load_event_b_project"); pout.openTerm("load_event_b_project");
printModels(refinementChainTranslators, pout, prolog); printModels(machineNodes, pout, prolog);
printModels(contextTranslators, pout, prolog); printModels(contextNodes, pout, prolog);
pout.openList(); pout.openList();
pout.openTerm("exporter_version"); pout.openTerm("exporter_version");
pout.printNumber(2); pout.printNumber(2);
...@@ -146,12 +161,9 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -146,12 +161,9 @@ public abstract class EventBTranslator implements ITranslator {
printProofInformation(refinementChainTranslators, contextTranslators, printProofInformation(refinementChainTranslators, contextTranslators,
pout); pout);
try {
Theories.translate(project, pout);
} catch (NoClassDefFoundError e) {
} catch (RodinDBException e) { if (theoryIsUsed) {
e.printStackTrace(); translateTheories(project, pout);
} }
printPragmaContents(refinementChainTranslators, contextTranslators, printPragmaContents(refinementChainTranslators, contextTranslators,
...@@ -161,4 +173,20 @@ public abstract class EventBTranslator implements ITranslator { ...@@ -161,4 +173,20 @@ public abstract class EventBTranslator implements ITranslator {
pout.printVariable("_Error"); pout.printVariable("_Error");
pout.closeTerm(); pout.closeTerm();
} }
private void checkIfTheoriesAvailable() throws TranslationFailedException {
try {
Theories.touch();
} catch (NoClassDefFoundError e) {
throw new TranslationFailedException(
"Theory",
"The model to animate makes use of a theory but the theory plug-in is not installed");
}
}
private void translateTheories(IEventBProject project2,
IPrologTermOutput pout) throws TranslationFailedException {
Theories.translate(project, pout);
}
} }
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment