From 61022245df24dfaf9add5230dd831ae698db7de5 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 14 Feb 2024 14:19:10 +0100
Subject: [PATCH] export comments of axioms and theorems
as descriptions
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../eventb/translator/ContextTranslator.java | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 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 8fa94a5d..9265e4ef 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -15,6 +15,8 @@ import java.util.Map;
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.IContextRoot;
import org.eventb.core.IEventBRoot;
import org.eventb.core.IExtendsContext;
@@ -45,6 +47,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.ADescriptionPredicate;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
import de.be4.classicalb.core.parser.node.AExtendsContextClause;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
@@ -56,6 +59,7 @@ import de.be4.classicalb.core.parser.node.PExpression;
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.be4.classicalb.core.parser.node.TPragmaFreeText;
import de.hhu.stups.sablecc.patch.SourcePosition;
import de.prob.core.translator.TranslationFailedException;
import de.prob.eventb.translator.internal.EProofStatus;
@@ -373,8 +377,18 @@ public final class ContextTranslator extends AbstractComponentTranslator {
for (final ISCAxiom element : predicates) {
if (element.isTheorem() == theorems) {
final PPredicate predicate = translatePredicate(ff, te, element);
- list.add(predicate);
- labelMapping.put(predicate, element);
+ final IAxiom uca = (IAxiom) element.getSource(); // comments only attached in unchecked source
+ if (uca.hasAttribute(EventBAttributes.COMMENT_ATTRIBUTE)) {
+ final String commentString = uca.getAttributeValue(EventBAttributes.COMMENT_ATTRIBUTE);
+ //System.out.println("Axiom/theorem " + element + " has description " + commentString);
+ final TPragmaFreeText desc = new TPragmaFreeText(commentString);
+ final ADescriptionPredicate dpred = new ADescriptionPredicate(desc,predicate);
+ list.add(dpred);
+ labelMapping.put(dpred, element);
+ } else {
+ list.add(predicate);
+ labelMapping.put(predicate, element);
+ }
// proofspragmas.add(new ClassifiedPragma("discharged",
// predicate,
// Arrays.asList(new String[0]), Arrays
--
GitLab