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

2017-04-14 Thread Florian Haftmann
For the record: Lukas and me have resolved that issue in 721feefce9c6. Cheers, Florian Am 14.01.2017 um 09:33 schrieb Florian Haftmann: > Hi Lukas, > > I am currently stuck with a problem in Quickcheck/Narrowing. > > After about 10 years it came to surface that code generation for

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

2017-01-25 Thread 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

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

2017-01-23 Thread Florian Haftmann
Hi Andreas, that should be fine. I am optimistic that we will manage somehow to work that our during February. Cheers, Florian Am 23.01.2017 um 09:39 schrieb Andreas Lochbihler: > Hi Florian, > > On 21/01/17 16:56, Florian Haftmann wrote: >> unfortunately, a selector-based solution

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

2017-01-21 Thread 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

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

2017-01-21 Thread Florian Haftmann
Hi Andreas, unfortunately, a selector-based solution didn't either yield a terminating example. If you like you can inspect the attached code, maybe I did get something wrong. I will resonsider this in approx. one week; maybe we have to raise the question seriously how maintenance of

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

2017-01-14 Thread Florian Haftmann
Hi Andreas, thanks for that quick reply. This could be done in any case, sure. Cheers, Florian Am 14.01.2017 um 10:03 schrieb Andreas Lochbihler: > Hi Florian, > > Lukas may be able to answer this question better, but here's a comment: > You do not need the lazy treatment of

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

2017-01-14 Thread Andreas Lochbihler
Hi Florian, Lukas may be able to answer this question better, but here's a comment: You do not need the lazy treatment of irrefutable patterns in Haskell as a primitive, because it is easy to emulate using selectors. That is, if we have a single-constructor HOL datatype dataype 'a T = C (s1: