[isabelle-dev] Bug report: code generation for eq with indirect-recursive datatypes
florian.haftmann at informatik.tu-muenchen.de
Mon Feb 23 21:37:13 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".
If you pull from the repository it shall be gone ;-). Thanks for
> 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.
I appreciate your attempt, but the major problem is not list_all2 (you
could likewise postpone the proof of the code theorem to List.thy); the
issue is the code_message type which *can* be moved before List.thy
using some duplication, but this is tedious since it also interferes
with the code serializer setup.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 252 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev