Email Gateway (Aug 22 2022 at 17:41): Email Gateway (Aug 22 2022 at 17:41):From: Lars Hupel <hupel@in.tum.de>
I figured it out. The problem is that there's a data constructor called
"Match". But Quickcheck catches "Match", the ML exception:
axiomatization catch_match :: "'a => 'a => 'a"
code_printing
constant catch_match ⇀ (Quickcheck) "((_) handle Match => _)"
I propose adding the following line to "Quickcheck_Random.thy":
code_reserved Quickcheck Match
Email Gateway (Aug 22 2022 at 17:43):From: Lars Hupel <hupel@in.tum.de>
This line does not break anything in the AFP and solves the immediate
problem. Is there any opposition to committing this change?
Email Gateway (Aug 22 2022 at 17:44):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Your change makes sense; I either overlooked that someone could come
up with an own constant Match, or evolution of the code generator and
changes to that part of theory somehow introduced this shortcoming.
Lukas
Email Gateway (Aug 22 2022 at 17:45):From: Lars Hupel <hupel@in.tum.de>
See now Isabelle/1148f63304f4.
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:53):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I discovered an internal ML error when using QuickCheck. The attached
theory file, which I attempted to strip down to the bare minimum,
exposes the problem. A "quickcheck" call appears to produce ML code that
doesn't type check.
This problem affects Isabelle2017 and 2018-RC1.
(The theory has been developed by a student.)
Cheers
Lars
Scratch.thy
Last updated: Apr 26 2024 at 04:17 UTC