From 9c2d26941d7aebdf7eaff6afcb51ec51c2fe3364 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Tue, 12 Sep 2023 13:12:58 +0200
Subject: [PATCH] add comments about WD export of theory operators
cf issue #325
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
de.prob.core/src/de/prob/eventb/translator/Theories.java | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/Theories.java b/de.prob.core/src/de/prob/eventb/translator/Theories.java
index 453e0c83..6df44f11 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -322,7 +322,7 @@ public class Theories {
throws CoreException {
prologOutput.openTerm("operator");
- prologOutput.printAtom(opDef.getLabel());
+ prologOutput.printAtom(opDef.getLabel()); // Name of the operator
final FormulaFactory ff = theory.getFormulaFactory();
final ITypeEnvironment teFromFF = theory.getTypeEnvironment(ff);
@@ -337,6 +337,9 @@ public class Theories {
}
// WD Condition
+ // TODO: does not seem to get the user-defined WD conditions
+ // we should probably call in INewOperatorDefinition.java : IOperatorWDCondition[] getOperatorWDConditions() throws RodinDBException;
+ // and convert this to a Predicate
Predicate wdCondition = opDef.getWDCondition(ff, te);
printPredicate(prologOutput, wdCondition);
--
GitLab