[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes
brianh at cs.pdx.edu
Mon Feb 23 22:00:32 CET 2009
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.
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?
More information about the isabelle-dev