Hi Lukas,

thanks for the offer.  We have still time before the next release to
work that out.  Just give me a sign when you start to dig into this.

All the best,

Am 21.01.2017 um 18:33 schrieb Lukas Bulwahn:
> Hi Florian,
> I have been quite busy the last few days and hence did find the time
> to answer you email quickly.
>> This however breaks Quickcheck/Narrowing where the lazy nature of
>> pattern bindings has been exploited, may be unconsciously. A minimal
>> example is attached (Quickcheck_Narrowing_Examples.thy) but I also
>> distilled the generated Haskell code:
> Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
> a evaluation engine that implements narrowing without actually
> transforming the program that is evaluated.
> The real ideas how to implement narrowing in Haskell come from the
> original authors of LazySmallCheck; the main contribution to make this
> possible in Isabelle is largely the engineering question how to
> combine the ideas from LazySmallCheck with the Isabelle code
> generator. As I was investigating this, I did some further extensions
> to allow existential quantifiers, but this is technically not that
> difficult to implement.
> There is a bit of documentation describing the implementation in my thesis.
> At the moment, I am a little bit busy, but hopefully mid of February,
> I could assist looking into this.
> Maintaining Quickcheck Narrowing has not been a major tasks in the
> last years there was no need to change anything as tricky as the point
> that we encounter now. Hence, I would expect that maintenance will
> continue to be low, once we resolved this issue.
> Lukas


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to