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 didn't either yield a >> terminating example. >> >> 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 -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev