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
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev