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