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

[Brian Huffman]

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".

I figured that someone must have known about this already; what tipped  
me off to the existence of this bug was the custom [code] rule for  
eq_class.eq given in the Typerep theory. (The log file says something  
about dropping the previously-installed code equations.) I'm just  
wondering if there is a solution in the works.

Honestly, the primary reason I'm interested is that I'd like to see  
Typerep.thy moved into Plain, and currently the eq_class.eq [code]  
rule adds a dependency on the list_all2 function, which I'd like to  
get rid of.

- Brian