From fa5196774a43913fe79e1befe3f93bcdc90de4ab Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 20 Nov 2024 10:16:16 +0100
Subject: [PATCH] export carrier set comments as desription pragmas
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../eventb/translator/ContextTranslator.java | 17 ++++++++++++++++-
1 file changed, 16 insertions(+), 1 deletion(-)
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 af6fd02f..0174b35d 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -18,6 +18,7 @@ import org.eclipse.core.runtime.Assert;
import org.eclipse.core.runtime.CoreException;
import org.eventb.core.EventBAttributes;
import org.eventb.core.IAxiom;
+import org.eventb.core.ICarrierSet;
import org.eventb.core.IContextRoot;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IExtendsContext;
@@ -52,6 +53,7 @@ import de.be4.classicalb.core.parser.node.ADeferredSetSet;
import de.be4.classicalb.core.parser.node.ADescriptionExpression;
import de.be4.classicalb.core.parser.node.ADescriptionPragma;
import de.be4.classicalb.core.parser.node.ADescriptionPredicate;
+import de.be4.classicalb.core.parser.node.ADescriptionSet;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
import de.be4.classicalb.core.parser.node.AExtendsContextClause;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -314,9 +316,22 @@ public final class ContextTranslator extends AbstractComponentTranslator {
final ISCCarrierSet[] carrierSets = context.getSCCarrierSets();
final List<PSet> setList = new ArrayList<PSet>(carrierSets.length);
for (final ISCCarrierSet carrierSet : carrierSets) {
+
final ADeferredSetSet deferredSet = new ADeferredSetSet(Arrays
.asList(new TIdentifierLiteral[] { new TIdentifierLiteral(carrierSet.getIdentifierString()) }));
- setList.add(deferredSet);
+
+ final ICarrierSet ucs = (ICarrierSet) carrierSet.getSource(); // comments only attached in unchecked source
+ if (ucs.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ final String commentString = ucs.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
+ System.out.println("Carrier set " + carrierSet + " has comment " + commentString);
+
+ final TPragmaFreeText desc = new TPragmaFreeText(commentString);
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ final ADescriptionSet descid = new ADescriptionSet(descPragma,deferredSet);
+ setList.add(descid);
+ } else {
+ setList.add(deferredSet);
+ }
}
return new ASetsContextClause(setList);
}
--
GitLab