Email Gateway (Aug 19 2022 at 13:53): Email Gateway (Aug 19 2022 at 13:53):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts on code generation,
The term reconstruction setup for the integer type seems to be broken in Isabelle2013-2
and the development version (tested with 801a72ad52d3). This makes quickcheck-narrowing
raise an exception as soon as the query contains a function variable whose domain is
related to the target-language numerals. If I import ~~/src/HOL/Library/Code_Target_Int,
functions with domain int are also affected.
Here's a minimal example:
theory Scratch imports "~~/src/HOL/Library/Code_Target_Int" begin
lemma "f = (g :: int => bool)"
quickcheck[narrowing]
*** Illegal numeral expression: illegal term,
*** in equation Code_Evaluation.term_of_integer_inst.term_of_integer (Code_Numeral.Neg ?a)
== ...
I am not particularly familiar with all this term reconstruction stuff, but I found the
following. In Code_Evaluation, there's a custom serialisation of term_of for integer for
the target Eval. Narrowing, however, uses the target Haskell_Quickcheck, which is not a
sub-target of Eval. Is there just an adaptation missing?
Best,
Andreas
Email Gateway (Aug 19 2022 at 14:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
I interpret this as that the regular evaluation using »value [code] …«
etc. is operative but Quickcheck Narrowing breaks. I follow your
analysis that a corresponding adaption for integer is missing for
Haskell_Quickcheck. Never did I attempt to understand fully the rather
fancy and specialist adaption setup for Haskell_Quickcheck, but I guess
you easily find out what to add by experimenting with a setup for
term_of similar to that of Eval.
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 14:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
The setup for Haskell_Quickcheck is indeed fragile and should be improved.
In 3b2db6132bfd, I've added the serialisation for term_of that makes all my examples work.
It is just as ugly as the whole serialisation setup.
Andreas
Last updated: Nov 21 2024 at 12:39 UTC