From 3d817e56882a12c052fc78ac79db1a7f8aca0995 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 25 Jan 2024 09:55:07 +0100
Subject: [PATCH] try fix export of inductive datatype definitions
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
README.md | 2 +-
.../src/de/prob/eventb/translator/Theories.java | 12 ++++++++++--
2 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 7ed60ece..f06073a3 100644
--- a/README.md
+++ b/README.md
@@ -5,7 +5,7 @@
## License
The ProB source code is distributed under the [EPL 1.0 license](https://www.eclipse.org/org/documents/epl-v10.html).
-(C) 2000-2021 Michael Leuschel and many others.
+(C) 2000-2024 Michael Leuschel and many others.
For updates please visit the ProB website: https://prob.hhu.de/w/
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 70238004..bd7653d6 100644
--- a/de.prob.core/src/de/prob/eventb/translator/Theories.java
+++ b/de.prob.core/src/de/prob/eventb/translator/Theories.java
@@ -430,8 +430,16 @@ public class Theories {
final IPrologTermOutput pto) throws CoreException {
pto.openTerm(functor);
pto.printAtom(id.getIdentifierString());
- Type type = id.getType(ff);
- printType(type, pto);
+ try {
+ Type type = id.getType(ff);
+ printType(type, pto);
+ } catch (CoreException e) {
+ // 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"
+ // as one cannot adapt the type parameters inside an inductive type definition
+ pto.printAtom("default_type_parameters")
+ }
pto.closeTerm();
}
--
GitLab