Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [SPAM] Exception in code generator

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's 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

Last updated: May 03 2024 at 08:18 UTC