From 68f3cb260f88b6b9334d6f9cf64d5e0ab703633a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 14 Nov 2024 09:18:01 +0100
Subject: [PATCH] add comments for constants as description pragmas
in .eventb export
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../eventb/translator/ContextTranslator.java | 31 +++++++++++++++----
1 file changed, 25 insertions(+), 6 deletions(-)
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 67849c1f..28f9a9cd 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -28,6 +28,7 @@ import org.eventb.core.IPSRoot;
import org.eventb.core.IPSStatus;
import org.eventb.core.ISCAxiom;
import org.eventb.core.ISCCarrierSet;
+import org.eventb.core.IConstant;
import org.eventb.core.ISCConstant;
import org.eventb.core.ISCContext;
import org.eventb.core.ISCContextRoot;
@@ -48,6 +49,7 @@ import de.be4.classicalb.core.parser.node.AAbstractConstantsContextClause;
import de.be4.classicalb.core.parser.node.AAxiomsContextClause;
import de.be4.classicalb.core.parser.node.AConstantsContextClause;
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.AEventBContextParseUnit;
@@ -340,13 +342,30 @@ public final class ContextTranslator extends AbstractComponentTranslator {
} catch (IllegalArgumentException E) {
// the attribute did not exist
}
-
- if (isAbstractConstant) {
- abstractConstants.add(new AIdentifierExpression(Arrays
- .asList(new TIdentifierLiteral[] { new TIdentifierLiteral(constant.getIdentifierString()) })));
+ // TODO: check unchecked constant and see if we have a comment and generate ADescriptionExpression
+
+ final AIdentifierExpression cstid = new AIdentifierExpression(Arrays
+ .asList(new TIdentifierLiteral[] { new TIdentifierLiteral(constant.getIdentifierString()) }));
+
+ final IConstant ucc = (IConstant) constant.getSource(); // comments only attached in unchecked source
+ if (ucc.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ final String commentString = ucc.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
+ // System.out.println("Constant " + constant + " has description " + commentString);
+
+ final TPragmaFreeText desc = new TPragmaFreeText(commentString);
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ final ADescriptionExpression descid = new ADescriptionExpression(descPragma,cstid);
+ if (isAbstractConstant) {
+ abstractConstants.add(descid);
+ } else {
+ concreteConstants.add(descid);
+ }
} else {
- concreteConstants.add(new AIdentifierExpression(Arrays
- .asList(new TIdentifierLiteral[] { new TIdentifierLiteral(constant.getIdentifierString()) })));
+ if (isAbstractConstant) {
+ abstractConstants.add(cstid);
+ } else {
+ concreteConstants.add(cstid);
+ }
}
}
--
GitLab