From b501d2a8e22a16884f8a3c349376c284d521156a Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 24 Jan 2024 16:31:02 +0100
Subject: [PATCH] add todos
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
de.prob.core/src/de/prob/eventb/translator/Theories.java | 2 ++
1 file changed, 2 insertions(+)
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 fef28e07..70238004 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -416,6 +416,7 @@ public class Theories {
Predicate pp = (Predicate) scFormula;
printPredicate(prologOutput, pp);
}
+ // TODO: we could insert the result type in the Prolog term; or at least if we have a pred or expr
if (scFormula instanceof Expression) {
Expression pp = (Expression) scFormula;
printExpression(prologOutput, pp);
@@ -488,6 +489,7 @@ public class Theories {
pto.openList();
// WD condition missing
pto.closeList();
+ // Result type is not written; we can maybe get it from: Formula<?> scFormula = def.getSCFormula(ff, te);
pto.closeTerm();
}
pto.closeList();
--
GitLab