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

[Florian Haftmann]

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.

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

	Florian

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090223/52f403ab/attachment.sig>