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