*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 4 Apr 2014 13:28:47 +0200*In-reply-to*: <533D87BC.4090907@informatik.tu-muenchen.de>*References*: <53344B5D.3030801@inf.ethz.ch> <533D87BC.4090907@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.4.0

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

**References**:**Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression***From:*Florian Haftmann

- Previous by Date: [isabelle] Inductive Approach for Security Protocol Analysis
- Next by Date: Re: [isabelle] I need an ML function to get the THY path and filename
- Previous by Thread: Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression
- Next by Thread: [isabelle] Inductive Approach for Security Protocol Analysis
- Cl-isabelle-users April 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list