# HG changeset patch # User wenzelm # Date 1460731823 -7200 # Node ID 19a19ee36daa4435ee3663f79b45223ad6784740 # Parent 2e874d9aca436a2a30e9639587bff8141ca08a14# Parent 1de6405023a3769a5f7b21ec70526bf9239d2387 merged diff -r 2e874d9aca43 -r 19a19ee36daa NEWS --- a/NEWS Fri Apr 15 11:15:40 2016 +0200 +++ b/NEWS Fri Apr 15 16:50:23 2016 +0200 @@ -41,6 +41,8 @@ results are isolated from the actual Isabelle/Pure that runs the IDE itself. +* Highlighting of entity def/ref positions wrt. cursor. + *** Isar *** diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Quickcheck_Exhaustive.thy --- a/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Quickcheck_Exhaustive.thy Fri Apr 15 16:50:23 2016 +0200 @@ -1,4 +1,6 @@ -(* Author: Lukas Bulwahn, TU Muenchen *) +(* Title: HOL/Quickcheck_Exhaustive.thy + Author: Lukas Bulwahn, TU Muenchen +*) section \A simple counterexample generator performing exhaustive testing\ @@ -7,32 +9,34 @@ keywords "quickcheck_generator" :: thy_decl begin -subsection \basic operations for exhaustive generators\ +subsection \Basic operations for exhaustive generators\ -definition orelse :: "'a option => 'a option => 'a option" (infixr "orelse" 55) -where - [code_unfold]: "x orelse y = (case x of Some x' => Some x' | None => y)" +definition orelse :: "'a option \ 'a option \ 'a option" (infixr "orelse" 55) + where [code_unfold]: "x orelse y = (case x of Some x' \ Some x' | None \ y)" -subsection \exhaustive generator type classes\ + +subsection \Exhaustive generator type classes\ class exhaustive = term_of + - fixes exhaustive :: "('a \ (bool * term list) option) \ natural \ (bool * term list) option" - + fixes exhaustive :: "('a \ (bool \ term list) option) \ natural \ (bool \ term list) option" + class full_exhaustive = term_of + - fixes full_exhaustive :: "('a * (unit => term) \ (bool * term list) option) \ natural \ (bool * term list) option" + fixes full_exhaustive :: + "('a \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option" instantiation natural :: full_exhaustive begin -function full_exhaustive_natural' :: "(natural * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option" +function full_exhaustive_natural' :: + "(natural \ (unit \ term) \ (bool \ term list) option) \ + natural \ natural \ (bool \ term list) option" where "full_exhaustive_natural' f d i = (if d < i then None - else (f (i, %_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))" + else (f (i, \_. Code_Evaluation.term_of i)) orelse (full_exhaustive_natural' f d (i + 1)))" by pat_completeness auto termination - by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))") - (auto simp add: less_natural_def) + by (relation "measure (\(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) definition "full_exhaustive f d = full_exhaustive_natural' f d 0" @@ -43,15 +47,15 @@ instantiation natural :: exhaustive begin -function exhaustive_natural' :: "(natural => (bool * term list) option) => natural => natural => (bool * term list) option" +function exhaustive_natural' :: + "(natural \ (bool \ term list) option) \ natural \ natural \ (bool \ term list) option" where "exhaustive_natural' f d i = (if d < i then None - else (f i orelse exhaustive_natural' f d (i + 1)))" + else (f i orelse exhaustive_natural' f d (i + 1)))" by pat_completeness auto termination - by (relation "measure (%(_, d, i). nat_of_natural (d + 1 - i))") - (auto simp add: less_natural_def) + by (relation "measure (\(_, d, i). nat_of_natural (d + 1 - i))") (auto simp add: less_natural_def) definition "exhaustive f d = exhaustive_natural' f d 0" @@ -62,12 +66,14 @@ instantiation integer :: exhaustive begin -function exhaustive_integer' :: "(integer => (bool * term list) option) => integer => integer => (bool * term list) option" - where "exhaustive_integer' f d i = (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))" +function exhaustive_integer' :: + "(integer \ (bool \ term list) option) \ integer \ integer \ (bool \ term list) option" + where "exhaustive_integer' f d i = + (if d < i then None else (f i orelse exhaustive_integer' f d (i + 1)))" by pat_completeness auto -termination - by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))") +termination + by (relation "measure (\(_, d, i). nat_of_integer (d + 1 - i))") (auto simp add: less_integer_def nat_of_integer_def) definition "exhaustive f d = exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" @@ -79,15 +85,23 @@ instantiation integer :: full_exhaustive begin -function full_exhaustive_integer' :: "(integer * (unit => term) => (bool * term list) option) => integer => integer => (bool * term list) option" - where "full_exhaustive_integer' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive_integer' f d (i + 1)))" +function full_exhaustive_integer' :: + "(integer \ (unit \ term) \ (bool \ term list) option) \ + integer \ integer \ (bool \ term list) option" + where "full_exhaustive_integer' f d i = + (if d < i then None + else + (case f (i, \_. Code_Evaluation.term_of i) of + Some t \ Some t + | None \ full_exhaustive_integer' f d (i + 1)))" by pat_completeness auto -termination - by (relation "measure (%(_, d, i). nat_of_integer (d + 1 - i))") +termination + by (relation "measure (\(_, d, i). nat_of_integer (d + 1 - i))") (auto simp add: less_integer_def nat_of_integer_def) -definition "full_exhaustive f d = full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" +definition "full_exhaustive f d = + full_exhaustive_integer' f (integer_of_natural d) (- (integer_of_natural d))" instance .. @@ -96,7 +110,7 @@ instantiation nat :: exhaustive begin -definition "exhaustive f d = exhaustive (%x. f (nat_of_natural x)) d" +definition "exhaustive f d = exhaustive (\x. f (nat_of_natural x)) d" instance .. @@ -105,7 +119,8 @@ instantiation nat :: full_exhaustive begin -definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (nat_of_natural x, %_. Code_Evaluation.term_of (nat_of_natural x))) d" +definition "full_exhaustive f d = + full_exhaustive (\(x, xt). f (nat_of_natural x, \_. Code_Evaluation.term_of (nat_of_natural x))) d" instance .. @@ -114,15 +129,18 @@ instantiation int :: exhaustive begin -function exhaustive_int' :: "(int => (bool * term list) option) => int => int => (bool * term list) option" - where "exhaustive_int' f d i = (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))" +function exhaustive_int' :: + "(int \ (bool \ term list) option) \ int \ int \ (bool \ term list) option" + where "exhaustive_int' f d i = + (if d < i then None else (f i orelse exhaustive_int' f d (i + 1)))" by pat_completeness auto -termination - by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto +termination + by (relation "measure (\(_, d, i). nat (d + 1 - i))") auto -definition "exhaustive f d = exhaustive_int' f (int_of_integer (integer_of_natural d)) - (- (int_of_integer (integer_of_natural d)))" +definition "exhaustive f d = + exhaustive_int' f (int_of_integer (integer_of_natural d)) + (- (int_of_integer (integer_of_natural d)))" instance .. @@ -131,15 +149,23 @@ instantiation int :: full_exhaustive begin -function full_exhaustive_int' :: "(int * (unit => term) => (bool * term list) option) => int => int => (bool * term list) option" - where "full_exhaustive_int' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive_int' f d (i + 1)))" +function full_exhaustive_int' :: + "(int \ (unit \ term) \ (bool \ term list) option) \ + int \ int \ (bool \ term list) option" + where "full_exhaustive_int' f d i = + (if d < i then None + else + (case f (i, \_. Code_Evaluation.term_of i) of + Some t \ Some t + | None \ full_exhaustive_int' f d (i + 1)))" by pat_completeness auto -termination - by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto +termination + by (relation "measure (\(_, d, i). nat (d + 1 - i))") auto -definition "full_exhaustive f d = full_exhaustive_int' f (int_of_integer (integer_of_natural d)) - (- (int_of_integer (integer_of_natural d)))" +definition "full_exhaustive f d = + full_exhaustive_int' f (int_of_integer (integer_of_natural d)) + (- (int_of_integer (integer_of_natural d)))" instance .. @@ -148,20 +174,21 @@ instantiation prod :: (exhaustive, exhaustive) exhaustive begin -definition - "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d" +definition "exhaustive f d = exhaustive (\x. exhaustive (\y. f ((x, y))) d) d" instance .. end -definition (in term_syntax) [code_unfold]: "valtermify_pair x y = Code_Evaluation.valtermify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) {\} x {\} y" +definition (in term_syntax) + [code_unfold]: "valtermify_pair x y = + Code_Evaluation.valtermify (Pair :: 'a::typerep \ 'b::typerep \ 'a \ 'b) {\} x {\} y" instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive begin -definition - "full_exhaustive f d = full_exhaustive (%x. full_exhaustive (%y. f (valtermify_pair x y)) d) d" +definition "full_exhaustive f d = + full_exhaustive (\x. full_exhaustive (\y. f (valtermify_pair x y)) d) d" instance .. @@ -172,7 +199,12 @@ fun exhaustive_set where - "exhaustive_set f i = (if i = 0 then None else (f {} orelse exhaustive_set (%A. f A orelse exhaustive (%x. if x \ A then None else f (insert x A)) (i - 1)) (i - 1)))" + "exhaustive_set f i = + (if i = 0 then None + else + f {} orelse + exhaustive_set + (\A. f A orelse exhaustive (\x. if x \ A then None else f (insert x A)) (i - 1)) (i - 1))" instance .. @@ -181,49 +213,70 @@ instantiation set :: (full_exhaustive) full_exhaustive begin -fun full_exhaustive_set +fun full_exhaustive_set where - "full_exhaustive_set f i = (if i = 0 then None else (f valterm_emptyset orelse full_exhaustive_set (%A. f A orelse Quickcheck_Exhaustive.full_exhaustive (%x. if fst x \ fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1)))" + "full_exhaustive_set f i = + (if i = 0 then None + else + f valterm_emptyset orelse + full_exhaustive_set + (\A. f A orelse Quickcheck_Exhaustive.full_exhaustive + (\x. if fst x \ fst A then None else f (valtermify_insert x A)) (i - 1)) (i - 1))" instance .. end -instantiation "fun" :: ("{equal, exhaustive}", exhaustive) exhaustive +instantiation "fun" :: ("{equal,exhaustive}", exhaustive) exhaustive begin -fun exhaustive_fun' :: "(('a => 'b) => (bool * term list) option) => natural => natural => (bool * term list) option" +fun exhaustive_fun' :: + "(('a \ 'b) \ (bool \ term list) option) \ natural \ natural \ (bool \ term list) option" where - "exhaustive_fun' f i d = (exhaustive (%b. f (%_. b)) d) - orelse (if i > 1 then - exhaustive_fun' (%g. exhaustive (%a. exhaustive (%b. - f (g(a := b))) d) d) (i - 1) d else None)" + "exhaustive_fun' f i d = + (exhaustive (\b. f (\_. b)) d) orelse + (if i > 1 then + exhaustive_fun' + (\g. exhaustive (\a. exhaustive (\b. f (g(a := b))) d) d) (i - 1) d else None)" -definition exhaustive_fun :: "(('a => 'b) => (bool * term list) option) => natural => (bool * term list) option" -where - "exhaustive_fun f d = exhaustive_fun' f d d" +definition exhaustive_fun :: + "(('a \ 'b) \ (bool \ term list) option) \ natural \ (bool \ term list) option" + where "exhaustive_fun f d = exhaustive_fun' f d d" instance .. end -definition [code_unfold]: "valtermify_absdummy = (%(v, t). (%_::'a. v, %u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))" +definition [code_unfold]: + "valtermify_absdummy = + (\(v, t). + (\_::'a. v, + \u::unit. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a::typerep)) (t ())))" -definition (in term_syntax) [code_unfold]: "valtermify_fun_upd g a b = Code_Evaluation.valtermify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) {\} g {\} a {\} b" +definition (in term_syntax) + [code_unfold]: "valtermify_fun_upd g a b = + Code_Evaluation.valtermify + (fun_upd :: ('a::typerep \ 'b::typerep) \ 'a \ 'b \ 'a \ 'b) {\} g {\} a {\} b" -instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive +instantiation "fun" :: ("{equal,full_exhaustive}", full_exhaustive) full_exhaustive begin -fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => natural => (bool * term list) option" +fun full_exhaustive_fun' :: + "(('a \ 'b) \ (unit \ term) \ (bool \ term list) option) \ + natural \ natural \ (bool \ term list) option" where - "full_exhaustive_fun' f i d = (full_exhaustive (%v. f (valtermify_absdummy v)) d) - orelse (if i > 1 then - full_exhaustive_fun' (%g. full_exhaustive (%a. full_exhaustive (%b. - f (valtermify_fun_upd g a b)) d) d) (i - 1) d else None)" + "full_exhaustive_fun' f i d = + full_exhaustive (\v. f (valtermify_absdummy v)) d orelse + (if i > 1 then + full_exhaustive_fun' + (\g. full_exhaustive + (\a. full_exhaustive (\b. f (valtermify_fun_upd g a b)) d) d) (i - 1) d + else None)" -definition full_exhaustive_fun :: "(('a => 'b) * (unit => term) => (bool * term list) option) => natural => (bool * term list) option" -where - "full_exhaustive_fun f d = full_exhaustive_fun' f d d" +definition full_exhaustive_fun :: + "(('a \ 'b) \ (unit \ term) \ (bool \ term list) option) \ + natural \ (bool \ term list) option" + where "full_exhaustive_fun f d = full_exhaustive_fun' f d d" instance .. @@ -232,75 +285,110 @@ subsubsection \A smarter enumeration scheme for functions over finite datatypes\ class check_all = enum + term_of + - fixes check_all :: "('a * (unit \ term) \ (bool * term list) option) \ (bool * term list) option" + fixes check_all :: "('a \ (unit \ term) \ (bool \ term list) option) \ (bool * term list) option" fixes enum_term_of :: "'a itself \ unit \ term list" - -fun check_all_n_lists :: "(('a :: check_all) list * (unit \ term list) \ (bool * term list) option) \ natural \ (bool * term list) option" + +fun check_all_n_lists :: "('a::check_all list \ (unit \ term list) \ + (bool \ term list) option) \ natural \ (bool * term list) option" where "check_all_n_lists f n = - (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))" + (if n = 0 then f ([], (\_. [])) + else check_all (\(x, xt). + check_all_n_lists (\(xs, xst). f ((x # xs), (\_. (xt () # xst ())))) (n - 1)))" -definition (in term_syntax) [code_unfold]: "termify_fun_upd g a b = (Code_Evaluation.termify (fun_upd :: ('a :: typerep => 'b :: typerep) => 'a => 'b => 'a => 'b) <\> g <\> a <\> b)" +definition (in term_syntax) + [code_unfold]: "termify_fun_upd g a b = + (Code_Evaluation.termify + (fun_upd :: ('a::typerep \ 'b::typerep) \ 'a \ 'b \ 'a \ 'b) <\> g <\> a <\> b)" -definition mk_map_term :: " (unit \ typerep) \ (unit \ typerep) \ (unit \ term list) \ (unit \ term list) \ unit \ term" -where - "mk_map_term T1 T2 domm rng = - (%_. let T1 = T1 (); - T2 = T2 (); - update_term = (%g (a, b). - Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App - (Code_Evaluation.Const (STR ''Fun.fun_upd'') - (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], - Typerep.Typerep (STR ''fun'') [T1, - Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) - g) a) b) - in - List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" +definition mk_map_term :: + "(unit \ typerep) \ (unit \ typerep) \ + (unit \ term list) \ (unit \ term list) \ unit \ term" + where "mk_map_term T1 T2 domm rng = + (\_. + let + T1 = T1 (); + T2 = T2 (); + update_term = + (\g (a, b). + Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App + (Code_Evaluation.Const (STR ''Fun.fun_upd'') + (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], + Typerep.Typerep (STR ''fun'') [T1, + Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) + g) a) b) + in + List.foldl update_term + (Code_Evaluation.Abs (STR ''x'') T1 + (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip (domm ()) (rng ())))" -instantiation "fun" :: ("{equal, check_all}", check_all) check_all +instantiation "fun" :: ("{equal,check_all}", check_all) check_all begin definition "check_all f = (let - mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) (enum_term_of (TYPE('a))); + mk_term = + mk_map_term + (\_. Typerep.typerep (TYPE('a))) + (\_. Typerep.typerep (TYPE('b))) + (enum_term_of (TYPE('a))); enum = (Enum.enum :: 'a list) - in check_all_n_lists (\(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) (natural_of_nat (length enum)))" + in + check_all_n_lists + (\(ys, yst). f (the o map_of (zip enum ys), mk_term yst)) + (natural_of_nat (length enum)))" -definition enum_term_of_fun :: "('a => 'b) itself => unit => term list" -where - "enum_term_of_fun = (%_ _. let - enum_term_of_a = enum_term_of (TYPE('a)); - mk_term = mk_map_term (%_. Typerep.typerep (TYPE('a))) (%_. Typerep.typerep (TYPE('b))) enum_term_of_a - in map (%ys. mk_term (%_. ys) ()) (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" - +definition enum_term_of_fun :: "('a \ 'b) itself \ unit \ term list" + where "enum_term_of_fun = + (\_ _. + let + enum_term_of_a = enum_term_of (TYPE('a)); + mk_term = + mk_map_term + (\_. Typerep.typerep (TYPE('a))) + (\_. Typerep.typerep (TYPE('b))) + enum_term_of_a + in + map (\ys. mk_term (\_. ys) ()) + (List.n_lists (length (enum_term_of_a ())) (enum_term_of (TYPE('b)) ())))" + instance .. end -fun (in term_syntax) check_all_subsets :: "(('a :: typerep) set * (unit => term) => (bool * term list) option) => ('a * (unit => term)) list => (bool * term list) option" +fun (in term_syntax) check_all_subsets :: + "(('a::typerep) set \ (unit \ term) \ (bool \ term list) option) \ + ('a \ (unit \ term)) list \ (bool \ term list) option" where "check_all_subsets f [] = f valterm_emptyset" -| "check_all_subsets f (x # xs) = check_all_subsets (%s. case f s of Some ts => Some ts | None => f (valtermify_insert x s)) xs" +| "check_all_subsets f (x # xs) = + check_all_subsets (\s. case f s of Some ts \ Some ts | None \ f (valtermify_insert x s)) xs" -definition (in term_syntax) [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a :: typerep) set)" -definition (in term_syntax) [code_unfold]: "termify_insert x s = Code_Evaluation.termify (insert :: ('a::typerep) => 'a set => 'a set) <\> x <\> s" +definition (in term_syntax) + [code_unfold]: "term_emptyset = Code_Evaluation.termify ({} :: ('a::typerep) set)" -definition (in term_syntax) setify :: "('a::typerep) itself => term list => term" +definition (in term_syntax) + [code_unfold]: "termify_insert x s = + Code_Evaluation.termify (insert :: ('a::typerep) \ 'a set \ 'a set) <\> x <\> s" + +definition (in term_syntax) setify :: "('a::typerep) itself \ term list \ term" where - "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" + "setify T ts = foldr (termify_insert T) ts (term_emptyset T)" instantiation set :: (check_all) check_all begin definition "check_all_set f = - check_all_subsets f (zip (Enum.enum :: 'a list) (map (%a. %u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))" + check_all_subsets f + (zip (Enum.enum :: 'a list) + (map (\a. \u :: unit. a) (Quickcheck_Exhaustive.enum_term_of (TYPE ('a)) ())))" -definition enum_term_of_set :: "'a set itself => unit => term list" -where - "enum_term_of_set _ _ = map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))" +definition enum_term_of_set :: "'a set itself \ unit \ term list" + where "enum_term_of_set _ _ = + map (setify (TYPE('a))) (sublists (Quickcheck_Exhaustive.enum_term_of (TYPE('a)) ()))" instance .. @@ -309,12 +397,10 @@ instantiation unit :: check_all begin -definition - "check_all f = f (Code_Evaluation.valtermify ())" +definition "check_all f = f (Code_Evaluation.valtermify ())" -definition enum_term_of_unit :: "unit itself => unit => term list" -where - "enum_term_of_unit = (%_ _. [Code_Evaluation.term_of ()])" +definition enum_term_of_unit :: "unit itself \ unit \ term list" + where "enum_term_of_unit = (\_ _. [Code_Evaluation.term_of ()])" instance .. @@ -325,55 +411,66 @@ begin definition - "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \ Some x' | None \ f (Code_Evaluation.valtermify True))" + "check_all f = + (case f (Code_Evaluation.valtermify False) of + Some x' \ Some x' + | None \ f (Code_Evaluation.valtermify True))" -definition enum_term_of_bool :: "bool itself => unit => term list" -where - "enum_term_of_bool = (%_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" +definition enum_term_of_bool :: "bool itself \ unit \ term list" + where "enum_term_of_bool = (\_ _. map Code_Evaluation.term_of (Enum.enum :: bool list))" instance .. end -definition (in term_syntax) [code_unfold]: "termify_pair x y = Code_Evaluation.termify (Pair :: 'a :: typerep => 'b :: typerep => 'a * 'b) <\> x <\> y" +definition (in term_syntax) [code_unfold]: + "termify_pair x y = + Code_Evaluation.termify (Pair :: 'a::typerep \ 'b :: typerep \ 'a * 'b) <\> x <\> y" instantiation prod :: (check_all, check_all) check_all begin -definition - "check_all f = check_all (%x. check_all (%y. f (valtermify_pair x y)))" +definition "check_all f = check_all (\x. check_all (\y. f (valtermify_pair x y)))" -definition enum_term_of_prod :: "('a * 'b) itself => unit => term list" -where - "enum_term_of_prod = (%_ _. map (%(x, y). termify_pair TYPE('a) TYPE('b) x y) - (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" +definition enum_term_of_prod :: "('a * 'b) itself \ unit \ term list" + where "enum_term_of_prod = + (\_ _. + map (\(x, y). termify_pair TYPE('a) TYPE('b) x y) + (List.product (enum_term_of (TYPE('a)) ()) (enum_term_of (TYPE('b)) ())))" instance .. end -definition (in term_syntax) [code_unfold]: "valtermify_Inl x = Code_Evaluation.valtermify (Inl :: 'a :: typerep => 'a + 'b :: typerep) {\} x" -definition (in term_syntax) [code_unfold]: "valtermify_Inr x = Code_Evaluation.valtermify (Inr :: 'b :: typerep => 'a ::typerep + 'b) {\} x" +definition (in term_syntax) + [code_unfold]: "valtermify_Inl x = + Code_Evaluation.valtermify (Inl :: 'a::typerep \ 'a + 'b :: typerep) {\} x" + +definition (in term_syntax) + [code_unfold]: "valtermify_Inr x = + Code_Evaluation.valtermify (Inr :: 'b::typerep \ 'a::typerep + 'b) {\} x" instantiation sum :: (check_all, check_all) check_all begin definition - "check_all f = check_all (%a. f (valtermify_Inl a)) orelse check_all (%b. f (valtermify_Inr b))" + "check_all f = check_all (\a. f (valtermify_Inl a)) orelse check_all (\b. f (valtermify_Inr b))" -definition enum_term_of_sum :: "('a + 'b) itself => unit => term list" -where - "enum_term_of_sum = (%_ _. - let - T1 = (Typerep.typerep (TYPE('a))); - T2 = (Typerep.typerep (TYPE('b))) - in - map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') - (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) - (enum_term_of (TYPE('a)) ()) @ - map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') - (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) - (enum_term_of (TYPE('b)) ()))" +definition enum_term_of_sum :: "('a + 'b) itself \ unit \ term list" + where "enum_term_of_sum = + (\_ _. + let + T1 = Typerep.typerep (TYPE('a)); + T2 = Typerep.typerep (TYPE('b)) + in + map + (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inl'') + (Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) + (enum_term_of (TYPE('a)) ()) @ + map + (Code_Evaluation.App (Code_Evaluation.Const (STR ''Sum_Type.Inr'') + (Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''Sum_Type.sum'') [T1, T2]]))) + (enum_term_of (TYPE('b)) ()))" instance .. @@ -383,13 +480,13 @@ begin definition - "check_all f = check_all (%(x, t1). check_all (%(y, t2). - f (Char x y, %_. Code_Evaluation.App + "check_all f = check_all (\(x, t1). check_all (\(y, t2). + f (Char x y, \_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of Char) (t1 ())) (t2 ()))))" -definition enum_term_of_char :: "char itself => unit => term list" +definition enum_term_of_char :: "char itself \ unit \ term list" where - "enum_term_of_char = (%_ _. map Code_Evaluation.term_of (Enum.enum :: char list))" + "enum_term_of_char = (\_ _. map Code_Evaluation.term_of (Enum.enum :: char list))" instance .. @@ -399,14 +496,29 @@ begin definition - "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App - (Code_Evaluation.Const (STR ''Option.option.Some'') - (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))" + "check_all f = + f (Code_Evaluation.valtermify (None :: 'a option)) orelse + check_all + (\(x, t). + f + (Some x, + \_. Code_Evaluation.App + (Code_Evaluation.Const (STR ''Option.option.Some'') + (Typerep.Typerep (STR ''fun'') + [Typerep.typerep TYPE('a), + Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))" -definition enum_term_of_option :: "'a option itself => unit => term list" -where - "enum_term_of_option = (% _ _. (Code_Evaluation.term_of (None :: 'a option)) # (map (Code_Evaluation.App (Code_Evaluation.Const (STR ''Option.option.Some'') - (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a), Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) (enum_term_of (TYPE('a)) ())))" +definition enum_term_of_option :: "'a option itself \ unit \ term list" + where "enum_term_of_option = + (\ _ _. + Code_Evaluation.term_of (None :: 'a option) # + (map + (Code_Evaluation.App + (Code_Evaluation.Const (STR ''Option.option.Some'') + (Typerep.Typerep (STR ''fun'') + [Typerep.typerep TYPE('a), + Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]]))) + (enum_term_of (TYPE('a)) ())))" instance .. @@ -416,12 +528,10 @@ instantiation Enum.finite_1 :: check_all begin -definition - "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)" +definition "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^sub>1)" -definition enum_term_of_finite_1 :: "Enum.finite_1 itself => unit => term list" -where - "enum_term_of_finite_1 = (%_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])" +definition enum_term_of_finite_1 :: "Enum.finite_1 itself \ unit \ term list" + where "enum_term_of_finite_1 = (\_ _. [Code_Evaluation.term_of Enum.finite_1.a\<^sub>1])" instance .. @@ -431,12 +541,13 @@ begin definition - "check_all f = (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) - orelse f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))" + "check_all f = + (f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>1) orelse + f (Code_Evaluation.valtermify Enum.finite_2.a\<^sub>2))" -definition enum_term_of_finite_2 :: "Enum.finite_2 itself => unit => term list" -where - "enum_term_of_finite_2 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" +definition enum_term_of_finite_2 :: "Enum.finite_2 itself \ unit \ term list" + where "enum_term_of_finite_2 = + (\_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_2 list))" instance .. @@ -446,13 +557,14 @@ begin definition - "check_all f = (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) - orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) - orelse f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))" + "check_all f = + (f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>1) orelse + f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>2) orelse + f (Code_Evaluation.valtermify Enum.finite_3.a\<^sub>3))" -definition enum_term_of_finite_3 :: "Enum.finite_3 itself => unit => term list" -where - "enum_term_of_finite_3 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" +definition enum_term_of_finite_3 :: "Enum.finite_3 itself \ unit \ term list" + where "enum_term_of_finite_3 = + (\_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_3 list))" instance .. @@ -462,14 +574,15 @@ begin definition - "check_all f = (f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) - orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) - orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) - orelse f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4))" + "check_all f = + f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>1) orelse + f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>2) orelse + f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>3) orelse + f (Code_Evaluation.valtermify Enum.finite_4.a\<^sub>4)" -definition enum_term_of_finite_4 :: "Enum.finite_4 itself => unit => term list" -where - "enum_term_of_finite_4 = (%_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))" +definition enum_term_of_finite_4 :: "Enum.finite_4 itself \ unit \ term list" + where "enum_term_of_finite_4 = + (\_ _. map Code_Evaluation.term_of (Enum.enum :: Enum.finite_4 list))" instance .. @@ -480,69 +593,61 @@ class bounded_forall = fixes bounded_forall :: "('a \ bool) \ natural \ bool" + subsection \Fast exhaustive combinators\ class fast_exhaustive = term_of + fixes fast_exhaustive :: "('a \ unit) \ natural \ unit" -axiomatization throw_Counterexample :: "term list => unit" -axiomatization catch_Counterexample :: "unit => term list option" +axiomatization throw_Counterexample :: "term list \ unit" +axiomatization catch_Counterexample :: "unit \ term list option" code_printing constant throw_Counterexample \ (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)" | constant catch_Counterexample \ - (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)" + (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts \ SOME ts)" + subsection \Continuation passing style functions as plus monad\ - -type_synonym 'a cps = "('a => term list option) => term list option" + +type_synonym 'a cps = "('a \ term list option) \ term list option" definition cps_empty :: "'a cps" -where - "cps_empty = (%cont. None)" + where "cps_empty = (\cont. None)" -definition cps_single :: "'a => 'a cps" -where - "cps_single v = (%cont. cont v)" +definition cps_single :: "'a \ 'a cps" + where "cps_single v = (\cont. cont v)" -definition cps_bind :: "'a cps => ('a => 'b cps) => 'b cps" -where - "cps_bind m f = (%cont. m (%a. (f a) cont))" +definition cps_bind :: "'a cps \ ('a \ 'b cps) \ 'b cps" + where "cps_bind m f = (\cont. m (\a. (f a) cont))" -definition cps_plus :: "'a cps => 'a cps => 'a cps" -where - "cps_plus a b = (%c. case a c of None => b c | Some x => Some x)" +definition cps_plus :: "'a cps \ 'a cps \ 'a cps" + where "cps_plus a b = (\c. case a c of None \ b c | Some x \ Some x)" + +definition cps_if :: "bool \ unit cps" + where "cps_if b = (if b then cps_single () else cps_empty)" -definition cps_if :: "bool => unit cps" -where - "cps_if b = (if b then cps_single () else cps_empty)" +definition cps_not :: "unit cps \ unit cps" + where "cps_not n = (\c. case n (\u. Some []) of None \ c () | Some _ \ None)" -definition cps_not :: "unit cps => unit cps" -where - "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)" - -type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => natural => (bool * term list) option" +type_synonym 'a pos_bound_cps = + "('a \ (bool * term list) option) \ natural \ (bool * term list) option" definition pos_bound_cps_empty :: "'a pos_bound_cps" -where - "pos_bound_cps_empty = (%cont i. None)" + where "pos_bound_cps_empty = (\cont i. None)" -definition pos_bound_cps_single :: "'a => 'a pos_bound_cps" -where - "pos_bound_cps_single v = (%cont i. cont v)" +definition pos_bound_cps_single :: "'a \ 'a pos_bound_cps" + where "pos_bound_cps_single v = (\cont i. cont v)" -definition pos_bound_cps_bind :: "'a pos_bound_cps => ('a => 'b pos_bound_cps) => 'b pos_bound_cps" -where - "pos_bound_cps_bind m f = (%cont i. if i = 0 then None else (m (%a. (f a) cont i) (i - 1)))" +definition pos_bound_cps_bind :: "'a pos_bound_cps \ ('a \ 'b pos_bound_cps) \ 'b pos_bound_cps" + where "pos_bound_cps_bind m f = (\cont i. if i = 0 then None else (m (\a. (f a) cont i) (i - 1)))" -definition pos_bound_cps_plus :: "'a pos_bound_cps => 'a pos_bound_cps => 'a pos_bound_cps" -where - "pos_bound_cps_plus a b = (%c i. case a c i of None => b c i | Some x => Some x)" +definition pos_bound_cps_plus :: "'a pos_bound_cps \ 'a pos_bound_cps \ 'a pos_bound_cps" + where "pos_bound_cps_plus a b = (\c i. case a c i of None \ b c i | Some x \ Some x)" -definition pos_bound_cps_if :: "bool => unit pos_bound_cps" -where - "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" +definition pos_bound_cps_if :: "bool \ unit pos_bound_cps" + where "pos_bound_cps_if b = (if b then pos_bound_cps_single () else pos_bound_cps_empty)" datatype (plugins only: code extraction) (dead 'a) unknown = Unknown | Known 'a @@ -550,35 +655,44 @@ datatype (plugins only: code extraction) (dead 'a) three_valued = Unknown_value | Value 'a | No_value -type_synonym 'a neg_bound_cps = "('a unknown => term list three_valued) => natural => term list three_valued" +type_synonym 'a neg_bound_cps = + "('a unknown \ term list three_valued) \ natural \ term list three_valued" definition neg_bound_cps_empty :: "'a neg_bound_cps" -where - "neg_bound_cps_empty = (%cont i. No_value)" + where "neg_bound_cps_empty = (\cont i. No_value)" + +definition neg_bound_cps_single :: "'a \ 'a neg_bound_cps" + where "neg_bound_cps_single v = (\cont i. cont (Known v))" -definition neg_bound_cps_single :: "'a => 'a neg_bound_cps" -where - "neg_bound_cps_single v = (%cont i. cont (Known v))" - -definition neg_bound_cps_bind :: "'a neg_bound_cps => ('a => 'b neg_bound_cps) => 'b neg_bound_cps" -where - "neg_bound_cps_bind m f = (%cont i. if i = 0 then cont Unknown else m (%a. case a of Unknown => cont Unknown | Known a' => f a' cont i) (i - 1))" +definition neg_bound_cps_bind :: "'a neg_bound_cps \ ('a \ 'b neg_bound_cps) \ 'b neg_bound_cps" + where "neg_bound_cps_bind m f = + (\cont i. + if i = 0 then cont Unknown + else m (\a. case a of Unknown \ cont Unknown | Known a' \ f a' cont i) (i - 1))" -definition neg_bound_cps_plus :: "'a neg_bound_cps => 'a neg_bound_cps => 'a neg_bound_cps" -where - "neg_bound_cps_plus a b = (%c i. case a c i of No_value => b c i | Value x => Value x | Unknown_value => (case b c i of No_value => Unknown_value | Value x => Value x | Unknown_value => Unknown_value))" - -definition neg_bound_cps_if :: "bool => unit neg_bound_cps" -where - "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)" +definition neg_bound_cps_plus :: "'a neg_bound_cps \ 'a neg_bound_cps \ 'a neg_bound_cps" + where "neg_bound_cps_plus a b = + (\c i. + case a c i of + No_value \ b c i + | Value x \ Value x + | Unknown_value \ + (case b c i of + No_value \ Unknown_value + | Value x \ Value x + | Unknown_value \ Unknown_value))" -definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps" -where - "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)" +definition neg_bound_cps_if :: "bool \ unit neg_bound_cps" + where "neg_bound_cps_if b = (if b then neg_bound_cps_single () else neg_bound_cps_empty)" -definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps" -where - "pos_bound_cps_not n = (%c i. case n (%u. Value []) i of No_value => c () | Value _ => None | Unknown_value => None)" +definition neg_bound_cps_not :: "unit pos_bound_cps \ unit neg_bound_cps" + where "neg_bound_cps_not n = + (\c i. case n (\u. Some (True, [])) i of None \ c (Known ()) | Some _ \ No_value)" + +definition pos_bound_cps_not :: "unit neg_bound_cps \ unit pos_bound_cps" + where "pos_bound_cps_not n = + (\c i. case n (\u. Value []) i of No_value \ c () | Value _ \ None | Unknown_value \ None)" + subsection \Defining generators for any first-order data type\ @@ -590,6 +704,7 @@ declare [[quickcheck_batch_tester = exhaustive]] + subsection \Defining generators for abstract types\ ML_file "Tools/Quickcheck/abstract_generators.ML" @@ -615,10 +730,11 @@ end *) hide_fact (open) orelse_def -no_notation orelse (infixr "orelse" 55) +no_notation orelse (infixr "orelse" 55) -hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair - valtermify_Inl valtermify_Inr +hide_const valtermify_absdummy valtermify_fun_upd + valterm_emptyset valtermify_insert + valtermify_pair valtermify_Inl valtermify_Inr termify_fun_upd term_emptyset termify_insert termify_pair setify hide_const (open) @@ -631,9 +747,12 @@ orelse unknown mk_map_term check_all_n_lists check_all_subsets hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued + hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not - pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not - neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not + pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind + pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not + neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind + neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not Unknown Known Unknown_value Value No_value end diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Quickcheck_Random.thy --- a/src/HOL/Quickcheck_Random.thy Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Quickcheck_Random.thy Fri Apr 15 16:50:23 2016 +0200 @@ -1,4 +1,6 @@ -(* Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen *) +(* Title: HOL/Quickcheck_Random.thy + Author: Florian Haftmann & Lukas Bulwahn, TU Muenchen +*) section \A simple counterexample generator performing random testing\ diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Apr 15 16:50:23 2016 +0200 @@ -1960,7 +1960,7 @@ val setT = HOLogic.mk_setT T val elems = HOLogic.mk_set T ts val ([dots], ctxt') = ctxt - |> Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix.mixfix "...")] + |> Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix.mixfix "...")] (* check expected values *) val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT) val () = diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Quickcheck/abstract_generators.ML --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Apr 15 16:50:23 2016 +0200 @@ -7,7 +7,7 @@ signature ABSTRACT_GENERATORS = sig val quickcheck_generator : string -> term option -> term list -> theory -> theory -end; +end structure Abstract_Generators : ABSTRACT_GENERATORS = struct @@ -15,19 +15,17 @@ fun check_constrs ctxt tyco constrs = let fun check_type c = - case try (dest_Type o body_type o fastype_of) c of + (case try (dest_Type o body_type o fastype_of) c of NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.") | SOME (tyco', vs) => if not (tyco' = tyco) then error (Syntax.string_of_term ctxt c ^ " has mismatching result type. " ^ "Expected type constructor " ^ quote tyco ^ ", but found " ^ quote tyco' ^ ".") else - case try (map dest_TFree) vs of + (case try (map dest_TFree) vs of NONE => error (Syntax.string_of_term ctxt c ^ " has mismatching result type.") - | SOME _ => () - in - map check_type constrs - end - + | SOME _ => ())) + in map check_type constrs end + fun gen_quickcheck_generator prep_tyco prep_term tyco_raw opt_pred_raw constrs_raw thy = let val ctxt = Proof_Context.init_global thy @@ -36,36 +34,36 @@ val constrs = map (prep_term ctxt) constrs_raw val _ = check_constrs ctxt tyco constrs val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs))))) - val name = Long_Name.base_name tyco + val name = Long_Name.base_name tyco fun mk_dconstrs (Const (s, T)) = - (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T)) - | mk_dconstrs t = error (Syntax.string_of_term ctxt t ^ - " is not a valid constructor for quickcheck_generator, which expects a constant.") + (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T)) + | mk_dconstrs t = + error (Syntax.string_of_term ctxt t ^ + " is not a valid constructor for quickcheck_generator, which expects a constant.") fun the_descr _ _ = - let - val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))] - in - (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], [])) - end + let val descr = [(0, (tyco, map Old_Datatype_Aux.DtTFree vs, map mk_dconstrs constrs))] + in (descr, vs, [tyco], name, ([name], []), ([Type (tyco, map TFree vs)], [])) end fun ensure_sort (sort, instantiate) = - Quickcheck_Common.ensure_sort (((@{sort typerep}, @{sort term_of}), sort), - (the_descr, instantiate)) - Old_Datatype_Aux.default_config [tyco] + Quickcheck_Common.ensure_sort + (((@{sort typerep}, @{sort term_of}), sort), (the_descr, instantiate)) + Old_Datatype_Aux.default_config [tyco] in thy - |> ensure_sort (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype) + |> ensure_sort + (@{sort full_exhaustive}, Exhaustive_Generators.instantiate_full_exhaustive_datatype) |> ensure_sort (@{sort exhaustive}, Exhaustive_Generators.instantiate_exhaustive_datatype) |> ensure_sort (@{sort random}, Random_Generators.instantiate_random_datatype) - |> (case opt_pred of NONE => I | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco))) + |> (case opt_pred of NONE => I + | SOME t => Context.theory_map (Quickcheck_Common.register_predicate (t, tyco))) end val quickcheck_generator = gen_quickcheck_generator (K I) (K I) - + val quickcheck_generator_cmd = gen_quickcheck_generator ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true}) Syntax.read_term - + val _ = Outer_Syntax.command @{command_keyword quickcheck_generator} "define quickcheck generators for abstract types" @@ -75,4 +73,4 @@ >> (fn ((tyco, opt_pred), constrs) => Toplevel.theory (quickcheck_generator_cmd tyco opt_pred constrs))) -end; +end diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Apr 15 16:50:23 2016 +0200 @@ -6,28 +6,30 @@ signature EXHAUSTIVE_GENERATORS = sig - val compile_generator_expr: - Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option + val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list -> + (bool * term list) option * Quickcheck.report option val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list val compile_validator_exprs: Proof.context -> term list -> (int -> bool) list - val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) - -> Proof.context -> Proof.context - val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list) - -> Proof.context -> Proof.context - val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) -> Proof.context -> Proof.context + val put_counterexample: + (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) -> + Proof.context -> Proof.context + val put_counterexample_batch: (unit -> (Code_Numeral.natural -> term list option) list) -> + Proof.context -> Proof.context + val put_validator_batch: (unit -> (Code_Numeral.natural -> bool) list) -> + Proof.context -> Proof.context exception Counterexample of term list val smart_quantifier : bool Config.T val optimise_equality : bool Config.T val quickcheck_pretty : bool Config.T val setup_exhaustive_datatype_interpretation : theory -> theory val setup_bounded_forall_datatype_interpretation : theory -> theory - val instantiate_full_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> - (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory + (string * sort) list -> string list -> string -> string list * string list -> + typ list * typ list -> theory -> theory val instantiate_exhaustive_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> - (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory - -end; + (string * sort) list -> string list -> string -> string list * string list -> + typ list * typ list -> theory -> theory +end structure Exhaustive_Generators : EXHAUSTIVE_GENERATORS = struct @@ -43,44 +45,40 @@ val bounded_forall = Attrib.setup_config_bool @{binding quickcheck_bounded_forall} (K false) val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true) val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true) - + (** abstract syntax **) -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"}); +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \ Code_Evaluation.term"}) val size = @{term "i :: natural"} val size_pred = @{term "(i :: natural) - 1"} val size_ge_zero = @{term "(i :: natural) > 0"} fun mk_none_continuation (x, y) = - let - val (T as Type(@{type_name "option"}, _)) = fastype_of x - in - Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y - end + let val (T as Type (@{type_name option}, _)) = fastype_of x + in Const (@{const_name orelse}, T --> T --> T) $ x $ y end fun mk_if (b, t, e) = - let - val T = fastype_of t - in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end + let val T = fastype_of t + in Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e end + (* handling inductive datatypes *) (** constructing generator instances **) -exception FUNCTION_TYPE; +exception FUNCTION_TYPE exception Counterexample of term list -val resultT = @{typ "(bool * term list) option"}; +val resultT = @{typ "(bool * term list) option"} -val exhaustiveN = "exhaustive"; -val full_exhaustiveN = "full_exhaustive"; -val bounded_forallN = "bounded_forall"; +val exhaustiveN = "exhaustive" +val full_exhaustiveN = "full_exhaustive" +val bounded_forallN = "bounded_forall" -fun fast_exhaustiveT T = (T --> @{typ unit}) - --> @{typ natural} --> @{typ unit} +fun fast_exhaustiveT T = (T --> @{typ unit}) --> @{typ natural} --> @{typ unit} fun exhaustiveT T = (T --> resultT) --> @{typ natural} --> resultT @@ -100,9 +98,7 @@ |> map (fn (T, cs) => map (mk_consexpr T) cs) |> map mk_rhs val lhss = map2 (fn t => fn T => t $ test_function T $ size) exhaustives Ts - in - map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) - end + in map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) end fun gen_mk_call c T = (T, fn t => c T $ absdummy T t $ size_pred) @@ -110,9 +106,7 @@ let val T = Type (tyco, Ts) val _ = if not (null fTs) then raise FUNCTION_TYPE else () - in - (T, fn t => nth functerms k $ absdummy T t $ size_pred) - end + in (T, fn t => nth functerms k $ absdummy T t $ size_pred) end fun gen_mk_consexpr test_function simpleT (c, xs) = let @@ -125,50 +119,47 @@ fun mk_equations functerms = let fun test_function T = Free ("f", T --> resultT) - val mk_call = gen_mk_call (fn T => - Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)) + val mk_call = gen_mk_call (fn T => Const (@{const_name exhaustive}, exhaustiveT T)) val mk_aux_call = gen_mk_aux_call functerms val mk_consexpr = gen_mk_consexpr test_function fun mk_rhs exprs = - mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name "None"}, resultT)) - in - mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) - end + mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) + in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end fun mk_bounded_forall_equations functerms = let fun test_function T = Free ("P", T --> @{typ bool}) - val mk_call = gen_mk_call (fn T => - Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, - bounded_forallT T)) + val mk_call = gen_mk_call (fn T => Const (@{const_name bounded_forall}, bounded_forallT T)) val mk_aux_call = gen_mk_aux_call functerms val mk_consexpr = gen_mk_consexpr test_function - fun mk_rhs exprs = - mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term "True"}) - in - mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) - end - + fun mk_rhs exprs = mk_if (size_ge_zero, foldr1 HOLogic.mk_conj exprs, @{term True}) + in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end + fun mk_full_equations functerms = let fun test_function T = Free ("f", termifyT T --> resultT) - fun case_prod_const T = HOLogic.case_prod_const (T, @{typ "unit => Code_Evaluation.term"}, resultT) + fun case_prod_const T = + HOLogic.case_prod_const (T, @{typ "unit \ Code_Evaluation.term"}, resultT) fun mk_call T = let - val full_exhaustive = - Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, - full_exhaustiveT T) - in - (T, fn t => full_exhaustive $ - (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred) + val full_exhaustive = Const (@{const_name full_exhaustive}, full_exhaustiveT T) + in + (T, + fn t => + full_exhaustive $ + (case_prod_const T $ absdummy T (absdummy @{typ "unit \ Code_Evaluation.term"} t)) $ + size_pred) end fun mk_aux_call fTs (k, _) (tyco, Ts) = let val T = Type (tyco, Ts) val _ = if not (null fTs) then raise FUNCTION_TYPE else () in - (T, fn t => nth functerms k $ - (case_prod_const T $ absdummy T (absdummy @{typ "unit => Code_Evaluation.term"} t)) $ size_pred) + (T, + fn t => + nth functerms k $ + (case_prod_const T $ absdummy T (absdummy @{typ "unit \ Code_Evaluation.term"} t)) $ + size_pred) end fun mk_consexpr simpleT (c, xs) = let @@ -176,29 +167,30 @@ val constr = Const (c, Ts ---> simpleT) val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) val Eval_App = - Const (@{const_name Code_Evaluation.App}, HOLogic.termT --> HOLogic.termT --> HOLogic.termT) + Const (@{const_name Code_Evaluation.App}, + HOLogic.termT --> HOLogic.termT --> HOLogic.termT) val Eval_Const = - Const (@{const_name Code_Evaluation.Const}, HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) - val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) - bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) - val start_term = test_function simpleT $ - (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"} - $ (list_comb (constr, bounds)) $ absdummy @{typ unit} term) + Const (@{const_name Code_Evaluation.Const}, + HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) + val term = + fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) + bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) + val start_term = + test_function simpleT $ + (HOLogic.pair_const simpleT @{typ "unit \ Code_Evaluation.term"} $ + (list_comb (constr, bounds)) $ absdummy @{typ unit} term) in fold_rev (fn f => fn t => f t) fns start_term end fun mk_rhs exprs = - mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, - Const (@{const_name "None"}, resultT)) - in - mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) - end - + mk_if (size_ge_zero, foldr1 mk_none_continuation exprs, Const (@{const_name None}, resultT)) + in mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end + (** instantiating generator classes **) - + fun contains_recursive_type_under_function_types xs = exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs - + fun instantiate_datatype (name, constprfx, sort, mk_equations, mk_T, argnames) config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = if not (contains_recursive_type_under_function_types descr) then @@ -218,106 +210,111 @@ ("Creation of " ^ name ^ " failed because the datatype is recursive under a function type"); thy) -val instantiate_bounded_forall_datatype = instantiate_datatype - ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, - mk_bounded_forall_equations, bounded_forallT, ["P", "i"]); +val instantiate_bounded_forall_datatype = + instantiate_datatype + ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, + mk_bounded_forall_equations, bounded_forallT, ["P", "i"]) -val instantiate_exhaustive_datatype = instantiate_datatype - ("exhaustive generators", exhaustiveN, @{sort exhaustive}, - mk_equations, exhaustiveT, ["f", "i"]) +val instantiate_exhaustive_datatype = + instantiate_datatype + ("exhaustive generators", exhaustiveN, @{sort exhaustive}, + mk_equations, exhaustiveT, ["f", "i"]) -val instantiate_full_exhaustive_datatype = instantiate_datatype - ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive}, - mk_full_equations, full_exhaustiveT, ["f", "i"]) +val instantiate_full_exhaustive_datatype = + instantiate_datatype + ("full exhaustive generators", full_exhaustiveN, @{sort full_exhaustive}, + mk_full_equations, full_exhaustiveT, ["f", "i"]) + (* building and compiling generator expressions *) fun mk_let_expr (x, t, e) genuine = - let - val (T1, T2) = (fastype_of x, fastype_of (e genuine)) - in - Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) - end + let val (T1, T2) = (fastype_of x, fastype_of (e genuine)) + in Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine) end fun mk_safe_let_expr genuine_only none safe (x, t, e) genuine = let val (T1, T2) = (fastype_of x, fastype_of (e genuine)) - val if_t = Const (@{const_name "If"}, @{typ bool} --> T2 --> T2 --> T2) + val if_t = Const (@{const_name If}, @{typ bool} --> T2 --> T2 --> T2) in - Const (@{const_name "Quickcheck_Random.catch_match"}, T2 --> T2 --> T2) $ + Const (@{const_name Quickcheck_Random.catch_match}, T2 --> T2 --> T2) $ (Const (@{const_name Let}, T1 --> (T1 --> T2) --> T2) $ t $ lambda x (e genuine)) $ (if_t $ genuine_only $ none $ safe false) end fun mk_test_term lookup mk_closure mk_if mk_let none_t return ctxt = let - val cnstrs = flat (maps - (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) - (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) - Quickcheck_Common.compat_prefs))) - fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of - (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' - | _ => false) + val cnstrs = + flat (maps + (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd) + (Symtab.dest + (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) Quickcheck_Common.compat_prefs))) + fun is_constrt (Const (s, T), ts) = + (case (AList.lookup (op =) cnstrs s, body_type T) of + (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' + | _ => false) | is_constrt _ = false fun mk_naive_test_term t = - fold_rev mk_closure (map lookup (Term.add_free_names t [])) - (mk_if (t, none_t, return) true) + fold_rev mk_closure (map lookup (Term.add_free_names t [])) (mk_if (t, none_t, return) true) fun mk_test (vars, check) = fold_rev mk_closure (map lookup vars) check fun mk_smart_test_term' concl bound_vars assms genuine = let fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t []) fun mk_equality_term (lhs, f as Free (x, _)) c (assm, assms) = - if member (op =) (Term.add_free_names lhs bound_vars) x then - c (assm, assms) - else - (let - val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms - fun safe genuine = - the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine) - in - mk_test (remove (op =) x (vars_of assm), - mk_let safe f (try lookup x) lhs - (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) - - end) + if member (op =) (Term.add_free_names lhs bound_vars) x then + c (assm, assms) + else + let + val rec_call = mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms + fun safe genuine = + the_default I (Option.map mk_closure (try lookup x)) (rec_call genuine) + in + mk_test (remove (op =) x (vars_of assm), + mk_let safe f (try lookup x) lhs + (mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) + + end | mk_equality_term (lhs, t) c (assm, assms) = - if is_constrt (strip_comb t) then - let - val (constr, args) = strip_comb t - val T = fastype_of t - val vars = map Free (Variable.variant_frees ctxt (concl :: assms) - (map (fn t => ("x", fastype_of t)) args)) - val varnames = map (fst o dest_Free) vars - val dummy_var = Free (singleton - (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) - val new_assms = map HOLogic.mk_eq (vars ~~ args) - val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) - val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine - in - mk_test (vars_of lhs, - Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs - [(list_comb (constr, vars), cont_t), (dummy_var, none_t)]) - end - else c (assm, assms) + if is_constrt (strip_comb t) then + let + val (constr, args) = strip_comb t + val T = fastype_of t + val vars = + map Free + (Variable.variant_frees ctxt (concl :: assms) + (map (fn t => ("x", fastype_of t)) args)) + val varnames = map (fst o dest_Free) vars + val dummy_var = + Free (singleton + (Variable.variant_frees ctxt (concl :: assms @ vars)) ("dummy", T)) + val new_assms = map HOLogic.mk_eq (vars ~~ args) + val bound_vars' = union (op =) (vars_of lhs) (union (op =) varnames bound_vars) + val cont_t = mk_smart_test_term' concl bound_vars' (new_assms @ assms) genuine + in + mk_test (vars_of lhs, + Case_Translation.make_case ctxt Case_Translation.Quiet Name.context lhs + [(list_comb (constr, vars), cont_t), (dummy_var, none_t)]) + end + else c (assm, assms) fun default (assm, assms) = - mk_test (vars_of assm, - mk_if (HOLogic.mk_not assm, none_t, - mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) + mk_test + (vars_of assm, + mk_if (HOLogic.mk_not assm, none_t, + mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms) genuine) in - case assms of [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) - | assm :: assms => + (case assms of + [] => mk_test (vars_of concl, mk_if (concl, none_t, return) genuine) + | assm :: assms => if Config.get ctxt optimise_equality then (case try HOLogic.dest_eq assm of SOME (lhs, rhs) => mk_equality_term (lhs, rhs) (mk_equality_term (rhs, lhs) default) (assm, assms) | NONE => default (assm, assms)) - else default (assm, assms) + else default (assm, assms)) end val mk_smart_test_term = Quickcheck_Common.strip_imp #> (fn (assms, concl) => mk_smart_test_term' concl [] assms true) - in - if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term - end + in if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term end fun mk_fast_generator_expr ctxt (t, eval_terms) = let @@ -327,26 +324,30 @@ fun lookup v = the (AList.lookup (op =) (names ~~ frees) v) val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' val depth = Free (depth_name, @{typ natural}) - fun return _ = @{term "throw_Counterexample :: term list => unit"} $ - (HOLogic.mk_list @{typ "term"} - (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) + fun return _ = + @{term "throw_Counterexample :: term list \ unit"} $ + (HOLogic.mk_list @{typ term} + (map (fn t => HOLogic.mk_term_of (fastype_of t) t) (frees @ eval_terms))) fun mk_exhaustive_closure (free as Free (_, T)) t = - Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, - fast_exhaustiveT T) - $ lambda free t $ depth + Const (@{const_name fast_exhaustive}, fast_exhaustiveT T) $ lambda free t $ depth val none_t = @{term "()"} fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) - val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt + val mk_test_term = + mk_test_term lookup mk_exhaustive_closure mk_safe_if mk_let none_t return ctxt in lambda depth (@{term "catch_Counterexample :: unit => term list option"} $ mk_test_term t) end -fun mk_unknown_term T = HOLogic.reflect_term (Const (@{const_name Quickcheck_Exhaustive.unknown}, T)) +fun mk_unknown_term T = + HOLogic.reflect_term (Const (@{const_name unknown}, T)) -fun mk_safe_term t = @{term "Quickcheck_Random.catch_match :: term => term => term"} - $ (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) +fun mk_safe_term t = + @{term "Quickcheck_Random.catch_match :: term \ term \ term"} $ + (HOLogic.mk_term_of (fastype_of t) t) $ mk_unknown_term (fastype_of t) -fun mk_return t genuine = @{term "Some :: bool * term list => (bool * term list) option"} $ - (HOLogic.pair_const @{typ bool} @{typ "term list"} $ Quickcheck_Common.reflect_bool genuine $ t) +fun mk_return t genuine = + @{term "Some :: bool \ term list \ (bool \ term list) option"} $ + (HOLogic.pair_const @{typ bool} @{typ "term list"} $ + Quickcheck_Common.reflect_bool genuine $ t) fun mk_generator_expr ctxt (t, eval_terms) = let @@ -357,15 +358,16 @@ val ([depth_name, genuine_only_name], _) = Variable.variant_fixes ["depth", "genuine_only"] ctxt' val depth = Free (depth_name, @{typ natural}) - val genuine_only = Free (genuine_only_name, @{typ bool}) - val return = mk_return (HOLogic.mk_list @{typ "term"} + val genuine_only = Free (genuine_only_name, @{typ bool}) + val return = + mk_return (HOLogic.mk_list @{typ term} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) frees @ map mk_safe_term eval_terms)) fun mk_exhaustive_closure (free as Free (_, T)) t = - Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T) - $ lambda free t $ depth - val none_t = Const (@{const_name "None"}, resultT) + Const (@{const_name exhaustive}, exhaustiveT T) $ lambda free t $ depth + val none_t = Const (@{const_name None}, resultT) val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t - fun mk_let safe def v_opt t e = mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e) + fun mk_let safe def v_opt t e = + mk_safe_let_expr genuine_only none_t safe (the_default def v_opt, t, e) val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt in lambda genuine_only (lambda depth (mk_test_term t)) end @@ -379,33 +381,35 @@ Variable.variant_fixes ["depth", "genuine_only"] ctxt' val (term_names, _) = Variable.variant_fixes (map (prefix "t_") names) ctxt'' val depth = Free (depth_name, @{typ natural}) - val genuine_only = Free (genuine_only_name, @{typ bool}) - val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names + val genuine_only = Free (genuine_only_name, @{typ bool}) + val term_vars = map (fn n => Free (n, @{typ "unit \ term"})) term_names fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v) - val return = mk_return (HOLogic.mk_list @{typ term} + val return = + mk_return + (HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars @ map mk_safe_term eval_terms)) fun mk_exhaustive_closure (free as Free (_, T), term_var) t = if Sign.of_sort thy (T, @{sort check_all}) then - Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T) - $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT) - $ lambda free (lambda term_var t)) + Const (@{const_name check_all}, check_allT T) $ + (HOLogic.case_prod_const (T, @{typ "unit \ term"}, resultT) $ + lambda free (lambda term_var t)) else - Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"}, full_exhaustiveT T) - $ (HOLogic.case_prod_const (T, @{typ "unit => term"}, resultT) - $ lambda free (lambda term_var t)) $ depth - val none_t = Const (@{const_name "None"}, resultT) + Const (@{const_name full_exhaustive}, full_exhaustiveT T) $ + (HOLogic.case_prod_const (T, @{typ "unit \ term"}, resultT) $ + lambda free (lambda term_var t)) $ depth + val none_t = Const (@{const_name None}, resultT) val mk_if = Quickcheck_Common.mk_safe_if genuine_only none_t fun mk_let safe _ (SOME (v, term_var)) t e = - mk_safe_let_expr genuine_only none_t safe (v, t, - e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))]) + mk_safe_let_expr genuine_only none_t safe (v, t, + e #> subst_free [(term_var, absdummy @{typ unit} (mk_safe_term t))]) | mk_let safe v NONE t e = mk_safe_let_expr genuine_only none_t safe (v, t, e) val mk_test_term = mk_test_term lookup mk_exhaustive_closure mk_if mk_let none_t return ctxt in lambda genuine_only (lambda depth (mk_test_term t)) end fun mk_parametric_generator_expr mk_generator_expr = - Quickcheck_Common.gen_mk_parametric_generator_expr + Quickcheck_Common.gen_mk_parametric_generator_expr ((mk_generator_expr, - absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name "None"}, resultT)))), + absdummy @{typ bool} (absdummy @{typ natural} (Const (@{const_name None}, resultT)))), @{typ bool} --> @{typ natural} --> resultT) fun mk_validator_expr ctxt t = @@ -418,115 +422,116 @@ val ([depth_name], _) = Variable.variant_fixes ["depth"] ctxt' val depth = Free (depth_name, @{typ natural}) fun mk_bounded_forall (Free (s, T)) t = - Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T) - $ lambda (Free (s, T)) t $ depth + Const (@{const_name bounded_forall}, bounded_forallT T) $ lambda (Free (s, T)) t $ depth fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) val mk_test_term = mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt in lambda depth (mk_test_term t) end - -fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = +fun mk_bounded_forall_generator_expr ctxt (t, eval_terms) = let val frees = Term.add_free_names t [] - val dummy_term = @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') - (Typerep.Typerep (STR ''dummy'') [])"} - val return = @{term "Some :: term list => term list option"} $ - (HOLogic.mk_list @{typ "term"} - (replicate (length frees + length eval_terms) dummy_term)) + val dummy_term = + @{term "Code_Evaluation.Const (STR ''Pure.dummy_pattern'') (Typerep.Typerep (STR ''dummy'') [])"} + val return = + @{term "Some :: term list => term list option"} $ + (HOLogic.mk_list @{typ term} (replicate (length frees + length eval_terms) dummy_term)) val wrap = absdummy @{typ bool} - (@{term "If :: bool => term list option => term list option => term list option"} $ + (@{term "If :: bool \ term list option \ term list option \ term list option"} $ Bound 0 $ @{term "None :: term list option"} $ return) in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end - + (** generator compiliation **) structure Data = Proof_Data ( type T = - (unit -> Code_Numeral.natural -> bool -> - Code_Numeral.natural -> (bool * term list) option) * + (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> (bool * term list) option) * (unit -> (Code_Numeral.natural -> term list option) list) * - (unit -> (Code_Numeral.natural -> bool) list); + (unit -> (Code_Numeral.natural -> bool) list) val empty: T = (fn () => raise Fail "counterexample", fn () => raise Fail "counterexample_batch", - fn () => raise Fail "validator_batch"); - fun init _ = empty; -); + fn () => raise Fail "validator_batch") + fun init _ = empty +) -val get_counterexample = #1 o Data.get; -val get_counterexample_batch = #2 o Data.get; -val get_validator_batch = #3 o Data.get; +val get_counterexample = #1 o Data.get +val get_counterexample_batch = #2 o Data.get +val get_validator_batch = #3 o Data.get -val put_counterexample = Data.map o @{apply 3(1)} o K; -val put_counterexample_batch = Data.map o @{apply 3(2)} o K; -val put_validator_batch = Data.map o @{apply 3(3)} o K; +val put_counterexample = Data.map o @{apply 3(1)} o K +val put_counterexample_batch = Data.map o @{apply 3(2)} o K +val put_validator_batch = Data.map o @{apply 3(3)} o K -val target = "Quickcheck"; +val target = "Quickcheck" fun compile_generator_expr_raw ctxt ts = let - val mk_generator_expr = + val mk_generator_expr = if Config.get ctxt fast then mk_fast_generator_expr else if Config.get ctxt bounded_forall then mk_bounded_forall_generator_expr else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr - val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts; - val compile = Code_Runtime.dynamic_value_strict - (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample") - ctxt (SOME target) (fn proc => fn g => - fn card => fn genuine_only => fn size => g card genuine_only size + val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts + val compile = + Code_Runtime.dynamic_value_strict + (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample") + ctxt (SOME target) + (fn proc => fn g => fn card => fn genuine_only => fn size => + g card genuine_only size |> (Option.map o apsnd o map) proc) t' [] in - fn genuine_only => fn [card, size] => rpair NONE (compile card genuine_only size |> - (if Config.get ctxt quickcheck_pretty then - Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I)) - end; + fn genuine_only => fn [card, size] => + rpair NONE (compile card genuine_only size + |> (if Config.get ctxt quickcheck_pretty then + Option.map (apsnd (map Quickcheck_Common.post_process_term)) else I)) + end fun compile_generator_expr ctxt ts = - let - val compiled = compile_generator_expr_raw ctxt ts; - in fn genuine_only => fn [card, size] => - compiled genuine_only [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size] - end; + let val compiled = compile_generator_expr_raw ctxt ts in + fn genuine_only => fn [card, size] => + compiled genuine_only + [Code_Numeral.natural_of_integer card, Code_Numeral.natural_of_integer size] + end fun compile_generator_exprs_raw ctxt ts = let - val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts; - val compiles = Code_Runtime.dynamic_value_strict - (get_counterexample_batch, put_counterexample_batch, - "Exhaustive_Generators.put_counterexample_batch") - ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) - (HOLogic.mk_list @{typ "natural => term list option"} ts') [] + val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts + val compiles = + Code_Runtime.dynamic_value_strict + (get_counterexample_batch, put_counterexample_batch, + "Exhaustive_Generators.put_counterexample_batch") + ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) + (HOLogic.mk_list @{typ "natural => term list option"} ts') [] in - map (fn compile => fn size => compile size - |> (Option.map o map) Quickcheck_Common.post_process_term) compiles - end; + map (fn compile => fn size => + compile size |> (Option.map o map) Quickcheck_Common.post_process_term) compiles + end fun compile_generator_exprs ctxt ts = compile_generator_exprs_raw ctxt ts - |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)); + |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) fun compile_validator_exprs_raw ctxt ts = - let - val ts' = map (mk_validator_expr ctxt) ts - in + let val ts' = map (mk_validator_expr ctxt) ts in Code_Runtime.dynamic_value_strict (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch") - ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') [] - end; + ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural \ bool"} ts') [] + end fun compile_validator_exprs ctxt ts = compile_validator_exprs_raw ctxt ts - |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)); + |> map (fn f => fn size => f (Code_Numeral.natural_of_integer size)) fun size_matters_for thy Ts = not (forall (fn T => Sign.of_sort thy (T, @{sort check_all})) Ts) val test_goals = - Quickcheck_Common.generator_test_goal_terms ("exhaustive", (size_matters_for, compile_generator_expr)); - + Quickcheck_Common.generator_test_goal_terms + ("exhaustive", (size_matters_for, compile_generator_expr)) + + (* setup *) val setup_exhaustive_datatype_interpretation = @@ -540,7 +545,7 @@ (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs, instantiate_bounded_forall_datatype))) -val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); +val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true) val _ = Theory.setup @@ -548,6 +553,6 @@ (@{sort full_exhaustive}, instantiate_full_exhaustive_datatype) #> Context.theory_map (Quickcheck.add_tester ("exhaustive", (active, test_goals))) #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)) - #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs))); + #> Context.theory_map (Quickcheck.add_batch_validator ("exhaustive", compile_validator_exprs))) -end; +end diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Apr 15 16:50:23 2016 +0200 @@ -15,8 +15,9 @@ | Existential_Counterexample of (term * counterexample) list | Empty_Assignment val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context - val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context -end; + val put_existential_counterexample : (unit -> counterexample option) -> + Proof.context -> Proof.context +end structure Narrowing_Generators : NARROWING_GENERATORS = struct @@ -28,26 +29,29 @@ val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false) val ghc_options = Attrib.setup_config_string @{binding quickcheck_narrowing_ghc_options} (K "") + (* partial_term_of instances *) fun mk_partial_term_of (x, T) = Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of}, - Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) - $ Logic.mk_type T $ x + Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $ Logic.mk_type T $ x + (** formal definition **) fun add_partial_term_of tyco raw_vs thy = let - val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; - val ty = Type (tyco, map TFree vs); - val lhs = Const (@{const_name partial_term_of}, - Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) - $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term}); - val rhs = @{term "undefined :: Code_Evaluation.term"}; - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst - o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; + val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs + val ty = Type (tyco, map TFree vs) + val lhs = + Const (@{const_name partial_term_of}, + Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) $ + Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term}) + val rhs = @{term "undefined :: Code_Evaluation.term"} + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) + fun triv_name_of t = + (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ + "_triv" in thy |> Class.instantiation ([tyco], vs, @{sort partial_term_of}) @@ -55,13 +59,13 @@ |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) |> snd |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) - end; + end fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = let val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}) - andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; - in if need_inst then add_partial_term_of tyco raw_vs thy else thy end; + andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep} + in if need_inst then add_partial_term_of tyco raw_vs thy else thy end (** code equations for datatypes **) @@ -69,15 +73,17 @@ fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = let val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys)) - val narrowing_term = @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i - $ HOLogic.mk_list @{typ narrowing_term} (rev frees) - val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) + val narrowing_term = + @{term Quickcheck_Narrowing.Narrowing_constructor} $ HOLogic.mk_number @{typ integer} i $ + HOLogic.mk_list @{typ narrowing_term} (rev frees) + val rhs = + fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) (map mk_partial_term_of (frees ~~ tys)) (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) val insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), narrowing_term, rhs] - val cty = Thm.global_ctyp_of thy ty; + val cty = Thm.global_ctyp_of thy ty in @{thm partial_term_of_anything} |> Thm.instantiate' [SOME cty] insts @@ -86,44 +92,42 @@ fun add_partial_term_of_code tyco raw_vs raw_cs thy = let - val algebra = Sign.classes_of thy; - val vs = map (fn (v, sort) => - (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; - val ty = Type (tyco, map TFree vs); - val cs = (map o apsnd o apsnd o map o map_atyps) - (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco); + val algebra = Sign.classes_of thy + val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs + val ty = Type (tyco, map TFree vs) + val cs = + (map o apsnd o apsnd o map o map_atyps) + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs + val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco) val var_insts = map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"}, - @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]; + @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty] val var_eq = @{thm partial_term_of_anything} |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |> Thm.varifyT_global - val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs; - in + val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs + in thy |> Code.del_eqns const |> fold Code.add_eqn eqs - end; + end fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = - let - val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of}; - in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end; + let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of} + in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end (* narrowing generators *) (** narrowing specific names and types **) -exception FUNCTION_TYPE; +exception FUNCTION_TYPE -val narrowingN = "narrowing"; +val narrowingN = "narrowing" -fun narrowingT T = - @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T]) +fun narrowingT T = @{typ integer} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T]) fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T) @@ -136,11 +140,9 @@ end fun mk_sum (t, u) = - let - val T = fastype_of t - in - Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u - end + let val T = fastype_of t + in Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u end + (** deriving narrowing instances **) @@ -156,8 +158,7 @@ (T, nth narrowings k) end fun mk_consexpr simpleT (c, xs) = - let - val Ts = map fst xs + let val Ts = map fst xs in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end fun mk_rhs exprs = foldr1 mk_sum exprs val rhss = @@ -168,9 +169,7 @@ |> map mk_rhs val lhss = narrowings val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss) - in - eqs - end + in eqs end fun contains_recursive_type_under_function_types xs = exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT => @@ -178,8 +177,8 @@ fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let - val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..."; - val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames); + val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..." + val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames) in if not (contains_recursive_type_under_function_types descr) then thy @@ -188,14 +187,15 @@ (fn narrowings => mk_equations descr vs narrowings, NONE) prfx [] narrowingsN (map narrowingT (Ts @ Us)) |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) - else - thy - end; + else thy + end + (* testing framework *) val target = "Haskell_Quickcheck" + (** invocation of Haskell interpreter **) val narrowing_engine = @@ -213,14 +213,15 @@ let val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) - val _ = Isabelle_System.mkdirs path; - in Exn.release (Exn.capture f path) end; + val _ = Isabelle_System.mkdirs path + in Exn.release (Exn.capture f path) end fun elapsed_time description e = let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) + ctxt cookie (code_modules, _) = let val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie fun message s = if quiet then () else writeln s @@ -235,26 +236,33 @@ let fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs")) val generatedN = Code_Target.generatedN - val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file; + val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file val code = the (AList.lookup (op =) code_modules generatedN) val code_file = mk_code_file generatedN val narrowing_engine_file = mk_code_file "Narrowing_Engine" val main_file = mk_code_file "Main" - val main = "module Main where {\n\n" ^ + val main = + "module Main where {\n\n" ^ "import System.IO;\n" ^ "import System.Environment;\n" ^ "import Narrowing_Engine;\n" ^ "import " ^ generatedN ^ " ;\n\n" ^ "main = getArgs >>= \\[potential, size] -> " ^ - "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^ - "}\n" - val _ = map (uncurry File.write) (includes @ - [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine), - (code_file, code), (main_file, main)]) - val executable = File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")) - val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ - ghc_options ^ " " ^ - (space_implode " " (map File.bash_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ + "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ + ".value ())\n\n}\n" + val _ = + map (uncurry File.write) + (includes @ + [(narrowing_engine_file, + if contains_existentials then pnf_narrowing_engine else narrowing_engine), + (code_file, code), (main_file, main)]) + val executable = + File.bash_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing")) + val cmd = + "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^ + (space_implode " " + (map File.bash_path + (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ executable ^ ";" val (_, compilation_time) = elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) @@ -262,52 +270,49 @@ fun haskell_string_of_bool v = if v then "True" else "False" val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else () fun with_size genuine_only k = - if k > size then - (NONE, !current_result) + if k > size then (NONE, !current_result) else let val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k - val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) - (fn () => Isabelle_System.bash_output - (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k)) + val ((response, _), timing) = + elapsed_time ("execution of size " ^ string_of_int k) + (fn () => Isabelle_System.bash_output + (executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^ string_of_int k)) val _ = Quickcheck.add_timing timing current_result in - if response = "NONE\n" then - with_size genuine_only (k + 1) + if response = "NONE\n" then with_size genuine_only (k + 1) else let val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response) val ml_code = "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml - ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"; + ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))" val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) - |> Context.proof_map (exec false ml_code); + |> Context.proof_map (exec false ml_code) val counterexample = get ctxt' () in if is_genuine counterexample then (counterexample, !current_result) else let - val cex = Option.map (rpair []) (counterexample_of counterexample); - val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - val _ = message "Quickcheck continues to find a genuine counterexample..."; + val cex = Option.map (rpair []) (counterexample_of counterexample) + val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)) + val _ = message "Quickcheck continues to find a genuine counterexample..." in with_size true (k + 1) end end end in with_size genuine_only 0 end - in - with_tmp_dir tmp_prefix run - end; + in with_tmp_dir tmp_prefix run end fun dynamic_value_strict opts cookie ctxt postproc t = let fun evaluator program _ vs_ty_t deps = Exn.interruptible_capture (value opts ctxt cookie) - (Code_Target.evaluator ctxt target program deps true vs_ty_t); - in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end; + (Code_Target.evaluator ctxt target program deps true vs_ty_t) + in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end (** counterexample generator **) @@ -317,7 +322,7 @@ | Existential_Counterexample of (term * counterexample) list | Empty_Assignment -fun map_counterexample f Empty_Assignment = Empty_Assignment +fun map_counterexample _ Empty_Assignment = Empty_Assignment | map_counterexample f (Universal_Counterexample (t, c)) = Universal_Counterexample (f t, map_counterexample f c) | map_counterexample f (Existential_Counterexample cs) = @@ -327,18 +332,18 @@ ( type T = (unit -> (bool * term list) option) * - (unit -> counterexample option); + (unit -> counterexample option) val empty: T = (fn () => raise Fail "counterexample", - fn () => raise Fail "existential_counterexample"); - fun init _ = empty; -); + fn () => raise Fail "existential_counterexample") + fun init _ = empty +) val get_counterexample = #1 o Data.get; val get_existential_counterexample = #2 o Data.get; -val put_counterexample = Data.map o @{apply 2(1)} o K; -val put_existential_counterexample = Data.map o @{apply 2(2)} o K; +val put_counterexample = Data.map o @{apply 2(1)} o K +val put_existential_counterexample = Data.map o @{apply 2(2)} o K fun finitize_functions (xTs, t) = let @@ -350,27 +355,27 @@ Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT) fun eval_function (Type (@{type_name fun}, [dT, rT])) = - let - val (rt', rT') = eval_function rT - in - case dT of - Type (@{type_name fun}, _) => - (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), - Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT'])) - | _ => - (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), - Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])) - end + let + val (rt', rT') = eval_function rT + in + (case dT of + Type (@{type_name fun}, _) => + (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), + Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT'])) + | _ => + (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), + Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))) + end | eval_function (T as Type (@{type_name prod}, [fT, sT])) = - let - val (ft', fT') = eval_function fT - val (st', sT') = eval_function sT - val T' = Type (@{type_name prod}, [fT', sT']) - val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T) - fun apply_dummy T t = absdummy T (t (Bound 0)) - in - (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') - end + let + val (ft', fT') = eval_function fT + val (st', sT') = eval_function sT + val T' = Type (@{type_name prod}, [fT', sT']) + val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T) + fun apply_dummy T t = absdummy T (t (Bound 0)) + in + (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') + end | eval_function T = (I, T) val (tt, boundTs') = split_list (map eval_function boundTs) val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t) @@ -381,63 +386,63 @@ fun dest_ffun (Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT])) = (dT, rT) fun eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Constant"}, T) $ value) = - absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) + absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value) | eval_finite_functions (Const (@{const_name "Quickcheck_Narrowing.ffun.Update"}, T) $ a $ b $ f) = - let - val (T1, T2) = dest_ffun (body_type T) - in - Quickcheck_Common.mk_fun_upd T1 T2 - (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) - end + let + val (T1, T2) = dest_ffun (body_type T) + in + Quickcheck_Common.mk_fun_upd T1 T2 + (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f) + end | eval_finite_functions t = t + (** tester **) val rewrs = - map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) - (@{thms all_simps} @ @{thms ex_simps}) - @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) - [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}, - @{thm meta_eq_to_obj_eq [OF Ex1_def]}] + map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) + (@{thms all_simps} @ @{thms ex_simps}) @ + map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) + [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all}, + @{thm meta_eq_to_obj_eq [OF Ex1_def]}] fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = - apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t) + apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t) | strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) = - apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t) + apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t) | strip_quantifiers t = ([], t) -fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t)) +fun contains_existentials t = + exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t)) fun mk_property qs t = let fun enclose (@{const_name Ex}, (x, T)) t = - Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property}) - $ Abs (x, T, t) + Const (@{const_name Quickcheck_Narrowing.exists}, + (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t) | enclose (@{const_name All}, (x, T)) t = - Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property}) - $ Abs (x, T, t) - in - fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) - end + Const (@{const_name Quickcheck_Narrowing.all}, + (T --> @{typ property}) --> @{typ property}) $ Abs (x, T, t) + in fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) end fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = - Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) => - (t, mk_case_term ctxt (p - 1) qs' c)) cs) + Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) => + (t, mk_case_term ctxt (p - 1) qs' c)) cs) | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) = - if p = 0 then t else mk_case_term ctxt (p - 1) qs' c + if p = 0 then t else mk_case_term ctxt (p - 1) qs' c -val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions +val post_process = + perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions fun mk_terms ctxt qs result = let - val - ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs) - in - map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps - |> map (apsnd post_process) - end + val ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs) + in + map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps + |> map (apsnd post_process) + end fun test_term ctxt catch_code_errors (t, _) = let @@ -453,8 +458,8 @@ if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then let fun wrap f (qs, t) = - let val (qs1, qs2) = split_list qs in - apfst (map2 pair qs1) (f (qs2, t)) end + let val (qs1, qs2) = split_list qs + in apfst (map2 pair qs1) (f (qs2, t)) end val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I val (qs, prop_t) = finitize (strip_quantifiers pnf_t) val act = if catch_code_errors then try else (fn f => SOME o f) @@ -465,14 +470,14 @@ "Narrowing_Generators.put_existential_counterexample")) ctxt (apfst o Option.map o map_counterexample) in - case act execute (mk_property qs prop_t) of + (case act execute (mk_property qs prop_t) of SOME (counterexample, result) => Quickcheck.Result {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample, evaluation_terms = Option.map (K []) counterexample, timings = #timings (dest_result result), reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; - Quickcheck.empty_result) + Quickcheck.empty_result)) end else let @@ -481,10 +486,12 @@ fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t)) val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I fun ensure_testable t = - Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t + Const (@{const_name Quickcheck_Narrowing.ensure_testable}, + fastype_of t --> fastype_of t) $ t fun is_genuine (SOME (true, _)) = true | is_genuine _ = false - val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process)) + val counterexample_of = + Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process)) val act = if catch_code_errors then try else (fn f => SOME o f) val execute = dynamic_value_strict (false, opts) @@ -493,7 +500,7 @@ "Narrowing_Generators.put_counterexample")) ctxt (apfst o Option.map o apsnd o map) in - case act execute (ensure_testable (finitize t')) of + (case act execute (ensure_testable (finitize t')) of SOME (counterexample, result) => Quickcheck.Result {counterexample = counterexample_of counterexample, @@ -502,14 +509,14 @@ reports = #reports (dest_result result)} | NONE => (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing"; - Quickcheck.empty_result) + Quickcheck.empty_result)) end - end; + end fun test_goals ctxt catch_code_errors insts goals = - if (not (getenv "ISABELLE_GHC" = "")) then + if not (getenv "ISABELLE_GHC" = "") then let - val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..."; + val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..." val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals in Quickcheck_Common.collect_results (test_term ctxt catch_code_errors) @@ -522,9 +529,10 @@ ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false."); [Quickcheck.empty_result]) + (* setup *) -val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false); +val active = Attrib.setup_config_bool @{binding quickcheck_narrowing_active} (K false) val _ = Theory.setup @@ -532,6 +540,6 @@ #> Code.datatype_interpretation ensure_partial_term_of_code #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing} (@{sort narrowing}, instantiate_narrowing_datatype) - #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))); + #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals)))) -end; +end diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Fri Apr 15 16:50:23 2016 +0200 @@ -10,37 +10,39 @@ val strip_imp : term -> (term list * term) val reflect_bool : bool -> term val define_functions : ((term list -> term list) * (Proof.context -> tactic) option) - -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context + -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list -> (string * sort -> string * sort) option val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list -> (typ option * (term * term list)) list list val register_predicate : term * string -> Context.generic -> Context.generic val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term - val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list + val collect_results : ('a -> Quickcheck.result) -> 'a list -> + Quickcheck.result list -> Quickcheck.result list type result = (bool * term list) option * Quickcheck.report option - type generator = string * ((theory -> typ list -> bool) * + type generator = string * ((theory -> typ list -> bool) * (Proof.context -> (term * term list) list -> bool -> int list -> result)) val generator_test_goal_terms : generator -> Proof.context -> bool -> (string * typ) list -> (term * term list) list -> Quickcheck.result list - type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list - -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory + type instantiation = + Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list -> + string list -> string -> string list * string list -> typ list * typ list -> theory -> theory val ensure_sort : (((sort * sort) * sort) * ((theory -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list - * string * (string list * string list) * (typ list * typ list)) * instantiation)) - -> Old_Datatype_Aux.config -> string list -> theory -> theory - val ensure_common_sort_datatype : - (sort * instantiation) -> Old_Datatype_Aux.config -> string list -> theory -> theory + * string * (string list * string list) * (typ list * typ list)) * instantiation)) -> + Old_Datatype_Aux.config -> string list -> theory -> theory + val ensure_common_sort_datatype : (sort * instantiation) -> Old_Datatype_Aux.config -> + string list -> theory -> theory val datatype_interpretation : string -> sort * instantiation -> theory -> theory val gen_mk_parametric_generator_expr : - (((Proof.context -> term * term list -> term) * term) * typ) - -> Proof.context -> (term * term list) list -> term + (((Proof.context -> term * term list -> term) * term) * typ) -> + Proof.context -> (term * term list) list -> term val mk_fun_upd : typ -> typ -> term * term -> term -> term val post_process_term : term -> term val test_term : generator -> Proof.context -> bool -> term * term list -> Quickcheck.result -end; +end structure Quickcheck_Common : QUICKCHECK_COMMON = struct @@ -51,27 +53,32 @@ val define_foundationally = false + (* HOLogic's term functions *) -fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B) +fun strip_imp (Const(@{const_name HOL.implies}, _) $ A $ B) = apfst (cons A) (strip_imp B) | strip_imp A = ([], A) -fun reflect_bool b = if b then @{term "True"} else @{term "False"} +fun reflect_bool b = if b then @{term True} else @{term False} -fun mk_undefined T = Const(@{const_name undefined}, T) +fun mk_undefined T = Const (@{const_name undefined}, T) + (* testing functions: testing with increasing sizes (and cardinalities) *) type result = (bool * term list) option * Quickcheck.report option -type generator = string * ((theory -> typ list -> bool) * - (Proof.context -> (term * term list) list -> bool -> int list -> result)) +type generator = + string * ((theory -> typ list -> bool) * + (Proof.context -> (term * term list) list -> bool -> int list -> result)) fun check_test_term t = let - val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse - error "Term to be tested contains type variables"; - val _ = null (Term.add_vars t []) orelse - error "Term to be tested contains schematic variables"; + val _ = + (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse + error "Term to be tested contains type variables" + val _ = + null (Term.add_vars t []) orelse + error "Term to be tested contains schematic variables" in () end fun cpu_time description e = @@ -85,55 +92,59 @@ val _ = check_test_term t val names = Term.add_free_names t [] val current_size = Unsynchronized.ref 0 - val current_result = Unsynchronized.ref Quickcheck.empty_result - val act = if catch_code_errors then try else (fn f => SOME o f) - val (test_fun, comp_time) = cpu_time "quickcheck compilation" - (fn () => act (compile ctxt) [(t, eval_terms)]); + val current_result = Unsynchronized.ref Quickcheck.empty_result + val act = if catch_code_errors then try else (fn f => SOME o f) + val (test_fun, comp_time) = + cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)]) val _ = Quickcheck.add_timing comp_time current_result fun with_size test_fun genuine_only k = - if k > Config.get ctxt Quickcheck.size then - NONE + if k > Config.get ctxt Quickcheck.size then NONE else let - val _ = Quickcheck.verbose_message ctxt - ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k) + val _ = + Quickcheck.verbose_message ctxt + ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k) val _ = current_size := k val ((result, report), time) = cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1]) - val _ = if Config.get ctxt Quickcheck.timing then - Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else () + val _ = + if Config.get ctxt Quickcheck.timing then + Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") + else () val _ = Quickcheck.add_timing time current_result val _ = Quickcheck.add_report k report current_result in - case result of + (case result of NONE => with_size test_fun genuine_only (k + 1) | SOME (true, ts) => SOME (true, ts) | SOME (false, ts) => - if abort_potential then SOME (false, ts) - else - let - val (ts1, ts2) = chop (length names) ts - val (eval_terms', _) = chop (length ts2) eval_terms - val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) - in - (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; - with_size test_fun true k) - end - end; + if abort_potential then SOME (false, ts) + else + let + val (ts1, ts2) = chop (length names) ts + val (eval_terms', _) = chop (length ts2) eval_terms + val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) + in + Quickcheck.message ctxt + (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); + Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; + with_size test_fun true k + end) + end in case test_fun of - NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); - !current_result) + NONE => + (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); + !current_result) | SOME test_fun => - let - val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "..."); - val (response, exec_time) = - cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1) - val _ = Quickcheck.add_response names eval_terms response current_result - val _ = Quickcheck.add_timing exec_time current_result - in !current_result end - end; + let + val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...") + val (response, exec_time) = + cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1) + val _ = Quickcheck.add_response names eval_terms response current_result + val _ = Quickcheck.add_timing exec_time current_result + in !current_result end + end fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts = let @@ -145,105 +156,102 @@ val names = Term.add_free_names (hd ts') [] val Ts = map snd (Term.add_frees (hd ts') []) val current_result = Unsynchronized.ref Quickcheck.empty_result - fun test_card_size test_fun genuine_only (card, size) = - (* FIXME: why decrement size by one? *) + fun test_card_size test_fun genuine_only (card, size) = (* FIXME: why decrement size by one? *) let val _ = Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^ (if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^ - "cardinality: " ^ string_of_int card) + "cardinality: " ^ string_of_int card) val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) (fn () => fst (test_fun genuine_only [card, size + 1])) val _ = Quickcheck.add_timing timing current_result - in - Option.map (pair (card, size)) ts - end + in Option.map (pair (card, size)) ts end val enumeration_card_size = if size_matters_for thy Ts then map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) - else - map (rpair 0) (1 upto (length ts)) + else map (rpair 0) (1 upto (length ts)) val act = if catch_code_errors then try else (fn f => SOME o f) val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts) val _ = Quickcheck.add_timing comp_time current_result in - case test_fun of - NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); - !current_result) + (case test_fun of + NONE => + (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); + !current_result) | SOME test_fun => - let - val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "..."); - fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of - SOME ((card, _), (true, ts)) => - Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result - | SOME ((card, size), (false, ts)) => - if abort_potential then - Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (false, ts)) current_result - else - let - val (ts1, ts2) = chop (length names) ts - val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1)) - val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) - in - (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); - Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample..."; - test true (snd (take_prefix (fn x => not (x = (card, size))) enum))) - end - | NONE => () - in (test genuine_only enumeration_card_size; !current_result) end + let + val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...") + fun test genuine_only enum = + (case get_first (test_card_size test_fun genuine_only) enum of + SOME ((card, _), (true, ts)) => + Quickcheck.add_response names (nth eval_terms (card - 1)) + (SOME (true, ts)) current_result + | SOME ((card, size), (false, ts)) => + if abort_potential then + Quickcheck.add_response names (nth eval_terms (card - 1)) + (SOME (false, ts)) current_result + else + let + val (ts1, ts2) = chop (length names) ts + val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1)) + val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2) + in + Quickcheck.message ctxt + (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex)); + Quickcheck.message ctxt + "Quickcheck continues to find a genuine counterexample..."; + test true (snd (take_prefix (fn x => not (x = (card, size))) enum)) + end + | NONE => ()) + in (test genuine_only enumeration_card_size; !current_result) end) end fun get_finite_types ctxt = fst (chop (Config.get ctxt Quickcheck.finite_type_size) - [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"}, - @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}]) + [@{typ Enum.finite_1}, @{typ Enum.finite_2}, @{typ Enum.finite_3}, + @{typ Enum.finite_4}, @{typ Enum.finite_5}]) exception WELLSORTED of string -fun monomorphic_term thy insts default_T = - let - fun subst (T as TFree (v, S)) = - let - val T' = AList.lookup (op =) insts v - |> the_default default_T - in if Sign.of_sort thy (T', S) then T' - else raise (WELLSORTED ("For instantiation with default_type " ^ - Syntax.string_of_typ_global thy default_T ^ - ":\n" ^ Syntax.string_of_typ_global thy T' ^ - " to be substituted for variable " ^ - Syntax.string_of_typ_global thy T ^ " does not have sort " ^ - Syntax.string_of_sort_global thy S)) - end - | subst T = T; - in (map_types o map_atyps) subst end; +fun monomorphic_term ctxt insts default_T = + (map_types o map_atyps) + (fn T as TFree (v, S) => + let val T' = AList.lookup (op =) insts v |> the_default default_T in + if Sign.of_sort (Proof_Context.theory_of ctxt) (T', S) then T' + else + raise WELLSORTED ("For instantiation with default_type " ^ + Syntax.string_of_typ ctxt default_T ^ ":\n" ^ Syntax.string_of_typ ctxt T' ^ + " to be substituted for variable " ^ Syntax.string_of_typ ctxt T ^ + " does not have sort " ^ Syntax.string_of_sort ctxt S) + end + | T => T) datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list + (* minimalistic preprocessing *) -fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = - let - val (a', t') = strip_all t - in ((a, T) :: a', t') end - | strip_all t = ([], t); +fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = + let val (a', t') = strip_all t + in ((a, T) :: a', t') end + | strip_all t = ([], t) fun preprocess ctxt t = let val thy = Proof_Context.theory_of ctxt val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of - val rewrs = map (swap o dest) @{thms all_simps} @ - (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}, - @{thm bot_fun_def}, @{thm less_bool_def}]) + val rewrs = + map (swap o dest) @{thms all_simps} @ + (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}, + @{thm bot_fun_def}, @{thm less_bool_def}]) val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t) val (vs, body) = strip_all t' val vs' = Variable.variant_frees ctxt [t'] vs - in - subst_bounds (map Free (rev vs'), body) - end + in subst_bounds (map Free (rev vs'), body) end - + structure Subtype_Predicates = Generic_Data ( type T = (term * string) list @@ -257,99 +265,92 @@ fun subtype_preprocess ctxt (T, (t, ts)) = let val preds = Subtype_Predicates.get (Context.Proof ctxt) - fun matches (p $ _) = AList.defined Term.could_unify preds p + fun matches (p $ _) = AList.defined Term.could_unify preds p fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p) fun subst_of (tyco, v as Free (x, repT)) = let val [(info, _)] = Typedef.get_info ctxt tyco val repT' = Logic.varifyT_global (#rep_type info) - val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty + val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info)) in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end val (prems, concl) = strip_imp t val subst = map subst_of (map_filter get_match prems) val t' = Term.subst_free subst (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl) - in - (T, (t', ts)) - end + in (T, (t', ts)) end + (* instantiation of type variables with concrete types *) - -fun instantiate_goals lthy insts goals = + +fun instantiate_goals ctxt insts goals = let fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) - val thy = Proof_Context.theory_of lthy val default_insts = - if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type + if Config.get ctxt Quickcheck.finite_types + then get_finite_types else Quickcheck.default_type val inst_goals = map (fn (check_goal, eval_terms) => if not (null (Term.add_tfree_names check_goal [])) then map (fn T => - (pair (SOME T) o Term o apfst (preprocess lthy)) - (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) - handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) - else - [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals + (pair (SOME T) o Term o apfst (preprocess ctxt)) + (map_goal_and_eval_terms (monomorphic_term ctxt insts T) (check_goal, eval_terms)) + handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts ctxt) + else [(NONE, Term (preprocess ctxt check_goal, eval_terms))]) goals val error_msg = cat_lines (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) fun is_wellsorted_term (T, Term t) = SOME (T, t) | is_wellsorted_term (_, Wellsorted_Error _) = NONE val correct_inst_goals = - case map (map_filter is_wellsorted_term) inst_goals of + (case map (map_filter is_wellsorted_term) inst_goals of [[]] => error error_msg - | xs => xs - val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg - in - correct_inst_goals - end + | xs => xs) + val _ = if Config.get ctxt Quickcheck.quiet then () else warning error_msg + in correct_inst_goals end + (* compilation of testing functions *) fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine = let val T = fastype_of then_t - val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) + val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T) in - Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ + Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $ (if_t $ cond $ then_t $ else_t genuine) $ (if_t $ genuine_only $ none $ else_t false) end -fun collect_results f [] results = results +fun collect_results _ [] results = results | collect_results f (t :: ts) results = - let - val result = f t - in - if Quickcheck.found_counterexample result then - (result :: results) - else - collect_results f ts (result :: results) - end + let val result = f t in + if Quickcheck.found_counterexample result then result :: results + else collect_results f ts (result :: results) + end fun generator_test_goal_terms generator ctxt catch_code_errors insts goals = let val use_subtype = Config.get ctxt Quickcheck.use_subtype fun add_eval_term t ts = if is_Free t then ts else ts @ [t] fun add_equation_eval_terms (t, eval_terms) = - case try HOLogic.dest_eq (snd (strip_imp t)) of + (case try HOLogic.dest_eq (snd (strip_imp t)) of SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms)) - | NONE => (t, eval_terms) + | NONE => (t, eval_terms)) fun test_term' goal = - case goal of + (case goal of [(NONE, t)] => test_term generator ctxt catch_code_errors t - | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts) - val goals' = instantiate_goals ctxt insts goals + | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)) + val goals' = + instantiate_goals ctxt insts goals |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I) |> map (map (apsnd add_equation_eval_terms)) in if Config.get ctxt Quickcheck.finite_types then collect_results test_term' goals' [] - else - collect_results (test_term generator ctxt catch_code_errors) - (maps (map snd) goals') [] - end; + else collect_results (test_term generator ctxt catch_code_errors) (maps (map snd) goals') [] + end + (* defining functions *) @@ -388,38 +389,42 @@ (names ~~ eqs) lthy end) + (** ensuring sort constraints **) -type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list - -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory +type instantiation = + Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list -> + string list -> string -> string list * string list -> typ list * typ list -> theory -> theory fun perhaps_constrain thy insts raw_vs = let - fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) - (Logic.varifyT_global T, sort); + fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT_global T, sort) val vtab = Vartab.empty |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs - |> fold meet insts; - in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) - end handle Sorts.CLASS_ERROR _ => NONE; + |> fold meet insts + in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end + handle Sorts.CLASS_ERROR _ => NONE fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy = let - val algebra = Sign.classes_of thy; + val algebra = Sign.classes_of thy val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd) (Old_Datatype_Aux.interpret_construction descr vs constr) val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] } @ insts_of aux_sort { atyp = K [], dtyp = K o K } - val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos; - in if has_inst then thy - else case perhaps_constrain thy insts vs - of SOME constrain => instantiate config descr - (map constrain vs) tycos prfx (names, auxnames) - ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy - | NONE => thy - end; + val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos + in + if has_inst then thy + else + (case perhaps_constrain thy insts vs of + SOME constrain => + instantiate config descr + (map constrain vs) tycos prfx (names, auxnames) + ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy + | NONE => thy) + end fun ensure_common_sort_datatype (sort, instantiate) = ensure_sort (((@{sort typerep}, @{sort term_of}), sort), @@ -427,86 +432,89 @@ fun datatype_interpretation name = BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype - + + (** generic parametric compilation **) fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts = let - val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) - fun mk_if (index, (t, eval_terms)) else_t = if_t $ - (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $ + val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T) + fun mk_if (index, (t, eval_terms)) else_t = + if_t $ (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $ (mk_generator_expr ctxt (t, eval_terms)) $ else_t - in - absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) - end + in absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) end + (** post-processing of function terms **) fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2)) | dest_fun_upd t = raise TERM ("dest_fun_upd", [t]) -fun mk_fun_upd T1 T2 (t1, t2) t = +fun mk_fun_upd T1 T2 (t1, t2) t = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2 fun dest_fun_upds t = - case try dest_fun_upd t of + (case try dest_fun_upd t of NONE => (case t of - Abs (_, _, _) => ([], t) + Abs (_, _, _) => ([], t) | _ => raise TERM ("dest_fun_upds", [t])) - | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0) + | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)) fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps | make_set T1 ((t1, @{const True}) :: tps) = - Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) - $ t1 $ (make_set T1 tps) + Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $ + t1 $ (make_set T1 tps) | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t]) fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) - | make_coset T tps = + | make_coset T tps = let val U = T --> @{typ bool} fun invert @{const False} = @{const True} | invert @{const True} = @{const False} in - Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) - $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) + Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) $ + Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps) end fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2) | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps) - + fun post_process_term t = let fun map_Abs f t = - case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) - fun process_args t = case strip_comb t of - (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) + (case t of + Abs (x, T, t') => Abs (x, T, f t') + | _ => raise TERM ("map_Abs", [t])) + fun process_args t = + (case strip_comb t of + (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)) in - case fastype_of t of + (case fastype_of t of Type (@{type_name fun}, [T1, T2]) => (case try dest_fun_upds t of SOME (tps, t) => - (map (apply2 post_process_term) tps, map_Abs post_process_term t) - |> (case T2 of - @{typ bool} => - (case t of - Abs(_, _, @{const False}) => fst #> rev #> make_set T1 - | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1 - | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 - | _ => raise TERM ("post_process_term", [t])) - | Type (@{type_name option}, _) => - (case t of - Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2 - | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 - | _ => make_fun_upds T1 T2) - | _ => make_fun_upds T1 T2) + (map (apply2 post_process_term) tps, map_Abs post_process_term t) |> + (case T2 of + @{typ bool} => + (case t of + Abs(_, _, @{const False}) => fst #> rev #> make_set T1 + | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1 + | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1 + | _ => raise TERM ("post_process_term", [t])) + | Type (@{type_name option}, _) => + (case t of + Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2 + | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2 + | _ => make_fun_upds T1 T2) + | _ => make_fun_upds T1 T2) | NONE => process_args t) - | _ => process_args t + | _ => process_args t) end -end; +end diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Apr 15 16:50:23 2016 +0200 @@ -7,17 +7,19 @@ signature RANDOM_GENERATORS = sig type seed = Random_Engine.seed - val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) - -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) - -> seed -> (('a -> 'b) * (unit -> term)) * seed - val compile_generator_expr: - Proof.context -> (term * term list) list -> bool -> int list -> (bool * term list) option * Quickcheck.report option - val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed) - -> Proof.context -> Proof.context - val put_counterexample_report: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed) - -> Proof.context -> Proof.context + val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) -> + (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) -> + seed -> (('a -> 'b) * (unit -> term)) * seed + val compile_generator_expr: Proof.context -> (term * term list) list -> bool -> int list -> + (bool * term list) option * Quickcheck.report option + val put_counterexample: (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> + seed -> (bool * term list) option * seed) -> Proof.context -> Proof.context + val put_counterexample_report: (unit -> Code_Numeral.natural -> bool -> + Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed) -> + Proof.context -> Proof.context val instantiate_random_datatype : Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> - (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory + (string * sort) list -> string list -> string -> string list * string list -> + typ list * typ list -> theory -> theory end; structure Random_Generators : RANDOM_GENERATORS = @@ -25,22 +27,22 @@ (** abstract syntax **) -fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"}) +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \ term"}) val size = @{term "i::natural"}; val size_pred = @{term "(i::natural) - 1"}; val size' = @{term "j::natural"}; val seed = @{term "s::Random.seed"}; -val resultT = @{typ "(bool * term list) option"}; +val resultT = @{typ "(bool \ term list) option"}; -(** typ "'a => 'b" **) + +(** typ "'a \ 'b" **) type seed = Random_Engine.seed; fun random_fun T1 T2 eq term_of random random_split seed = let - val fun_upd = Const (@{const_name fun_upd}, - (T1 --> T2) --> T1 --> T2 --> T1 --> T2); + val fun_upd = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2); val ((_, t2), seed') = random seed; val (seed'', seed''') = random_split seed'; @@ -474,6 +476,7 @@ val test_goals = Quickcheck_Common.generator_test_goal_terms ("random", (size_matters_for, compile_generator_expr)); + (** setup **) diff -r 2e874d9aca43 -r 19a19ee36daa src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/HOL/Tools/try0.ML Fri Apr 15 16:50:23 2016 +0200 @@ -108,6 +108,7 @@ Config.put Metis_Tactic.verbose debug #> not debug ? (fn ctxt => ctxt + |> Simplifier_Trace.disable |> Context_Position.set_visible false |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound) |> Proof_Context.background_theory (fn thy => diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/General/name_space.ML Fri Apr 15 16:50:23 2016 +0200 @@ -13,6 +13,7 @@ val empty: string -> T val kind_of: T -> string val markup: T -> string -> Markup.T + val markup_def: T -> string -> Markup.T val the_entry: T -> string -> {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial} val entry_ord: T -> string * string -> order @@ -156,10 +157,13 @@ fun kind_of (Name_Space {kind, ...}) = kind; -fun markup (Name_Space {kind, entries, ...}) name = +fun gen_markup def (Name_Space {kind, entries, ...}) name = (case Change_Table.lookup entries name of NONE => Markup.intensify - | SOME (_, entry) => entry_markup false kind (name, entry)); + | SOME (_, entry) => entry_markup def kind (name, entry)); + +val markup = gen_markup false; +val markup_def = gen_markup true; fun undefined (space as Name_Space {kind, entries, ...}) bad = let diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/General/output_primitives_virtual.ML --- a/src/Pure/General/output_primitives_virtual.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/General/output_primitives_virtual.ML Fri Apr 15 16:50:23 2016 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/General/output_primitives.ML +(* Title: Pure/General/output_primitives_virtual.ML Author: Makarius Primitives for Isabelle output channels -- virtual version within Pure environment. diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Isar/generic_target.ML Fri Apr 15 16:50:23 2016 +0200 @@ -327,7 +327,9 @@ lthy |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd + |> Context_Position.set_visible false |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) + ||> Context_Position.restore_visible lthy end; diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Isar/local_defs.ML Fri Apr 15 16:50:23 2016 +0200 @@ -90,7 +90,7 @@ let val ((xs, mxs), specs) = defs |> split_list |>> split_list; val (bs, rhss) = specs |> split_list; - val eqs = mk_def ctxt (xs ~~ rhss); + val eqs = mk_def (Context_Position.set_visible false ctxt) (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; in ctxt diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Isar/proof.ML Fri Apr 15 16:50:23 2016 +0200 @@ -740,7 +740,7 @@ #-> (fn rhss => let val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) => - ((x, mx), ((Thm.def_binding_optional x a, atts), rhs))); + ((x, mx), ((Binding.reset_pos (Thm.def_binding_optional x a), atts), rhs))); in map_context_result (Local_Defs.add_defs defs) end)) |-> (set_facts o map (#2 o #2)) end; diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Apr 15 16:50:23 2016 +0200 @@ -1193,6 +1193,11 @@ let val (vars, _) = fold_map prep_var raw_vars ctxt; val (xs, ctxt') = Variable.add_fixes_binding (map #1 vars) ctxt; + val _ = + Context_Position.reports ctxt' + (flat (map2 (fn x => fn pos => + [(pos, Variable.markup ctxt' x), (pos, Variable.markup_entity_def ctxt' x)]) + xs (map (Binding.pos_of o #1) vars))); val vars' = map2 (fn x => fn (_, opt_T, mx) => (x, opt_T, mx)) xs vars; val (Ts, ctxt'') = fold_map declare_var vars' ctxt'; val vars'' = map2 (fn T => fn (x, _, mx) => (x, T, mx)) Ts vars'; diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Isar/specification.ML Fri Apr 15 16:50:23 2016 +0200 @@ -130,7 +130,14 @@ fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt = let val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars; - val (xs, params_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars; + val (xs, params_ctxt) = vars_ctxt + |> Context_Position.set_visible false + |> Proof_Context.add_fixes vars + ||> Context_Position.restore_visible vars_ctxt; + val _ = + Context_Position.reports params_ctxt + (map (Binding.pos_of o #1) vars ~~ + map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs); val Asss = (map o map) snd raw_specss diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/ML/ml_compiler.ML Fri Apr 15 16:50:23 2016 +0200 @@ -82,6 +82,17 @@ in cons (pos, markup, fn () => "") end end; + fun reported_entity_id def id loc = + let + val pos = Exn_Properties.position_of_polyml_location loc; + in + is_reported pos ? + let + fun markup () = + (Markup.entityN, [(if def then Markup.defN else Markup.refN, Markup.print_int id)]); + in cons (pos, markup, fn () => "") end + end; + fun reported_completions loc names = let val pos = Exn_Properties.position_of_polyml_location loc in if is_reported pos andalso not (null names) then @@ -94,6 +105,8 @@ fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) + | reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc + | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc | reported loc (PolyML.PTtype types) = reported_types loc types | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl @@ -268,7 +281,8 @@ PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth, PolyML.Compiler.CPCompilerResultFun result_fun, PolyML.Compiler.CPPrintInAlphabeticalOrder false, - PolyML.Compiler.CPDebug debug]; + PolyML.Compiler.CPDebug debug, + PolyML.Compiler.CPBindingSeq serial]; val _ = (while not (List.null (! input_buffer)) do diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/ML/ml_print_depth.ML --- a/src/Pure/ML/ml_print_depth.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/ML/ml_print_depth.ML Fri Apr 15 16:50:23 2016 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/ML/ml_print_depth0.ML +(* Title: Pure/ML/ml_print_depth.ML Author: Makarius Print depth for ML toplevel pp: context option with global default. diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/PIDE/markup.scala Fri Apr 15 16:50:23 2016 +0200 @@ -86,11 +86,12 @@ val BINDING = "binding" val ENTITY = "entity" - val DEF = "def" - val REF = "ref" object Entity { + val Def = new Properties.Long("def") + val Ref = new Properties.Long("ref") + def unapply(markup: Markup): Option[(String, String)] = markup match { case Markup(ENTITY, props) => diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 15 16:50:23 2016 +0200 @@ -51,9 +51,7 @@ [Name_Space.markup (Consts.space_of (Proof_Context.consts_of ctxt)) c]; fun markup_free ctxt x = - (if Variable.is_improper ctxt x then Markup.improper - else if Name.is_skolem x then Markup.skolem - else Markup.free) :: + Variable.markup ctxt x :: (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x then [Variable.markup_fixed ctxt x] else []); diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/Tools/simplifier_trace.ML --- a/src/Pure/Tools/simplifier_trace.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/Tools/simplifier_trace.ML Fri Apr 15 16:50:23 2016 +0200 @@ -6,6 +6,7 @@ signature SIMPLIFIER_TRACE = sig + val disable: Proof.context -> Proof.context val add_term_breakpoint: term -> Context.generic -> Context.generic val add_thm_breakpoint: thm -> Context.generic -> Context.generic end @@ -63,6 +64,13 @@ val get_data = Data.get o Context.Proof val put_data = Context.proof_map o Data.put +val disable = + Config.put simp_trace false #> + (Context.proof_map o Data.map) + (fn {max_depth, mode = _, interactive, parent, memory, breakpoints} => + {max_depth = max_depth, mode = Disabled, interactive = interactive, parent = parent, + memory = memory, breakpoints = breakpoints}); + val get_breakpoints = #breakpoints o get_data fun map_breakpoints f = diff -r 2e874d9aca43 -r 19a19ee36daa src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Pure/variable.ML Fri Apr 15 16:50:23 2016 +0200 @@ -43,9 +43,12 @@ val is_newly_fixed: Proof.context -> Proof.context -> string -> bool val fixed_ord: Proof.context -> string * string -> order val intern_fixed: Proof.context -> string -> string - val markup_fixed: Proof.context -> string -> Markup.T val lookup_fixed: Proof.context -> string -> string option val revert_fixed: Proof.context -> string -> string + val markup_fixed: Proof.context -> string -> Markup.T + val markup: Proof.context -> string -> Markup.T + val markup_entity_def: Proof.context -> string -> Markup.T + val dest_fixes: Proof.context -> (string * string) list val add_fixed_names: Proof.context -> term -> string list -> string list val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list val add_newly_fixed: Proof.context -> Proof.context -> @@ -58,7 +61,6 @@ val auto_fixes: term -> Proof.context -> Proof.context val fix_dummy_patterns: term -> Proof.context -> term * Proof.context val variant_fixes: string list -> Proof.context -> string list * Proof.context - val dest_fixes: Proof.context -> (string * string) list val gen_all: Proof.context -> thm -> thm val export_terms: Proof.context -> Proof.context -> term list -> term list val exportT_terms: Proof.context -> Proof.context -> term list -> term list @@ -375,6 +377,13 @@ Name_Space.markup (fixes_space ctxt) x |> Markup.name (revert_fixed ctxt x); +fun markup ctxt x = + if is_improper ctxt x then Markup.improper + else if Name.is_skolem x then Markup.skolem + else Markup.free; + +val markup_entity_def = Name_Space.markup_def o fixes_space; + fun dest_fixes ctxt = Name_Space.fold_table (fn (x, (y, _)) => cons (y, x)) (fixes_of ctxt) [] |> sort (Name_Space.entry_ord (fixes_space ctxt) o apply2 #2); diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/jEdit/etc/options Fri Apr 15 16:50:23 2016 +0200 @@ -99,6 +99,8 @@ option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" +option entity_color : string = "CCD9FF80" +option entity_ref_color : string = "800080FF" option breakpoint_disabled_color : string = "CCCC0080" option breakpoint_enabled_color : string = "FF9966FF" option quoted_color : string = "8B8B8B19" diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Apr 15 16:50:23 2016 +0200 @@ -185,6 +185,7 @@ private val delay_caret_update = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { session.caret_focus.post(Session.Caret_Focus) + JEdit_Lib.invalidate(text_area) } private val caret_listener = new CaretListener { @@ -194,7 +195,7 @@ /* text status overview left of scrollbar */ - private val overview = new Text_Overview(this) + private val text_overview = new Text_Overview(this) /* main */ @@ -202,7 +203,7 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Raw_Edits => - overview.invoke() + text_overview.invoke() case changed: Session.Commands_Changed => val buffer = model.buffer @@ -217,28 +218,9 @@ if (changed.assignment || load_changed || (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) - overview.invoke() + text_overview.invoke() - val visible_lines = text_area.getVisibleLines - if (visible_lines > 0) { - if (changed.assignment || load_changed) - text_area.invalidateScreenLineRange(0, visible_lines) - else { - val visible_range = JEdit_Lib.visible_range(text_area).get - val visible_iterator = - snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1) - if (visible_iterator.exists(changed.commands)) { - for { - line <- (0 until visible_lines).iterator - start = text_area.getScreenLineStartOffset(line) if start >= 0 - end = text_area.getScreenLineEndOffset(line) if end >= 0 - range = Text.Range(start, end) - line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1) - if line_cmds.exists(changed.commands) - } text_area.invalidateScreenLineRange(line, line) - } - } - } + JEdit_Lib.invalidate(text_area) } } } @@ -256,7 +238,7 @@ text_area.getGutter.addExtension(gutter_painter) text_area.addKeyListener(key_listener) text_area.addCaretListener(caret_listener) - text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint() + text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint() Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). foreach(text_area.addStructureMatcher(_)) session.raw_edits += main @@ -271,7 +253,7 @@ session.commands_changed -= main Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)). foreach(text_area.removeStructureMatcher(_)) - overview.revoke(); text_area.removeLeftOfScrollBar(overview) + text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview) text_area.removeCaretListener(caret_listener); delay_caret_update.revoke() text_area.removeKeyListener(key_listener) text_area.getGutter.removeExtension(gutter_painter) diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Apr 15 16:50:23 2016 +0200 @@ -234,6 +234,12 @@ } } + def invalidate(text_area: TextArea) + { + val visible_lines = text_area.getVisibleLines + if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) + } + /* graphics range */ diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Fri Apr 15 16:50:23 2016 +0200 @@ -151,6 +151,8 @@ private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) + private val caret_focus_elements = Markup.Elements(Markup.ENTITY) + private val highlight_elements = Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, @@ -206,7 +208,8 @@ Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements + Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + + Markup.Markdown_Item.name ++ active_elements private val foreground_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, @@ -250,6 +253,8 @@ val spell_checker_color = color_value("spell_checker_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") + val entity_color = color_value("entity_color") + val entity_ref_color = color_value("entity_ref_color") val breakpoint_disabled_color = color_value("breakpoint_disabled_color") val breakpoint_enabled_color = color_value("breakpoint_enabled_color") val caret_debugger_color = color_value("caret_debugger_color") @@ -392,6 +397,46 @@ } + /* caret focus */ + + def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = + { + val focus_results = + snapshot.cumulate[Set[Long]](caret_range, Set.empty, Rendering.caret_focus_elements, _ => + { + case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) => Some(serials + i) + case Markup.Entity.Ref(i) => Some(serials + i) + case _ => None + } + case _ => None + }) + val focus = (Set.empty[Long] /: focus_results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } + + def visible_focus(range: Text.Range): Boolean = + snapshot.cumulate[Boolean](range, false, Rendering.caret_focus_elements, _ => + { + case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if focus(i) => Some(true) + case _ => None + } + }).exists({ case Text.Info(_, visible) => visible }) + + if (focus.nonEmpty && (visible_focus(caret_range) || visible_focus(visible_range))) focus + else Set.empty[Long] + } + + def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = + snapshot.select(range, Rendering.caret_focus_elements, _ => + { + case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) => + Some(entity_ref_color) + case _ => None + }) + + /* highlighted area */ def highlight(range: Text.Range): Option[Text.Info[Color]] = @@ -697,7 +742,7 @@ /* text background */ - def background(range: Text.Range): List[Text.Info[Color]] = + def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = { for { Text.Info(r, result) <- @@ -712,6 +757,12 @@ Some((Nil, Some(bad_color))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(intensify_color))) + case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(entity_color))) + case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(entity_color))) + case _ => None + } case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => val color = depth match { diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Apr 15 16:50:23 2016 +0200 @@ -73,6 +73,7 @@ @volatile private var painter_rendering: Rendering = null @volatile private var painter_clip: Shape = null + @volatile private var caret_focus: Set[Long] = Set.empty private val set_state = new TextAreaExtension { @@ -82,6 +83,12 @@ { painter_rendering = get_rendering() painter_clip = gfx.getClip + caret_focus = + JEdit_Lib.visible_range(text_area) match { + case Some(visible_range) if caret_enabled => + painter_rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range) + case _ => Set.empty[Long] + } } } @@ -93,6 +100,7 @@ { painter_rendering = null painter_clip = null + caret_focus = Set.empty } } @@ -161,6 +169,9 @@ List((highlight_area, true), (hyperlink_area, true), (active_area, false)) def active_reset(): Unit = active_areas.foreach(_._1.reset) + private def area_active(): Boolean = + active_areas.exists({ case (area, _) => area.is_active }) + private val focus_listener = new FocusAdapter { override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } } } @@ -294,7 +305,7 @@ // background color for { - Text.Info(range, color) <- rendering.background(line_range) + Text.Info(range, color) <- rendering.background(line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color) @@ -557,8 +568,19 @@ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) } + // entity def range + if (!area_active() && caret_visible) { + for { + Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) + r <- JEdit_Lib.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) + } + } + // completion range - if (!hyperlink_area.is_active && caret_visible) { + if (!area_active() && caret_visible) { for { completion <- Completion_Popup.Text_Area(text_area) Text.Info(range, color) <- completion.rendering(rendering, line_range) diff -r 2e874d9aca43 -r 19a19ee36daa src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Apr 15 11:15:40 2016 +0200 +++ b/src/Tools/quickcheck.ML Fri Apr 15 16:50:23 2016 +0200 @@ -293,17 +293,19 @@ if not (Config.get ctxt quiet) andalso Config.get ctxt verbose then writeln s else (); -fun test_terms ctxt (limit_time, is_interactive) insts goals = - (case active_testers ctxt of - [] => error "No active testers for quickcheck" - | testers => - limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) - (fn () => - Par_List.get_some (fn tester => - tester ctxt (length testers > 1) insts goals |> - (fn result => if exists found_counterexample result then SOME result else NONE)) - testers) - (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ()); +fun test_terms ctxt0 (limit_time, is_interactive) insts goals = + let val ctxt = Simplifier_Trace.disable ctxt0 in + (case active_testers ctxt of + [] => error "No active testers for quickcheck" + | testers => + limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) + (fn () => + Par_List.get_some (fn tester => + tester ctxt (length testers > 1) insts goals |> + (fn result => if exists found_counterexample result then SOME result else NONE)) + testers) + (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ()) + end fun all_axioms_of ctxt t = let @@ -338,27 +340,28 @@ fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state = let - val lthy = Proof.context_of state; + val ctxt = Proof.context_of state; val thy = Proof.theory_of state; + fun strip (Const (@{const_name Pure.all}, _) $ Abs (_, _, t)) = strip t | strip t = t; val {goal = st, ...} = Proof.raw_goal state; val (gi, frees) = Logic.goal_params (Thm.prop_of st) i; - val some_locale = Named_Target.bottom_locale_of lthy; + val opt_locale = Named_Target.bottom_locale_of ctxt; val assms = - if Config.get lthy no_assms then [] + if Config.get ctxt no_assms then [] else - (case some_locale of - NONE => Assumption.all_assms_of lthy - | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy)); + (case opt_locale of + NONE => Assumption.all_assms_of ctxt + | SOME locale => Assumption.local_assms_of ctxt (Locale.init locale thy)); val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); fun axioms_of locale = (case fst (Locale.specification_of thy locale) of NONE => [] - | SOME t => the_default [] (all_axioms_of lthy t)); - val config = locale_config_of (Config.get lthy locale); + | SOME t => the_default [] (all_axioms_of ctxt t)); + val config = locale_config_of (Config.get ctxt locale); val goals = - (case some_locale of + (case opt_locale of NONE => [(proto_goal, eval_terms)] | SOME locale => fold (fn c => @@ -370,11 +373,11 @@ (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale)) else I) config []); val _ = - verbose_message lthy + verbose_message ctxt (Pretty.string_of - (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals))); + (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term ctxt o fst) goals))); in - test_terms lthy (time_limit, is_interactive) insts goals + test_terms ctxt (time_limit, is_interactive) insts goals end;