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

Reply via email to