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

[Brian Huffman]

Hi Florian,

One more thing: The indirect recursion causes SML/OCaml code  
generation to fail, but converting to the equivalent mutual-recursive  
definition makes it work again.

datatype 'a tree = Node 'a "'a tree list"
definition "test2 = (Node True [] = Node True [Node False []])"
export_code test2 in OCaml file -

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

datatype 'a tree = Node 'a "'a forest"
and 'a forest = Empty | Trees "'a tree" "'a forest"
definition "test2 = (Node True Empty = Node True (Trees (Node False  
Empty) Empty))"
export_code test2 in OCaml file -

The second version works just fine for OCaml or SML.

I would have expected both versions of the tree datatype to produce  
basically the same code for eq, since they both have essentially the  
same recursion combinator.

- Brian