From 0cf8520d6e8109bffc0e682fdfccd51a18e2140f Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Wed, 2 Jan 2013 15:33:12 +0100
Subject: [PATCH] translation of units pragmas in machines, contexts next
---
.../core/translator/pragmas/UnitPragma.java | 26 +++++++++++++++++++
.../eventb/translator/ContextTranslator.java | 23 +++++++++++++---
.../translator/internal/ModelTranslator.java | 21 +++++++++++++--
.../ui/eventb/StartUnitAnalysisHandler.java | 8 +++---
4 files changed, 69 insertions(+), 9 deletions(-)
create mode 100644 de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
diff --git a/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
new file mode 100644
index 00000000..851fa593
--- /dev/null
+++ b/de.prob.core/src/de/prob/core/translator/pragmas/UnitPragma.java
@@ -0,0 +1,26 @@
+package de.prob.core.translator.pragmas;
+
+import de.prob.prolog.output.IPrologTermOutput;
+
+public class UnitPragma implements IPragma {
+ private String definedIn;
+ private String attachedTo;
+ private String content;
+
+ public UnitPragma(String definedIn, String attachedTo, String content) {
+ this.definedIn = definedIn;
+ this.attachedTo = attachedTo;
+ this.content = content;
+ }
+
+ @Override
+ public void output(IPrologTermOutput pout) {
+ pout.openTerm("pragma");
+ pout.printAtom("unit");
+ pout.printAtom(definedIn);
+ pout.printAtom(attachedTo);
+ pout.printAtom(content);
+ pout.closeTerm();
+ }
+
+}
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 62fb49e4..bc24a254 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -32,9 +32,11 @@ import org.eventb.core.ISCMachineRoot;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
import org.eventb.core.seqprover.IConfidence;
+import org.rodinp.core.IAttributeType;
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;
@@ -52,8 +54,10 @@ import de.be4.classicalb.core.parser.node.PPredicate;
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.internal.Activator;
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;
@@ -112,7 +116,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
if (rodinFile.exists()) {
ISCContextRoot root = (ISCContextRoot) rodinFile.getRoot();
collectProofInfo(root);
- collectPragmas(root);
}
} catch (Exception e) {
// We do not guarantee to include proof infos. If something goes
@@ -124,11 +127,23 @@ public final class ContextTranslator extends AbstractComponentTranslator {
Assert.isTrue(machine_root.getRodinFile().isConsistent());
}
translateContext();
-
+ collectPragmas();
}
- private void collectPragmas(ISCContextRoot origin) {
- // TODO
+ private void collectPragmas() throws RodinDBException {
+ // unit pragma, attached to constants
+ final IAttributeType.String UNITATTRIBUTE = RodinCore
+ .getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute");
+
+ final ISCConstant[] constants = context.getSCConstants();
+
+ for (final ISCConstant constant : constants) {
+ if (constant.hasAttribute(UNITATTRIBUTE)) {
+ pragmas.add(new UnitPragma(getResource(), constant
+ .getIdentifierString(), constant
+ .getAttributeValue(UNITATTRIBUTE)));
+ }
+ }
}
private void collectProofInfo(ISCContextRoot origin)
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 fd794bea..db29b3ae 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
@@ -35,13 +35,16 @@ import org.eventb.core.ISCVariable;
import org.eventb.core.ISCVariant;
import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement;
+import org.eventb.core.IVariable;
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;
@@ -66,8 +69,10 @@ import de.be4.classicalb.core.parser.node.PPredicate;
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.internal.Activator;
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;
@@ -176,8 +181,20 @@ public class ModelTranslator extends AbstractComponentTranslator {
collectPragmas();
}
- private void collectPragmas() {
- // TODO
+ private void collectPragmas() throws RodinDBException {
+ // unit pragma, attached to constants
+ final IAttributeType.String UNITATTRIBUTE = RodinCore
+ .getStringAttrType(Activator.PLUGIN_ID + ".unitPragmaAttribute");
+
+ final IVariable[] variables = origin.getVariables();
+
+ for (final IVariable variable : variables) {
+ if (variable.hasAttribute(UNITATTRIBUTE)) {
+ pragmas.add(new UnitPragma(getResource(), variable
+ .getIdentifierString(), variable
+ .getAttributeValue(UNITATTRIBUTE)));
+ }
+ }
}
private void collectProofInfo() throws RodinDBException {
diff --git a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
index 3b2ce2fe..4bbe282b 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/StartUnitAnalysisHandler.java
@@ -56,7 +56,7 @@ import de.prob.parser.ResultParserException;
import de.prob.prolog.term.CompoundPrologTerm;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
-import de.prob.ui.pragmas.InferredUnitPragma;
+import de.prob.ui.pragmas.InferredUnitPragmaAttribute;
public class StartUnitAnalysisHandler extends AbstractHandler implements
IHandler {
@@ -178,7 +178,8 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
for (IVariable var : allVariables) {
String variableName = var.getIdentifierString();
if (variables.containsKey(variableName)) {
- var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+ var.setAttributeValue(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
variables.get(variableName),
new NullProgressMonitor());
}
@@ -192,7 +193,8 @@ public class StartUnitAnalysisHandler extends AbstractHandler implements
for (IConstant var : allConstants) {
String constantName = var.getIdentifierString();
if (variables.containsKey(constantName)) {
- var.setAttributeValue(InferredUnitPragma.ATTRIBUTE,
+ var.setAttributeValue(
+ InferredUnitPragmaAttribute.ATTRIBUTE,
variables.get(constantName),
new NullProgressMonitor());
}
--
GitLab