diff --git a/de.prob.core/src/de/prob/eventb/translator/AbstractComponentTranslator.java b/de.prob.core/src/de/prob/eventb/translator/AbstractComponentTranslator.java
index 5e64e8e77dfd79a432892d127cd75f5725e3e2fc..69c7cb6cd836d106c8f9a6ba8c9560cd51eeea7b 100644
--- a/de.prob.core/src/de/prob/eventb/translator/AbstractComponentTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/AbstractComponentTranslator.java
@@ -6,13 +6,32 @@
package de.prob.eventb.translator;
+import java.util.ArrayList;
import java.util.Collections;
+import java.util.LinkedList;
+import java.util.List;
import java.util.Map;
import java.util.concurrent.ConcurrentHashMap;
+import org.eventb.core.ISCExpressionElement;
+import org.eventb.core.ISCIdentifierElement;
+import org.eventb.core.ISCPredicateElement;
+import org.eventb.core.ast.Expression;
+import org.eventb.core.ast.FormulaFactory;
+import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.ast.Predicate;
+import org.rodinp.core.IAttributeType;
import org.rodinp.core.IInternalElement;
+import org.rodinp.core.RodinCore;
+import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.node.PPredicate;
+import de.prob.core.translator.pragmas.IPragma;
+import de.prob.core.translator.pragmas.UnitPragma;
+import de.prob.eventb.translator.internal.ProofObligation;
+import de.prob.eventb.translator.internal.TranslationVisitor;
public abstract class AbstractComponentTranslator {
@@ -21,7 +40,83 @@ public abstract class AbstractComponentTranslator {
public Map<Node, IInternalElement> getLabelMapping() {
return Collections.unmodifiableMap(labelMapping);
}
-
- abstract public String getResource();
+
+ private boolean theoryIsUsed = false;
+ private final List<IPragma> pragmas = new ArrayList<IPragma>();
+ private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
+ private final String resourceName;
+
+ protected AbstractComponentTranslator(String resourceName) {
+ this.resourceName = resourceName;
+ }
+
+ public String getResource() {
+ return resourceName;
+ }
+
+ public List<IPragma> getPragmas() {
+ return Collections.unmodifiableList(pragmas);
+ }
+
+ public List<ProofObligation> getProofs() {
+ return Collections.unmodifiableList(proofs);
+ }
+
+ protected void addProof(ProofObligation po) {
+ proofs.add(po);
+ }
+
+ protected void addUnitPragmas(ISCIdentifierElement[] elements)
+ throws RodinDBException {
+ try {
+ final IAttributeType.String UNITATTRIBUTE = RodinCore
+ .getStringAttrType("de.prob.units.unitPragmaAttribute");
+
+ for (final ISCIdentifierElement variable : elements) {
+ if (variable.hasAttribute(UNITATTRIBUTE)) {
+ String content = variable.getAttributeValue(UNITATTRIBUTE);
+
+ if (!content.isEmpty()) {
+ pragmas.add(new UnitPragma(getResource(), variable
+ .getIdentifierString(), content));
+ }
+ }
+ }
+ } catch (IllegalArgumentException ex) {
+ // Happens if the attribute does not exist, i.e. the unit plugin is
+ // not installed
+ }
+
+ }
+
+ protected PPredicate translatePredicate(FormulaFactory ff,
+ final ITypeEnvironment env, final ISCPredicateElement predicate)
+ throws RodinDBException {
+ final PredicateVisitor visitor = new PredicateVisitor(
+ new LinkedList<String>());
+ final Predicate pred = predicate.getPredicate(ff, env);
+ pred.accept(visitor);
+ final PPredicate result = visitor.getPredicate();
+ theoryIsUsed |= TranslationVisitor.checkNewImplementation(pred, result);
+ return result;
+ }
+
+ protected PExpression translateExpression(FormulaFactory ff,
+ final ITypeEnvironment env, final ISCExpressionElement expression)
+ throws RodinDBException {
+ final ExpressionVisitor visitor = new ExpressionVisitor(
+ new LinkedList<String>());
+ final Expression expr = expression.getExpression(ff, env);
+ expr.accept(visitor);
+ final PExpression result = visitor.getExpression();
+ theoryIsUsed |= TranslationVisitor.checkNewImplementation(expr, result);
+ return result;
+ }
+
+ public boolean isTheoryUsed() {
+ return theoryIsUsed;
+ }
+
+ abstract public Node getAST();
}
\ No newline at end of file
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index ed06174c383f320972bcd7542360bafa60cd4bc5..4322265947bc67873a3610dbb0010940d9957d9c 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -31,14 +31,11 @@ import org.eventb.core.ISCExtendsContext;
import org.eventb.core.ISCInternalContext;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
-import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IConfidence;
-import org.rodinp.core.IAttributeType;
import org.rodinp.core.IInternalElement;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.IRodinProject;
-import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.analysis.pragma.internal.ClassifiedPragma;
@@ -50,6 +47,7 @@ import de.be4.classicalb.core.parser.node.AExtendsContextClause;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.ASetsContextClause;
import de.be4.classicalb.core.parser.node.ATheoremsContextClause;
+import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PContextClause;
import de.be4.classicalb.core.parser.node.PExpression;
import de.be4.classicalb.core.parser.node.PPredicate;
@@ -57,12 +55,9 @@ import de.be4.classicalb.core.parser.node.PSet;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.prob.core.translator.TranslationFailedException;
-import de.prob.core.translator.pragmas.IPragma;
-import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.internal.EProofStatus;
import de.prob.eventb.translator.internal.ProofObligation;
import de.prob.eventb.translator.internal.SequentSource;
-import de.prob.eventb.translator.internal.TranslationVisitor;
public final class ContextTranslator extends AbstractComponentTranslator {
@@ -70,9 +65,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private final ISCContext context;
private final AEventBContextParseUnit model = new AEventBContextParseUnit();
private final Map<String, ISCContext> depContext = new HashMap<String, ISCContext>();
- private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
private final List<ClassifiedPragma> proofspragmas = new ArrayList<ClassifiedPragma>();
- private final List<IPragma> pragmas = new ArrayList<IPragma>();
private final IEventBRoot root;
private final FormulaFactory ff;
@@ -159,6 +152,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private ContextTranslator(final ISCContext context,
final FormulaFactory ff, final ITypeEnvironment te,
final IEventBRoot root) throws TranslationFailedException {
+ super(context.getComponentName());
this.context = context;
this.ff = ff;
this.te = te;
@@ -173,26 +167,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
private void collectPragmas() throws RodinDBException {
// unit pragma, attached to constants
- try {
- final IAttributeType.String UNITATTRIBUTE = RodinCore
- .getStringAttrType("de.prob.units.unitPragmaAttribute");
-
- final ISCConstant[] constants = context.getSCConstants();
-
- for (final ISCConstant constant : constants) {
- if (constant.hasAttribute(UNITATTRIBUTE)) {
- String content = constant.getAttributeValue(UNITATTRIBUTE);
-
- if (!content.isEmpty()) {
- pragmas.add(new UnitPragma(getResource(), constant
- .getIdentifierString(), content));
- }
- }
- }
- } catch (IllegalArgumentException ex) {
- // Happens if the attribute does not exist, i.e. the unit plugin is
- // not installed
- }
+ addUnitPragmas(context.getSCConstants());
}
private void collectProofInfo() throws RodinDBException {
@@ -241,7 +216,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
.getLabel()));
}
- proofs.add(new ProofObligation(origin, s, name, pstatus));
+ addProof(new ProofObligation(origin, s, name, pstatus));
}
}
@@ -382,12 +357,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
predicates.length);
for (final ISCAxiom element : predicates) {
if (element.isTheorem() == theorems) {
- final PredicateVisitor visitor = new PredicateVisitor(
- new LinkedList<String>());
- final Predicate p = element.getPredicate(ff, te);
- p.accept(visitor);
- final PPredicate predicate = visitor.getPredicate();
- TranslationVisitor.checkNewImplementation(p, predicate);
+ final PPredicate predicate = translatePredicate(ff, te, element);
list.add(predicate);
labelMapping.put(predicate, element);
proofspragmas.add(new ClassifiedPragma("discharged", predicate,
@@ -398,14 +368,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return list;
}
- public List<ProofObligation> getProofs() {
- return proofs;
- }
-
- public List<IPragma> getPragmas() {
- return pragmas;
- }
-
public List<ClassifiedPragma> getProofspragmas() {
return proofspragmas;
}
@@ -415,4 +377,9 @@ public final class ContextTranslator extends AbstractComponentTranslator {
return context.getComponentName();
}
+ @Override
+ public Node getAST() {
+ return getContextAST();
+ }
+
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
index b1edb97e3b185017e1b3ba7c097985a46011e827..21d51c5cc4ca7931cab48da34d058bf745089b39 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/EventBTranslator.java
@@ -19,14 +19,11 @@ 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.node.AEventBContextParseUnit;
-import de.be4.classicalb.core.parser.node.AEventBModelParseUnit;
import de.be4.classicalb.core.parser.node.Node;
import de.prob.core.translator.ITranslator;
import de.prob.core.translator.TranslationFailedException;
import de.prob.core.translator.pragmas.IPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
-import de.prob.eventb.translator.ContextTranslator;
import de.prob.eventb.translator.Theories;
import de.prob.prolog.output.IPrologTermOutput;
@@ -56,42 +53,29 @@ public abstract class EventBTranslator implements ITranslator {
return printer;
}
- private void printContexts(
- final Collection<ContextTranslator> contextTranslators,
- final IPrologTermOutput pout, final ASTProlog prolog) {
- pout.openList();
- for (final ContextTranslator contextTranslator : contextTranslators) {
- final AEventBContextParseUnit contextAST = contextTranslator
- .getContextAST();
- contextAST.apply(prolog);
- }
- pout.closeList();
- }
-
private void printModels(
- final Collection<ModelTranslator> refinementChainTranslators,
+ final Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
final IPrologTermOutput pout, final ASTProlog prolog) {
pout.openList();
- for (final ModelTranslator modelTranslator : refinementChainTranslators) {
- final AEventBModelParseUnit modelAST = modelTranslator
- .getModelAST();
+ for (final AbstractComponentTranslator translateor : refinementChainTranslators) {
+ final Node modelAST = translateor.getAST();
modelAST.apply(prolog);
}
pout.closeList();
}
private void printProofInformation(
- final Collection<ModelTranslator> refinementChainTranslators,
- Collection<ContextTranslator> contextTranslators,
+ final Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
+ Collection<? extends AbstractComponentTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
ArrayList<ProofObligation> list = new ArrayList<ProofObligation>();
- for (ContextTranslator contextTranslator : contextTranslators) {
+ for (AbstractComponentTranslator contextTranslator : contextTranslators) {
list.addAll(contextTranslator.getProofs());
}
- for (ModelTranslator modelTranslator : refinementChainTranslators) {
+ for (AbstractComponentTranslator modelTranslator : refinementChainTranslators) {
list.addAll(modelTranslator.getProofs());
}
@@ -116,15 +100,15 @@ public abstract class EventBTranslator implements ITranslator {
}
private void printPragmaContents(
- Collection<ModelTranslator> refinementChainTranslators,
- Collection<ContextTranslator> contextTranslators,
+ Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
+ Collection<? extends AbstractComponentTranslator> contextTranslators,
IPrologTermOutput pout) {
ArrayList<IPragma> pragmas = new ArrayList<IPragma>();
- for (ContextTranslator contextTranslator : contextTranslators) {
+ for (AbstractComponentTranslator contextTranslator : contextTranslators) {
pragmas.addAll(contextTranslator.getPragmas());
}
- for (ModelTranslator modelTranslator : refinementChainTranslators) {
+ for (AbstractComponentTranslator modelTranslator : refinementChainTranslators) {
pragmas.addAll(modelTranslator.getPragmas());
}
@@ -136,8 +120,8 @@ public abstract class EventBTranslator implements ITranslator {
protected abstract void printFlowInformation(final IPrologTermOutput pout);
private ASTProlog createAstVisitor(
- final Collection<ModelTranslator> refinementChainTranslators,
- final Collection<ContextTranslator> contextTranslators,
+ final Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
+ final Collection<? extends AbstractComponentTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
Collection<AbstractComponentTranslator> translators = new ArrayList<AbstractComponentTranslator>();
translators.addAll(refinementChainTranslators);
@@ -146,15 +130,15 @@ public abstract class EventBTranslator implements ITranslator {
}
protected void printProlog(
- final Collection<ModelTranslator> refinementChainTranslators,
- final Collection<ContextTranslator> contextTranslators,
+ final Collection<? extends AbstractComponentTranslator> refinementChainTranslators,
+ final Collection<? extends AbstractComponentTranslator> contextTranslators,
final IPrologTermOutput pout) throws TranslationFailedException {
final ASTProlog prolog = createAstVisitor(refinementChainTranslators,
contextTranslators, pout);
pout.openTerm("load_event_b_project");
printModels(refinementChainTranslators, pout, prolog);
- printContexts(contextTranslators, pout, prolog);
+ printModels(contextTranslators, pout, prolog);
pout.openList();
pout.openTerm("exporter_version");
pout.printNumber(2);
@@ -164,6 +148,8 @@ public abstract class EventBTranslator implements ITranslator {
pout);
try {
Theories.translate(project, pout);
+ } catch (NoClassDefFoundError e) {
+
} catch (RodinDBException e) {
e.printStackTrace();
}
diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
index 5aaacd2ab0b38d194b81fd554751f15f9576ff77..45049f26186f142fef8e614154bf1e2a32fc1c6c 100644
--- a/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java
@@ -9,7 +9,6 @@ package de.prob.eventb.translator.internal; // NOPMD by bendisposto
import java.util.ArrayList;
import java.util.Arrays;
-import java.util.Collections;
import java.util.LinkedList;
import java.util.List;
@@ -37,13 +36,10 @@ import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
-import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IConfidence;
-import org.rodinp.core.IAttributeType;
import org.rodinp.core.IElementType;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
-import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
import de.be4.classicalb.core.parser.node.AAnticipatedEventstatus;
@@ -60,6 +56,7 @@ import de.be4.classicalb.core.parser.node.ATheoremsModelClause;
import de.be4.classicalb.core.parser.node.AVariablesModelClause;
import de.be4.classicalb.core.parser.node.AVariantModelClause;
import de.be4.classicalb.core.parser.node.AWitness;
+import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.PEvent;
import de.be4.classicalb.core.parser.node.PEventstatus;
import de.be4.classicalb.core.parser.node.PExpression;
@@ -69,12 +66,8 @@ import de.be4.classicalb.core.parser.node.PSubstitution;
import de.be4.classicalb.core.parser.node.PWitness;
import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
import de.prob.core.translator.TranslationFailedException;
-import de.prob.core.translator.pragmas.IPragma;
-import de.prob.core.translator.pragmas.UnitPragma;
import de.prob.eventb.translator.AbstractComponentTranslator;
import de.prob.eventb.translator.AssignmentVisitor;
-import de.prob.eventb.translator.ExpressionVisitor;
-import de.prob.eventb.translator.PredicateVisitor;
import de.prob.logging.Logger;
public class ModelTranslator extends AbstractComponentTranslator {
@@ -84,8 +77,6 @@ public class ModelTranslator extends AbstractComponentTranslator {
private final FormulaFactory ff;
private final ITypeEnvironment te;
private final IMachineRoot origin;
- private final List<ProofObligation> proofs = new ArrayList<ProofObligation>();
- private final List<IPragma> pragmas = new ArrayList<IPragma>();
// private final List<String> depContext = new ArrayList<String>();
@@ -119,14 +110,6 @@ public class ModelTranslator extends AbstractComponentTranslator {
return modelTranslator;
}
- public List<ProofObligation> getProofs() {
- return Collections.unmodifiableList(proofs);
- }
-
- public List<IPragma> getPragmas() {
- return Collections.unmodifiableList(pragmas);
- }
-
public AEventBModelParseUnit getModelAST() {
if (broken) {
final String message = "The machine contains Rodin Problems. Please fix it before animating";
@@ -149,6 +132,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
private ModelTranslator(final ISCMachineRoot machine)
throws TranslationFailedException {
+ super(machine.getComponentName());
this.machine = machine;
origin = machine.getMachineRoot();
ff = ((ISCMachineRoot) machine).getFormulaFactory();
@@ -181,26 +165,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
private void collectPragmas() throws RodinDBException {
// unit pragma, attached to variables
- try {
- final IAttributeType.String UNITATTRIBUTE = RodinCore
- .getStringAttrType("de.prob.units.unitPragmaAttribute");
-
- final ISCVariable[] variables = machine.getSCVariables();
-
- for (final ISCVariable variable : variables) {
- if (variable.hasAttribute(UNITATTRIBUTE)) {
- String content = variable.getAttributeValue(UNITATTRIBUTE);
-
- if (!content.isEmpty()) {
- pragmas.add(new UnitPragma(getResource(), variable
- .getIdentifierString(), content));
- }
- }
- }
- } catch (IllegalArgumentException ex) {
- // Happens if the attribute does not exist, i.e. the unit plugin is
- // not installed
- }
+ addUnitPragmas(machine.getSCVariables());
}
private void collectProofInfo() throws RodinDBException {
@@ -244,7 +209,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
s.add(new SequentSource(type, le.getLabel()));
}
- proofs.add(new ProofObligation(origin, s, name, pstatus));
+ addProof(new ProofObligation(origin, s, name, pstatus));
}
if (!bugs.isEmpty()) {
@@ -284,10 +249,9 @@ public class ModelTranslator extends AbstractComponentTranslator {
final ISCVariant[] variant = machine.getSCVariants();
final AVariantModelClause var;
if (variant.length == 1) {
- final ExpressionVisitor visitor = new ExpressionVisitor(
- new LinkedList<String>());
- variant[0].getExpression(ff, te).accept(visitor);
- var = new AVariantModelClause(visitor.getExpression());
+ final PExpression expression = translateExpression(ff, te,
+ variant[0]);
+ var = new AVariantModelClause(expression);
} else if (variant.length == 0) {
var = null;
} else
@@ -423,15 +387,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
final List<PPredicate> theoremsList) throws RodinDBException {
final ISCGuard[] guards = revent.getSCGuards();
for (final ISCGuard guard : guards) {
- final PredicateVisitor visitor = new PredicateVisitor(
- new LinkedList<String>());
- final Predicate guardPredicate = guard.getPredicate(ff, localEnv);
- // System.out.println("GUARD: " + guard.getLabel() + " -> "
- // + guardPredicate);
- guardPredicate.accept(visitor);
- final PPredicate predicate = visitor.getPredicate();
- TranslationVisitor
- .checkNewImplementation(guardPredicate, predicate);
+ final PPredicate predicate = translatePredicate(ff, localEnv, guard);
if (guard.isTheorem()) {
theoremsList.add(predicate);
} else {
@@ -466,11 +422,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
final List<PWitness> witnessList = new ArrayList<PWitness>(
witnesses.length);
for (final ISCWitness witness : witnesses) {
- final PredicateVisitor visitor = new PredicateVisitor(
- new LinkedList<String>());
- final Predicate pp = witness.getPredicate(ff, localEnv);
- pp.accept(visitor);
- final PPredicate predicate = visitor.getPredicate();
+ final PPredicate predicate = translatePredicate(ff, localEnv,
+ witness);
final TIdentifierLiteral label = new TIdentifierLiteral(
witness.getLabel());
witnessList.add(new AWitness(label, predicate));
@@ -533,12 +486,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
// only use predicates that are defined in the current refinement
// level, not in an abstract machine
if (!isDefinedInAbstraction(evPredicate)) {
- final PredicateVisitor visitor = new PredicateVisitor(
- new LinkedList<String>());
- Predicate p = evPredicate.getPredicate(ff, te);
- p.accept(visitor);
- final PPredicate predicate = visitor.getPredicate();
- TranslationVisitor.checkNewImplementation(p, predicate);
+ final PPredicate predicate = translatePredicate(ff, te,
+ evPredicate);
list.add(predicate);
labelMapping.put(predicate, evPredicate);
}
@@ -573,8 +522,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
}
@Override
- public String getResource() {
- return machine.getComponentName();
+ public Node getAST() {
+ return getModelAST();
}
-
}