Email Gateway (Aug 18 2022 at 11:52): Email Gateway (Aug 18 2022 at 11:52):From: John Matthews <matthews@galois.com>
Hello,
I'm now trying to define an overloaded Cryptol constant that is
supposed to return zero on all types, but quickcheck's code generator
seems to be failing on one of the overloaded definitions. Here is a
stripped-down example:
class czero_ty = type +
fixes czero :: "'a"
instance bool :: czero_ty
czero_bool_def: "czero == False"
..
instance "fun" :: (type,czero_ty)czero_ty
czero_fun_def: "czero n == czero"
..
When I try to test "(czero :: int => bool) n = False" with quickcheck,
I get the following error:
*** Unable to generate code for term:
*** czero
*** required by:
*** czero_quickcheck.czero_ty_class.czero def1, <Top>
*** At command "quickcheck".
I think the problem is in czero_fun_def, because if I try to execute
this:
declare czero_fun_def[code]
then Isabelle returns this exception:
*** exception TERM raised: dest_Trueprop
*** At command "declare".
I'm using Isabelle2007.
Thanks,
-john
Email Gateway (Aug 18 2022 at 11:52):From: Stefan Berghofer <berghofe@in.tum.de>
John Matthews wrote:
Hello John,
this kind of overloading is not supported by the old code generator, and
therefore not supported by quickcheck either. The old code generator only
supports those cases of overloading that can be resolved while generating
code. Unfortunately, this is not the case for czero_fun_def, since the
right-hand side of the definition again contains a polymorphic constant
czero, and the code generator cannot figure out which definition it should
use in this case.
The new code generator by Florian Haftmann supports code generation from
definitions like czero_fun_def as well (using a dictionary construction),
but we are not yet completely finished with porting quickcheck to the new
code generator.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 11:52):From: John Matthews <matthews@galois.com>
Ok, thanks Stefan. Then I'll wait to try out autoquickcheck once it's
ported to Florian's framework.
Best,
-john
Last updated: May 03 2024 at 08:18 UTC