Skip to content
Snippets Groups Projects
Commit 3d817e56 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

try fix export of inductive datatype definitions

parent b501d2a8
No related branches found
No related tags found
No related merge requests found
Pipeline #129057 failed
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
## License ## License
The ProB source code is distributed under the [EPL 1.0 license](https://www.eclipse.org/org/documents/epl-v10.html). 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/ For updates please visit the ProB website: https://prob.hhu.de/w/
......
...@@ -430,8 +430,16 @@ public class Theories { ...@@ -430,8 +430,16 @@ public class Theories {
final IPrologTermOutput pto) throws CoreException { final IPrologTermOutput pto) throws CoreException {
pto.openTerm(functor); pto.openTerm(functor);
pto.printAtom(id.getIdentifierString()); pto.printAtom(id.getIdentifierString());
try {
Type type = id.getType(ff); Type type = id.getType(ff);
printType(type, pto); 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(); pto.closeTerm();
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment