Hi Florian, On 21/01/17 16:56, Florian Haftmann wrote:

unfortunately, a selector-based solution didn't either yield a terminating example.## Advertising

If you like you can inspect the attached code, maybe I did get something wrong.

`I am afraid, I am busy with other stuff and won't have the time to dig into the details. I`

`hope that Lukas will be able to find out what is going wrong.`

Andreas

I will resonsider this in approx. one week; maybe we have to raise the question seriously how maintenance of quickcheck/narrowing can go on. 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 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: 'a) (s2: 'a T) (s3: 'a T list) then we can introduce a copy of the case operator by definition case_lazy_T where "case_lazy_T = case_T" lemma [code]: "case_lazy_T f x = f (s1 x) (s2 x) (s3 x)" Now, when you want to use the semantics of irrefutable patterns in let-bindings, use case_lazy_T in the code equation. If you really want to force the evaluation, then use case_T and compile it with the new scheme. I have not tried this, but my guess is that if you do it this way for the three types narrowing_type narrowing_term narrowing_cons of Quickcheck_Narrowing and adjust the code equations for the constants in Quickcheck_Narrowing accordingly, then you get back the old behaviour. Hope this helps, Andreas On 14/01/17 09:33, Florian Haftmann wrote:Hi Lukas, I am currently stuck with a problem in Quickcheck/Narrowing. After about 10 years it came to surface that code generation for Haskell may produce irrefutable patterns due to pattern bindings in let clauses. See <https://wiki.haskell.org/Lazy_pattern_match>; if I understand <https://www.haskell.org/tutorial/patterns.html> correctly that particular semantics allows fancy definitions like the following fibonacci one-liner: »fib @ (1 : more_fib) = 1 : 1 : [ a + b | (a, b) <- zip fib more_fib ]«. However the partial correctness approach of the code generator assumes that pattern match clauses may silently be dropped, which is made use of to translate the HOL-ish »partial« undefined conveniently. This breaks down in presence of irrefutable patterns (see the post on isabelle-users by Rene Thiemann). The correction is obvious: for Haskell, only local variables may be bound by let clauses, but never patterns – these are solely bound by case clauses, which are strict in Haskell (as in function equations). 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: The same before and after: Typerep.hs Then the difference occurs: Generated_Code.hs Before: Generated_Code.A.hs After: Generated_Code.B.hs The same before and after: Narrowing_Engine.hs Main.hs The diff ist straight-forward to read:93,102c93,106 < let { < (Narrowing_cons (Narrowing_sum_of_products ps) cfs) = f d; < (Narrowing_cons ta cas) = a (d - (1 :: Prelude.Int)); < shallow = (0 :: Prelude.Int) < d && non_empty ta; < aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs < else []); < } in Narrowing_cons < (Narrowing_sum_of_products < (if shallow then map (\ ab -> ta : ab) ps else [])) < aa; --- > (case f d of { > Narrowing_cons (Narrowing_sum_of_products ps) cfs -> > (case a (d - (1 :: Prelude.Int)) of { > Narrowing_cons ta cas -> > let { > shallow = (0 :: Prelude.Int) < d && non_empty ta; > aa = (if shallow then map (\ cf (x : xs) -> cf xs (conv cas x)) cfs > else []); > } in Narrowing_cons > (Narrowing_sum_of_products > (if shallow then map (\ ab -> ta : ab) ps else [])) > aa; > }); > }); 112,115c116,122 < let { < (Narrowing_cons (Narrowing_sum_of_products ssa) ca) = a d; < (Narrowing_cons (Narrowing_sum_of_products ssb) cb) = b d; < } in Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb); --- > (case a d of { > Narrowing_cons (Narrowing_sum_of_products ssa) ca -> > (case b d of { > Narrowing_cons (Narrowing_sum_of_products ssb) cb -> > Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb); > }); > });Unfortunately my knowledge is too restricted what could be done here to restore the intended behaviour economically. Hence I ask whether you have an idea what is going wrong here. Thanks a lot! Florian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev