Re: [isabelle] Exception in code generator
Ok, thanks Stefan. Then I'll wait to try out autoquickcheck once it's
ported to Florian's framework.
On May 13, 2008, at 10:14 AM, Stefan Berghofer wrote:
John Matthews wrote:
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:
*** required by:
*** czero_quickcheck.czero_ty_class.czero def1, <Top>
*** At command "quickcheck".
I think the problem is in czero_fun_def, [...]
this kind of overloading is not supported by the old code generator,
therefore not supported by quickcheck either. The old code generator
supports those cases of overloading that can be resolved while
code. Unfortunately, this is not the case for czero_fun_def, since the
right-hand side of the definition again contains a polymorphic
czero, and the code generator cannot figure out which definition it
use in this case.
The new code generator by Florian Haftmann supports code generation
definitions like czero_fun_def as well (using a dictionary
but we are not yet completely finished with porting quickcheck to
Dr. Stefan Berghofer E-Mail: berghofe at in.tum.de
Institut fuer Informatik Phone: +49 89 289 17328
Technische Universitaet Muenchen Fax: +49 89 289 17307
Boltzmannstr. 3 Room: 01.11.059
85748 Garching, GERMANY http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and