From aa10dac7fdd63fe49c94a9bfc46259ae2add4518 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 25 Jan 2024 19:16:07 +0100
Subject: [PATCH] detect recursive type reference without try-catch
in .eventb export of inductive datatypes
we compare the string of the type of the sub-argument
against the current datatype, if it is equal we generate
a recursive reference without parsing (which will usually,
but *not* always raise a CoreException as type paras are missing)
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
.../src/de/prob/eventb/translator/Theories.java | 16 +++++++---------
1 file changed, 7 insertions(+), 9 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 bb7e443c..6a1629c6 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -435,21 +435,19 @@ public class Theories {
final IPrologTermOutput pto) throws CoreException {
pto.openTerm(functor);
pto.printAtom(id.getIdentifierString());
- //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)) {
- // the the checked theory files tcf no longer contain the type paras
+ final String typeString = id.getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
+ // todo: is there a better way to check if type refers recursively to def? do we need to trim typeString?
+ // System.out.println("Inductive datatype: " + def.getIdentifierString() + " destructor arg has type: " + typeString);
+ if (def.getIdentifierString().equals(typeString)) {
+ // 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 {
- try {
+ printTypeOfDataType(def,ff,pto);
+ } else {
Type type = id.getType(ff);
printType(type, pto);
- } catch (CoreException e) {
- printTypeOfDataType(def,ff,pto);
}
pto.closeTerm();
}
--
GitLab