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

[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 Haskell
> may produce irrefutable patterns due to pattern bindings in let clauses.
> See ; if I understand
>  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
>>  >  <   } 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
> 

-- 

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

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

[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 (Quickcheck_Narrowing_Examples.thy) but I also
> distilled the generated Haskell code:

Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
a evaluation engine that implements narrowing without actually
transforming the program that is evaluated.

The real ideas how to implement narrowing in Haskell come from the
original authors of LazySmallCheck; the main contribution to make this
possible in Isabelle is largely the engineering question how to
combine the ideas from LazySmallCheck with the Isabelle code
generator. As I was investigating this, I did some further extensions
to allow existential quantifiers, but this is technically not that
difficult to implement.

There is a bit of documentation describing the implementation in my thesis.
At the moment, I am a little bit busy, but hopefully mid of February,
I could assist looking into this.

Maintaining Quickcheck Narrowing has not been a major tasks in the
last years there was no need to change anything as tricky as the point
that we encounter now. Hence, I would expect that maintenance will
continue to be low, once we resolved this issue.

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

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

[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 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 ; if I understand
  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
>  <   } 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;
> >  

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

[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 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 (Quickcheck_Narrowing_Examples.thy) but I also
>> distilled the generated Haskell code:
> 
> Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have
> a evaluation engine that implements narrowing without actually
> transforming the program that is evaluated.
> 
> The real ideas how to implement narrowing in Haskell come from the
> original authors of LazySmallCheck; the main contribution to make this
> possible in Isabelle is largely the engineering question how to
> combine the ideas from LazySmallCheck with the Isabelle code
> generator. As I was investigating this, I did some further extensions
> to allow existential quantifiers, but this is technically not that
> difficult to implement.
> 
> There is a bit of documentation describing the implementation in my thesis.
> At the moment, I am a little bit busy, but hopefully mid of February,
> I could assist looking into this.
> 
> Maintaining Quickcheck Narrowing has not been a major tasks in the
> last years there was no need to change anything as tricky as the point
> that we encounter now. Hence, I would expect that maintenance will
> continue to be low, once we resolved this issue.
> 
> Lukas
> 

-- 

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

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

[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 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 ; if I understand
>>  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
>>> >> <   } 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 

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

[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 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 ; if I understand
>>  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
>>> >> <   } 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
>>
>>
>>
>> 

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

[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 ; if I understand
 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
 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