[isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Sat Jan 21 16:56:02 CET 2017
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 <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-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Generated_Code.A.hs
Type: text/x-haskell
Size: 6377 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170121/9001c21d/attachment-0004.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Generated_Code.B.hs
Type: text/x-haskell
Size: 6574 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170121/9001c21d/attachment-0005.hs>
-------------- next part --------------
# HG changeset patch
# Parent a5a09855e4246bfd3d8ccd5b1d80f01479130d75
use explicit selectors in generated haskell code to not rely on accidental lazy pattern matching in generated let clauses;
modernized
diff -r a5a09855e424 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy Fri Jan 20 21:05:11 2017 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Sat Jan 21 16:48:58 2017 +0100
@@ -50,18 +50,24 @@
datatype (plugins only: code extraction) (dead 'a) narrowing_cons =
Narrowing_cons narrowing_type "(narrowing_term list \<Rightarrow> 'a) list"
-primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
-where
- "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (\<lambda>c. f o c) cs)"
+definition apply_cons :: "(narrowing_type list list \<Rightarrow> (narrowing_term list \<Rightarrow> 'a) list \<Rightarrow> 'b) \<Rightarrow> 'a narrowing_cons \<Rightarrow> 'b"
+ where "apply_cons f t =
+ (case t of Narrowing_cons (Narrowing_sum_of_products tyss) cs \<Rightarrow> f tyss cs)"
+
+lemma apply_cons [simp, code]:
+ "apply_cons f (Narrowing_cons (Narrowing_sum_of_products tyss) cs) = f tyss cs"
+ by (simp add: apply_cons_def)
+
subsubsection \<open>From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms\<close>
class partial_term_of = typerep +
- fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
+ fixes partial_term_of :: "'a itself \<Rightarrow> narrowing_term \<Rightarrow> Code_Evaluation.term"
lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
+
subsubsection \<open>Auxilary functions for Narrowing\<close>
consts nth :: "'a list => integer => 'a"
@@ -80,48 +86,39 @@
code_printing constant marker \<rightharpoonup> (Haskell_Quickcheck) "''\\0'"
+
subsubsection \<open>Narrowing's basic operations\<close>
-type_synonym 'a narrowing = "integer => 'a narrowing_cons"
+type_synonym 'a narrowing = "integer \<Rightarrow> 'a narrowing_cons"
definition empty :: "'a narrowing"
-where
- "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
+ where "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
-definition cons :: "'a => 'a narrowing"
-where
- "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
+definition cons :: "'a \<Rightarrow> 'a narrowing"
+ where "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(\<lambda>_. a)])"
-fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
-where
- "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
-| "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
+primrec conv :: "(narrowing_term list \<Rightarrow> 'a) list \<Rightarrow> narrowing_term \<Rightarrow> 'a"
+ where "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
+ | "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
-fun non_empty :: "narrowing_type => bool"
-where
- "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
+definition "apply" :: "('a \<Rightarrow> 'b) narrowing \<Rightarrow> 'a narrowing \<Rightarrow> 'b narrowing"
+ where "apply f a d = apply_cons (\<lambda>ps cfs.
+ apply_cons (\<lambda>ps' cas.
+ (let
+ shallow = d > 0 \<and> ps' \<noteq> [];
+ cs = [(\<lambda>xs'. (case xs' of x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
+ in Narrowing_cons (Narrowing_sum_of_products [Narrowing_sum_of_products ps' # p. shallow, p <- ps]) cs))
+ (a (d - 1))) (f d)"
-definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
-where
- "apply f a d =
- (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
- case a (d - 1) of Narrowing_cons ta cas =>
- let
- shallow = (d > 0 \<and> non_empty ta);
- cs = [(\<lambda>xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
- in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
-
-definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
-where
- "sum a b d =
- (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))"
+definition sum :: "'a narrowing \<Rightarrow> 'a narrowing \<Rightarrow> 'a narrowing"
+ where "sum a b d = apply_cons (\<lambda>ssa ca.
+ apply_cons (\<lambda>ssb cb. Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))
+ (a d)) (b d)"
lemma [fundef_cong]:
assumes "a d = a' d" "b d = b' d" "d = d'"
shows "sum a b d = sum a' b' d'"
-using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
+ using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
lemma [fundef_cong]:
assumes "f d = f' d" "(\<And>d'. 0 \<le> d' \<and> d' < d \<Longrightarrow> a d' = a' d')"
@@ -132,10 +129,11 @@
moreover have "0 < d' \<Longrightarrow> 0 \<le> d' - 1"
by (simp add: less_integer_def less_eq_integer_def)
ultimately show ?thesis
- by (auto simp add: apply_def Let_def
+ by (auto simp add: apply_def Let_def apply_cons_def
split: narrowing_cons.split narrowing_type.split)
qed
+
subsubsection \<open>Narrowing generator type class\<close>
class narrowing =
@@ -155,6 +153,7 @@
where
"all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
+
subsubsection \<open>class \<open>is_testable\<close>\<close>
text \<open>The class \<open>is_testable\<close> ensures that all necessary type instances are generated.\<close>
@@ -193,6 +192,7 @@
hide_type (open) cfun
hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun
+
subsubsection \<open>Setting up the counterexample generator\<close>
ML_file "Tools/Quickcheck/narrowing_generators.ML"
@@ -213,6 +213,7 @@
z = (conv :: _ => _ => unit) in f)"
unfolding Let_def ensure_testable_def ..
+
subsection \<open>Narrowing for sets\<close>
instantiation set :: (narrowing) narrowing
@@ -224,6 +225,7 @@
end
+
subsection \<open>Narrowing for integers\<close>
@@ -263,8 +265,7 @@
end
-lemma [code, code del]: "partial_term_of (ty :: int itself) t \<equiv> undefined"
- by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: int itself \<Rightarrow> _"]]
lemma [code]:
"partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
@@ -273,7 +274,7 @@
(if i mod 2 = 0
then Code_Evaluation.term_of (- (int_of_integer i) div 2)
else Code_Evaluation.term_of ((int_of_integer i + 1) div 2))"
- by (rule partial_term_of_anything)+
+ by (fact partial_term_of_anything)+
instantiation integer :: narrowing
begin
@@ -286,8 +287,7 @@
end
-lemma [code, code del]: "partial_term_of (ty :: integer itself) t \<equiv> undefined"
- by (rule partial_term_of_anything)+
+declare [[code drop: "partial_term_of :: integer itself \<Rightarrow> _"]]
lemma [code]:
"partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
@@ -319,15 +319,17 @@
(Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
(mkNumber (- i)); } in mkNumber)"
+
subsection \<open>The \<open>find_unused_assms\<close> command\<close>
ML_file "Tools/Quickcheck/find_unused_assms.ML"
+
subsection \<open>Closing up\<close>
hide_type narrowing_type narrowing_term narrowing_cons property
-hide_const map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
+hide_const nth error toEnum marker empty Narrowing_cons conv ensure_testable all exists drawn_from around_zero apply_cons
hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
-hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
+hide_fact empty_def cons_def conv.simps apply_def sum_def ensure_testable_def all_def exists_def
end
-------------- next part --------------
# HG changeset patch
# Parent 65a2474441004d3db26b0c4343f023d131a00c94
for generated Haskell code, never use let-binds with pattern matching: irrefutable patterns destroy partial correctness
diff -r 65a247444100 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Tools/Code/code_haskell.ML Wed Jan 11 20:51:37 2017 +0100
@@ -103,14 +103,14 @@
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
- | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
+ | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) =
let
- val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
- fun print_match ((pat, _), t) vars =
+ val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr);
+ fun print_assignment ((some_v, _), t) vars =
vars
- |> print_bind tyvars some_thm BR pat
+ |> print_bind tyvars some_thm BR (IVar some_v)
|>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
- val (ps, vars') = fold_map print_match binds vars;
+ val (ps, vars') = fold_map print_assignment vs vars;
in brackify_block fxy (str "let {")
ps
(concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
@@ -451,9 +451,9 @@
fun dest_monad (IConst { sym = Constant c, ... } `$ t1 `$ t2) =
if c = c_bind then dest_bind t1 t2
else NONE
- | dest_monad t = case Code_Thingol.split_let t
- of SOME (((pat, ty), tbind), t') =>
- SOME ((SOME ((pat, ty), false), tbind), t')
+ | dest_monad t = case Code_Thingol.split_let_no_pat t
+ of SOME (((some_v, ty), tbind), t') =>
+ SOME ((SOME ((IVar some_v, ty), false), tbind), t')
| NONE => NONE;
val implode_monad = Code_Thingol.unfoldr dest_monad;
fun print_monad print_bind print_term (NONE, t) vars =
diff -r 65a247444100 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML Wed Jan 11 16:43:31 2017 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Jan 11 20:51:37 2017 +0100
@@ -47,7 +47,9 @@
val unfold_app: iterm -> iterm * iterm list
val unfold_abs: iterm -> (vname option * itype) list * iterm
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
+ val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+ val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) list * iterm
val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
val unfold_const_app: iterm -> (const * iterm list) option
@@ -184,8 +186,14 @@
(fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
| _ => NONE);
+val split_let_no_pat =
+ (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body)
+ | _ => NONE);
+
val unfold_let = unfoldr split_let;
+val unfold_let_no_pat = unfoldr split_let_no_pat;
+
fun unfold_const_app t =
case unfold_app t
of (IConst c, ts) => SOME (c, ts)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170121/9001c21d/attachment.sig>
More information about the isabelle-dev
mailing list