From 614ff6a997ddc3ea96229c58d543b839918944b4 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 25 Jan 2024 11:59:49 +0100
Subject: [PATCH] revert to try-catch for detecting recursive types
in datatype destructors
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../src/de/prob/eventb/translator/Theories.java | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
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 dfbf5bc3..170cb9cb 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -435,18 +435,21 @@ public class Theories {
final IPrologTermOutput pto) throws CoreException {
pto.openTerm(functor);
pto.printAtom(id.getIdentifierString());
- final String typeString = getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
+ //final String typeString = getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
// todo: is there a better way to check if type refers recursively to def?
- if (def.getIdentifierString().equals(typeString)) {
+ //if (def.getIdentifierString().equals(typeString)) {
// the the checked theory files tcf no longer contain the type paras
// the tuf file may contain org.eventb.theory.core.type="Baum(L)"
// the tcf file now contains org.eventb.theory.core.type="Baum"
// getType would lead to a CoreException
// we print the type of the recursive data type directly
- pto.printTypeOfDataType(def,ff,pto);
- } else {
+ // pto.printTypeOfDataType(def,ff,pto);
+ //} else {
+ try {
Type type = id.getType(ff);
printType(type, pto);
+ } catch (CoreException e) {
+ printTypeOfDataType(def,ff,pto);
}
pto.closeTerm();
}
--
GitLab