Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression



Hi Florian,

On 03/04/14 18:09, Florian Haftmann wrote:
Hi Andreas,

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.