[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing

[Florian Haftmann]

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,
	Florian


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:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170121/e1c18ccf/attachment.sig>