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-...@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
module
Generated_Code(Narrowing_type(..), Narrowing_term(..), Term(..), Itself(..),
Typerepa(..), Partial_term_of(..), Is_testable(..),
Narrowing_cons(..), Narrowing(..), Term_of(..), Num(..),
Char(..), Nat(..), typerep_nat, term_of_nat, non_empty, conv,
apply, cons, sum, narrowing_nat, partial_term_of_nat,
typerep_bool, narrowing_bool, partial_term_of_bool,
narrowing_dummy_partial_term_of, narrowing_dummy_narrowing,
ensure_testable, equal_nat, value)
where {
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Typerep;
newtype Narrowing_type = Narrowing_sum_of_products [[Narrowing_type]];
data Narrowing_term = Narrowing_variable [Prelude.Int] Narrowing_type
| Narrowing_constructor Prelude.Int [Narrowing_term];
data Term = Const String Typerep.Typerep | App Term Term
| Abs String Typerep.Typerep Term | Free String Typerep.Typerep;
data Itself a = Type;
class Typerepa a where {
typerep :: Itself a -> Typerep.Typerep;
};
class (Typerepa a) => Partial_term_of a where {
partial_term_of :: Itself a -> Narrowing_term -> Term;
};
class Is_testable a where {
};
data Narrowing_cons a = Narrowing_cons Narrowing_type [[Narrowing_term] -> a];
class Narrowing a where {
narrowing :: Prelude.Int -> Narrowing_cons a;
};
class (Typerepa a) => Term_of a where {
term_of :: a -> Term;
};
instance (Term_of a, Narrowing a, Partial_term_of a,
Is_testable b) => Is_testable (a -> b) where {
};
data Num = One | Bit0 Num | Bit1 Num;
data Char = Zero_char | Char Num;
data Nat = Zero_nat | Suc Nat;
typerep_nat :: Itself Nat -> Typerep.Typerep;
typerep_nat t = Typerep.Typerep "Nat.nat" [];
instance Typerepa Nat where {
typerep = typerep_nat;
};
term_of_nat :: Nat -> Term;
term_of_nat (Suc a) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(term_of_nat a);
term_of_nat Zero_nat =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
instance Term_of Nat where {
term_of = term_of_nat;
};
non_empty :: Narrowing_type -> Bool;
non_empty (Narrowing_sum_of_products ps) = not (null ps);
conv :: forall a. [[Narrowing_term] -> a] -> Narrowing_term -> a;
conv cs (Narrowing_variable p uu) = error ('\0' : map Prelude.toEnum p);
conv cs (Narrowing_constructor i xs) = (cs !! i) xs;
apply ::
forall a b.
(Prelude.Int -> Narrowing_cons (a -> b)) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons b;
apply f a d =
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;
cons :: forall a. a -> Prelude.Int -> Narrowing_cons a;
cons a d = Narrowing_cons (Narrowing_sum_of_products [[]]) [(\ _ -> a)];
sum ::
forall a.
(Prelude.Int -> Narrowing_cons a) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons a;
sum a b d =
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);
narrowing_nat :: Prelude.Int -> Narrowing_cons Nat;
narrowing_nat = sum (cons Zero_nat) (apply (cons Suc) narrowing_nat);
instance Narrowing Nat where {
narrowing = narrowing_nat;
};
partial_term_of_nat :: Itself Nat -> Narrowing_term -> Term;
partial_term_of_nat ty (Narrowing_constructor (1 :: Prelude.Int) [a]) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(partial_term_of_nat Type a);
partial_term_of_nat ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
partial_term_of_nat ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "Nat.nat" []);
instance Partial_term_of Nat where {
partial_term_of = partial_term_of_nat;
};
typerep_bool :: Itself Bool -> Typerep.Typerep;
typerep_bool t = Typerep.Typerep "HOL.bool" [];
instance Typerepa Bool where {
typerep = typerep_bool;
};
narrowing_bool :: Prelude.Int -> Narrowing_cons Bool;
narrowing_bool = sum (cons True) (cons False);
instance Narrowing Bool where {
narrowing = narrowing_bool;
};
instance Is_testable Bool where {
};
partial_term_of_bool :: Itself Bool -> Narrowing_term -> Term;
partial_term_of_bool ty (Narrowing_constructor (1 :: Prelude.Int) []) =
Const "HOL.False" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "HOL.True" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "HOL.bool" []);
instance Partial_term_of Bool where {
partial_term_of = partial_term_of_bool;
};
narrowing_dummy_partial_term_of ::
forall a. (Partial_term_of a) => Itself a -> Narrowing_term -> Term;
narrowing_dummy_partial_term_of = partial_term_of;
narrowing_dummy_narrowing ::
forall a. (Narrowing a) => Prelude.Int -> Narrowing_cons a;
narrowing_dummy_narrowing = narrowing;
ensure_testable :: forall a. (Is_testable a) => a -> a;
ensure_testable f =
let {
_ = (narrowing_dummy_narrowing :: Prelude.Int -> Narrowing_cons Bool);
_ = (narrowing_dummy_partial_term_of ::
Itself Bool -> Narrowing_term -> Term);
_ = conv;
} in f;
equal_nat :: Nat -> Nat -> Bool;
equal_nat Zero_nat (Suc x2) = False;
equal_nat (Suc x2) Zero_nat = False;
equal_nat (Suc x2) (Suc y2) = equal_nat x2 y2;
equal_nat Zero_nat Zero_nat = True;
value :: forall a. a -> Nat -> Nat -> Bool;
value dummy = ensure_testable (\ y x -> equal_nat x y);
}
module
Generated_Code(Narrowing_type(..), Narrowing_term(..), Term(..), Itself(..),
Typerepa(..), Partial_term_of(..), Is_testable(..),
Narrowing_cons(..), Narrowing(..), Term_of(..), Num(..),
Char(..), Nat(..), typerep_nat, term_of_nat, apply_cons, conv,
apply, cons, sum, narrowing_nat, partial_term_of_nat,
typerep_bool, narrowing_bool, partial_term_of_bool,
narrowing_dummy_partial_term_of, narrowing_dummy_narrowing,
ensure_testable, equal_nat, value)
where {
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
import qualified Typerep;
newtype Narrowing_type = Narrowing_sum_of_products [[Narrowing_type]];
data Narrowing_term = Narrowing_variable [Prelude.Int] Narrowing_type
| Narrowing_constructor Prelude.Int [Narrowing_term];
data Term = Const String Typerep.Typerep | App Term Term
| Abs String Typerep.Typerep Term | Free String Typerep.Typerep;
data Itself a = Type;
class Typerepa a where {
typerep :: Itself a -> Typerep.Typerep;
};
class (Typerepa a) => Partial_term_of a where {
partial_term_of :: Itself a -> Narrowing_term -> Term;
};
class Is_testable a where {
};
data Narrowing_cons a = Narrowing_cons Narrowing_type [[Narrowing_term] -> a];
class Narrowing a where {
narrowing :: Prelude.Int -> Narrowing_cons a;
};
class (Typerepa a) => Term_of a where {
term_of :: a -> Term;
};
instance (Term_of a, Narrowing a, Partial_term_of a,
Is_testable b) => Is_testable (a -> b) where {
};
data Num = One | Bit0 Num | Bit1 Num;
data Char = Zero_char | Char Num;
data Nat = Zero_nat | Suc Nat;
typerep_nat :: Itself Nat -> Typerep.Typerep;
typerep_nat t = Typerep.Typerep "Nat.nat" [];
instance Typerepa Nat where {
typerep = typerep_nat;
};
term_of_nat :: Nat -> Term;
term_of_nat (Suc a) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(term_of_nat a);
term_of_nat Zero_nat =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
instance Term_of Nat where {
term_of = term_of_nat;
};
apply_cons ::
forall a b.
([[Narrowing_type]] -> [[Narrowing_term] -> a] -> b) ->
Narrowing_cons a -> b;
apply_cons f (Narrowing_cons (Narrowing_sum_of_products tyss) cs) = f tyss cs;
conv :: forall a. [[Narrowing_term] -> a] -> Narrowing_term -> a;
conv cs (Narrowing_variable p uu) = error ('\0' : map Prelude.toEnum p);
conv cs (Narrowing_constructor i xs) = (cs !! i) xs;
apply ::
forall a b.
(Prelude.Int -> Narrowing_cons (a -> b)) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons b;
apply f a d =
apply_cons
(\ ps cfs ->
apply_cons
(\ psa cas ->
let {
shallow = (0 :: Prelude.Int) < d && not (null psa);
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 -> Narrowing_sum_of_products psa : ab) ps
else []))
aa)
(a (d - (1 :: Prelude.Int))))
(f d);
cons :: forall a. a -> Prelude.Int -> Narrowing_cons a;
cons a d = Narrowing_cons (Narrowing_sum_of_products [[]]) [(\ _ -> a)];
sum ::
forall a.
(Prelude.Int -> Narrowing_cons a) ->
(Prelude.Int -> Narrowing_cons a) -> Prelude.Int -> Narrowing_cons a;
sum a b d =
apply_cons
(\ ssa ca ->
apply_cons
(\ ssb cb ->
Narrowing_cons (Narrowing_sum_of_products (ssa ++ ssb)) (ca ++ cb))
(a d))
(b d);
narrowing_nat :: Prelude.Int -> Narrowing_cons Nat;
narrowing_nat = sum (cons Zero_nat) (apply (cons Suc) narrowing_nat);
instance Narrowing Nat where {
narrowing = narrowing_nat;
};
partial_term_of_nat :: Itself Nat -> Narrowing_term -> Term;
partial_term_of_nat ty (Narrowing_constructor (1 :: Prelude.Int) [a]) =
App (Const "Nat.Suc"
(Typerep.Typerep "fun"
[Typerep.Typerep "Nat.nat" [], Typerep.Typerep "Nat.nat" []]))
(partial_term_of_nat Type a);
partial_term_of_nat ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "Nat.zero_nat_inst.zero_nat" (Typerep.Typerep "Nat.nat" []);
partial_term_of_nat ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "Nat.nat" []);
instance Partial_term_of Nat where {
partial_term_of = partial_term_of_nat;
};
typerep_bool :: Itself Bool -> Typerep.Typerep;
typerep_bool t = Typerep.Typerep "HOL.bool" [];
instance Typerepa Bool where {
typerep = typerep_bool;
};
narrowing_bool :: Prelude.Int -> Narrowing_cons Bool;
narrowing_bool = sum (cons True) (cons False);
instance Narrowing Bool where {
narrowing = narrowing_bool;
};
instance Is_testable Bool where {
};
partial_term_of_bool :: Itself Bool -> Narrowing_term -> Term;
partial_term_of_bool ty (Narrowing_constructor (1 :: Prelude.Int) []) =
Const "HOL.False" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_constructor (0 :: Prelude.Int) []) =
Const "HOL.True" (Typerep.Typerep "HOL.bool" []);
partial_term_of_bool ty (Narrowing_variable p tt) =
Free "_" (Typerep.Typerep "HOL.bool" []);
instance Partial_term_of Bool where {
partial_term_of = partial_term_of_bool;
};
narrowing_dummy_partial_term_of ::
forall a. (Partial_term_of a) => Itself a -> Narrowing_term -> Term;
narrowing_dummy_partial_term_of = partial_term_of;
narrowing_dummy_narrowing ::
forall a. (Narrowing a) => Prelude.Int -> Narrowing_cons a;
narrowing_dummy_narrowing = narrowing;
ensure_testable :: forall a. (Is_testable a) => a -> a;
ensure_testable f =
let {
_ = (narrowing_dummy_narrowing :: Prelude.Int -> Narrowing_cons Bool);
_ = (narrowing_dummy_partial_term_of ::
Itself Bool -> Narrowing_term -> Term);
_ = conv;
} in f;
equal_nat :: Nat -> Nat -> Bool;
equal_nat Zero_nat (Suc x2) = False;
equal_nat (Suc x2) Zero_nat = False;
equal_nat (Suc x2) (Suc y2) = equal_nat x2 y2;
equal_nat Zero_nat Zero_nat = True;
value :: forall a. a -> Nat -> Nat -> Bool;
value dummy = ensure_testable (\ y x -> equal_nat x y);
}
# 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
# 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)
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
