[isabelle] Code equation for term_of_integer contains illegal numeral expression

[Andreas Lochbihler]

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

[Florian Haftmann]

Hi Andreas,

Post by Andreas Lochbihler
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?

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

[Andreas Lochbihler]

Hi Florian,

Post by Florian Haftmann
Hi Andreas,

Post by Andreas Lochbihler
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?

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.

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