Email Gateway (Aug 19 2022 at 15:44): Email Gateway (Aug 19 2022 at 15:44):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I encountered the following problem when using datatype_compat:
datatype_new 'a tree = Empty | Node 'a "'a tree list"
datatype_compat tree
datatype_new 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
datatype_compat ttree
exception TYPE raised (line 329 of "~~/src/HOL/Tools/hologic.ML"):
dest_prodT
(('a ttree × 'b) list tree × 'd) list
However, both datatypes are easily declared using the old datatype package:
datatype 'a tree = Empty | Node 'a "'a tree list"
datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
The problem occurs with both Isabelle2014-RC1 and -RC2.
The datatypes can be also be found in $AFP/thys/Datatype_Order_Generator/Derive_Examples.
Kind regards,
René
Email Gateway (Aug 19 2022 at 15:44):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi René,
Thanks for the report! Dmitriy and I have been looking more closely at the issue but we haven't been able yet to determine if it's his bug or mine. ;) Hopefully we'll be able to come back to you in the coming days with a fix. Regarding the Isabelle2014 release, I fear we won't be able to include a fix, since this isn't a regression and we must be very conservative in our changes so close to a release.
As usual, sorry for the trouble.
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 15:46):From: Dmitriy Traytel <traytel@in.tum.de>
Hi René,
It should be better now in Isabelle's repository version 9c065009cd8a.
The observed bug was mine, but your report triggered a cascade of
robustifications in both, mine and Jasmin's code. Thanks again!
Dmitriy
Last updated: Apr 26 2024 at 12:28 UTC