From ea1e6dd69b4348905b2c31be96aeb02915be8386 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Fri, 14 Feb 2025 14:07:53 +0100
Subject: [PATCH] extract comments for witnesses as desc pragmas
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../translator/internal/ModelTranslator.java | 15 +++++++++++++--
1 file changed, 13 insertions(+), 2 deletions(-)
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 bf8135a6..5924907f 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
@@ -40,6 +40,7 @@ import org.eventb.core.ISCWitness;
import org.eventb.core.ITraceableElement;
import org.eventb.core.IVariable;
import org.eventb.core.IVariant;
+import org.eventb.core.IWitness;
import org.eventb.core.ast.Assignment;
import org.eventb.core.ast.FormulaFactory;
import org.eventb.core.ast.ITypeEnvironment;
@@ -503,8 +504,18 @@ public class ModelTranslator extends AbstractComponentTranslator {
witness);
final TIdentifierLiteral label = new TIdentifierLiteral(
witness.getLabel());
- witnessList.add(new AWitness(label, predicate));
- labelMapping.put(predicate, witness);
+ final IWitness ucw = (IWitness) witness.getSource(); // comments only attached in unchecked
+ if (ucw.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ final String commentString = ucw.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
+ final TPragmaFreeText desc = new TPragmaFreeText(commentString);
+ ADescriptionPragma descPragma = new ADescriptionPragma(Collections.singletonList(desc));
+ ADescriptionPredicate dpred = new ADescriptionPredicate(descPragma, predicate);
+ witnessList.add(new AWitness(label, dpred));
+ labelMapping.put(dpred, witness);
+ } else {
+ witnessList.add(new AWitness(label, predicate));
+ labelMapping.put(predicate, witness);
+ }
}
return witnessList;
}
--
GitLab