[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes

[Brian Huffman]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> Hi Brian,
>
>> The following code works:
>>
>> datatype 'a bintree = Branch "'a bintree" "'a bintree" | Tip 'a
>> definition "test1 = (Tip True = Branch (Tip False) (Tip True))"
>> export_code test1 in Haskell file -
>>
>> but this other example doesn't:
>>
>> datatype 'a tree = Node 'a "'a tree list"
>> definition "test2 = (Node True [] = Node True [Node False []])"
>> export_code test2 in Haskell file -
>>
>> Instead it fails with:
>>
>> *** exception UNDEF raised
>> *** At command "export_code".
>
> If you pull from the repository it shall be gone ;-).  Thanks for
> reporting this.

Hi Florian,

Thanks for the quick response! The Haskell code generation works now  
for both examples.

However, if I try to generate OCaml or SML code, the second one still  
fails, but with a different error this time:

*** Illegal mutual dependencies: "tree :: eq", "eq_class.eq [tree]"
*** At command "export_code".

What do you think?

- Brian