Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code equation for term_of_integer contains ill...


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC