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

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: default avatarMichael Leuschel <leuschel@uni-duesseldorf.de>
parent a6ed00a4
No related branches found
No related tags found
No related merge requests found
...@@ -435,21 +435,19 @@ public class Theories { ...@@ -435,21 +435,19 @@ 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());
//final String typeString = getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE); final String typeString = id.getAttributeValue(EventBAttributes.TYPE_ATTRIBUTE);
// todo: is there a better way to check if type refers recursively to def? // todo: is there a better way to check if type refers recursively to def? do we need to trim typeString?
//if (def.getIdentifierString().equals(typeString)) { // System.out.println("Inductive datatype: " + def.getIdentifierString() + " destructor arg has type: " + typeString);
// the the checked theory files tcf no longer contain the type paras 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 tuf file may contain org.eventb.theory.core.type="Baum(L)"
// the tcf file now contains org.eventb.theory.core.type="Baum" // the tcf file now contains org.eventb.theory.core.type="Baum"
// getType would lead to a CoreException // getType would lead to a CoreException
// we print the type of the recursive data type directly // we print the type of the recursive data type directly
// pto.printTypeOfDataType(def,ff,pto); printTypeOfDataType(def,ff,pto);
//} else { } else {
try {
Type type = id.getType(ff); Type type = id.getType(ff);
printType(type, pto); printType(type, pto);
} catch (CoreException e) {
printTypeOfDataType(def,ff,pto);
} }
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