--- a/Admin/isatest/isatest-lint Fri Dec 03 17:16:53 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Florian Haftmann, TUM
-#
-# Do consistency and quality checks on the isabelle sources
-#
-
-use strict;
-use File::Find;
-use File::Basename;
-
-# configuration
-my $isabelleRoot = $ENV{'HOME'} . "/isabelle";
-my @suffices = ('\.thy', '\.ml', '\.ML');
-
-# lint main procedure
-sub lint() {
- my ($basename, $dirname, $ext) = fileparse($File::Find::name, @suffices);
- if ($ext) {
- open ISTREAM, $File::Find::name or die("error opening $File::Find::name");
- my $found = 0;
- while (<ISTREAM>) {
- $found ||= m/\$Id[^\$]*\$/;
- last if $found;
- }
- close ISTREAM;
- my $relname = substr($File::Find::name, (length $isabelleRoot) + 1);
- if (! $found) {
- print "Found no CVS id in $relname\n";
- }
- }
-}
-
-# first argument =^= isabelle repository root
-if (@ARGV) {
- $isabelleRoot = $ARGV[0];
-}
-
-find(\&lint, $isabelleRoot);
-
--- a/NEWS Fri Dec 03 17:16:53 2010 +0100
+++ b/NEWS Fri Dec 03 17:18:41 2010 +0100
@@ -101,6 +101,14 @@
*** HOL ***
+* Quickcheck now by default uses exhaustive testing instead of random testing.
+Random testing can be invoked by quickcheck[random],
+exhaustive testing by quickcheck[exhaustive].
+
+* Quickcheck instantiates polymorphic types with small finite datatypes
+by default. This enables a simple execution mechanism to handle
+quantifiers and function equality over the finite datatypes.
+
* Functions can be declared as coercions and type inference will add them
as necessary upon input of a term. In Complex_Main, real :: nat => real
and real :: int => real are declared as coercions. A new coercion function
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Dec 03 17:18:41 2010 +0100
@@ -929,14 +929,21 @@
and \emph{code} for code generation in SML.
\item @{command (HOL) "quickcheck"} tests the current goal for
- counter examples using a series of arbitrary assignments for its
+ counter examples using a series of assignments for its
free variables; by default the first subgoal is tested, an other
can be selected explicitly using an optional goal index.
+ Assignments can be chosen exhausting the search space upto a given
+ size or using a fixed number of random assignments in the search space.
+ By default, quickcheck uses exhaustive testing.
A number of configuration options are supported for
@{command (HOL) "quickcheck"}, notably:
\begin{description}
+ \item[@{text tester}] specifies how to explore the search space
+ (e.g. exhaustive or random).
+ An unknown configuration option is treated as an argument to tester,
+ making @{text "tester ="} optional.
\item[@{text size}] specifies the maximum size of the search space
for assignment values.
--- a/src/HOL/Enum.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Enum.thy Fri Dec 03 17:18:41 2010 +0100
@@ -46,14 +46,14 @@
end
+lemma [code]:
+ "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum"
+by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
+
lemma [code nbe]:
"HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
by (fact equal_refl)
-lemma [code]:
- "HOL.equal f g \<longleftrightarrow> list_all (%x. f x = g x) enum"
-by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
-
lemma order_fun [code]:
fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
@@ -318,6 +318,8 @@
datatype finite_1 = a\<^isub>1
+notation (output) a\<^isub>1 ("a\<^isub>1")
+
instantiation finite_1 :: enum
begin
@@ -352,6 +354,9 @@
datatype finite_2 = a\<^isub>1 | a\<^isub>2
+notation (output) a\<^isub>1 ("a\<^isub>1")
+notation (output) a\<^isub>2 ("a\<^isub>2")
+
instantiation finite_2 :: enum
begin
@@ -388,6 +393,10 @@
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
+notation (output) a\<^isub>1 ("a\<^isub>1")
+notation (output) a\<^isub>2 ("a\<^isub>2")
+notation (output) a\<^isub>3 ("a\<^isub>3")
+
instantiation finite_3 :: enum
begin
@@ -422,6 +431,11 @@
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
+notation (output) a\<^isub>1 ("a\<^isub>1")
+notation (output) a\<^isub>2 ("a\<^isub>2")
+notation (output) a\<^isub>3 ("a\<^isub>3")
+notation (output) a\<^isub>4 ("a\<^isub>4")
+
instantiation finite_4 :: enum
begin
@@ -438,6 +452,12 @@
datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
+notation (output) a\<^isub>1 ("a\<^isub>1")
+notation (output) a\<^isub>2 ("a\<^isub>2")
+notation (output) a\<^isub>3 ("a\<^isub>3")
+notation (output) a\<^isub>4 ("a\<^isub>4")
+notation (output) a\<^isub>5 ("a\<^isub>5")
+
instantiation finite_5 :: enum
begin
--- a/src/HOL/Finite_Set.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Finite_Set.thy Fri Dec 03 17:18:41 2010 +0100
@@ -517,6 +517,9 @@
lemma finite [simp]: "finite (A \<Colon> 'a set)"
by (rule subset_UNIV finite_UNIV finite_subset)+
+lemma finite_code [code]: "finite (A \<Colon> 'a set) = True"
+ by simp
+
end
lemma UNIV_unit [no_atp]:
--- a/src/HOL/Library/SML_Quickcheck.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Dec 03 17:18:41 2010 +0100
@@ -7,7 +7,21 @@
setup {*
Inductive_Codegen.quickcheck_setup #>
- Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
+ Context.theory_map (Quickcheck.add_generator ("SML",
+ fn ctxt => fn t =>
+ let
+ val test_fun = Codegen.test_term ctxt t
+ val iterations = Config.get ctxt Quickcheck.iterations
+ fun iterate size 0 = NONE
+ | iterate size j =
+ let
+ val result = test_fun size handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ in
+ case result of NONE => iterate size (j - 1) | SOME q => SOME q
+ end
+ in fn size => (iterate size iterations, NONE) end))
*}
end
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Fri Dec 03 17:18:41 2010 +0100
@@ -231,7 +231,7 @@
with wf less loc
have "approx_stk G hp [xcp] ST'"
by (auto simp add: sup_state_conv approx_stk_def approx_val_def
- elim: conf_widen split: Err.split)
+ elim: conf_widen split: err.split)
moreover
note len pc
ultimately
@@ -702,7 +702,7 @@
G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk>
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
apply (frule conf_widen)
prefer 2
apply assumption
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Fri Dec 03 17:18:41 2010 +0100
@@ -17,13 +17,24 @@
fun run_atp force_full_types timeout i n ctxt goal name =
let
val thy = ProofContext.theory_of ctxt
- val params as {full_types, ...} =
+ val chained_ths = [] (* a tactic has no chained ths *)
+ val params as {full_types, relevance_thresholds, max_relevant, ...} =
((if force_full_types then [("full_types", "true")] else [])
- @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
-(* @ [("overlord", "true")] *)
+ @ [("timeout", Int.toString (Time.toSeconds timeout))])
+ @ [("overlord", "true")]
|> Sledgehammer_Isar.default_params ctxt
val prover = Sledgehammer.get_prover thy false name
- val facts = []
+ val default_max_relevant =
+ Sledgehammer.default_max_relevant_for_prover thy name
+ val is_built_in_const =
+ Sledgehammer.is_built_in_const_for_prover ctxt name
+ val relevance_fudge = Sledgehammer.relevance_fudge_for_prover name
+ val relevance_override = {add = [], del = [], only = false}
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
+ val facts =
+ Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
(* Check for constants other than the built-in HOL constants. If none of
them appear (as should be the case for TPTP problems, unless "auto" or
"simp" already did its "magic"), we can skip the relevance filter. *)
@@ -32,11 +43,14 @@
not (String.isSubstring "HOL" s))
(prop_of goal))
val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, facts = [],
+ {state = Proof.init ctxt, goal = goal, subgoal = i,
+ facts = map Sledgehammer.Untranslated facts,
only = true, subgoal_count = n}
in
- prover params (K "") problem |> #message
- handle ERROR message => "Error: " ^ message ^ "\n"
+ (case prover params (K "") problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
end
fun to_period ("." :: _) = []
@@ -44,12 +58,6 @@
| to_period (s :: ss) = s :: to_period ss
| to_period [] = []
-val extract_metis_facts =
- space_explode " "
- #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
- #> fst o chop_while (not o member (op =) ["metis", "metisFT"])
- #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
-
val atp = "e" (* or "vampire" *)
fun thms_of_name ctxt name =
@@ -68,19 +76,20 @@
fun sledgehammer_with_metis_tac ctxt i th =
let
val thy = ProofContext.theory_of ctxt
- val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
- val s = run_atp false timeout i i ctxt th atp
- val xs = these (extract_metis_facts s)
- val ths = maps (thms_of_name ctxt) xs
- in Metis_Tactics.metis_tac ctxt ths i th end
+ val timeout = Time.fromSeconds 30
+ in
+ case run_atp false timeout i i ctxt th atp of
+ SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
fun sledgehammer_as_oracle_tac ctxt i th =
let
val thy = ProofContext.theory_of ctxt
- val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
- val s = run_atp true timeout i i ctxt th atp
+ val timeout = Time.fromSeconds 30
+ val xs = run_atp true timeout i i ctxt th atp
in
- if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
+ if is_some xs then Skip_Proof.cheat_tac thy th
else Seq.empty
end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Dec 03 17:18:41 2010 +0100
@@ -313,7 +313,7 @@
lemma snd_linear: "linear snd" unfolding linear_def by (simp add: algebra_simps)
-lemma fst_snd_linear: "linear (%z. fst z + snd z)" unfolding linear_def by (simp add: algebra_simps)
+lemma fst_snd_linear: "linear (%(x,y). x + y)" unfolding linear_def by (simp add: algebra_simps)
lemma scaleR_2:
fixes x :: "'a::real_vector"
@@ -5451,11 +5451,11 @@
shows "convex hull (S \<oplus> T) = (convex hull S) \<oplus> (convex hull T)"
proof-
have "(convex hull S) \<oplus> (convex hull T) =
- (%z. fst z + snd z) ` ((convex hull S) <*> (convex hull T))"
+ (%(x,y). x + y) ` ((convex hull S) <*> (convex hull T))"
by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
+also have "... = (%(x,y). x + y) ` (convex hull (S <*> T))" using convex_hull_direct_sum by auto
also have "...= convex hull (S \<oplus> T)" using fst_snd_linear linear_conv_bounded_linear
- convex_hull_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+ convex_hull_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
finally show ?thesis by auto
qed
@@ -5464,11 +5464,11 @@
assumes "convex S" "convex T"
shows "rel_interior (S \<oplus> T) = (rel_interior S) \<oplus> (rel_interior T)"
proof-
-have "(rel_interior S) \<oplus> (rel_interior T) = (%z. fst z + snd z) ` (rel_interior S <*> rel_interior T)"
+have "(rel_interior S) \<oplus> (rel_interior T) = (%(x,y). x + y) ` (rel_interior S <*> rel_interior T)"
by (simp add: set_plus_image)
-also have "... = (%z. fst z + snd z) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
+also have "... = (%(x,y). x + y) ` rel_interior (S <*> T)" using rel_interior_direct_sum assms by auto
also have "...= rel_interior (S \<oplus> T)" using fst_snd_linear convex_direct_sum assms
- rel_interior_convex_linear_image[of "(%z. fst z + snd z)" "S <*> T"] by (auto simp add: set_plus_image)
+ rel_interior_convex_linear_image[of "(%(x,y). x + y)" "S <*> T"] by (auto simp add: set_plus_image)
finally show ?thesis by auto
qed
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Fri Dec 03 17:18:41 2010 +0100
@@ -26,7 +26,7 @@
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
-ML {* Auto_Tools.time_limit := 10 *}
+ML {* Auto_Tools.time_limit := 10.0 *}
ML {* val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/mutabelle.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Fri Dec 03 17:18:41 2010 +0100
@@ -55,7 +55,7 @@
structure Mutabelle : MUTABELLE =
struct
-val testgen_name = Unsynchronized.ref "SML";
+val testgen_name = Unsynchronized.ref "random";
fun all_unconcealed_thms_of thy =
let
@@ -497,9 +497,12 @@
(map_types (inst_type insts) (freeze t));
fun is_executable thy insts th =
- ((Quickcheck.test_term
- ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
- (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
+ ((Quickcheck.test_term
+ (ProofContext.init_global thy
+ |> Config.put Quickcheck.size 1
+ |> Config.put Quickcheck.iterations 1
+ |> Config.put Quickcheck.tester (!testgen_name))
+ false (preprocess thy insts (prop_of th));
Output.urgent_message "executable"; true) handle ERROR s =>
(Output.urgent_message ("not executable: " ^ s); false));
@@ -507,9 +510,10 @@
| qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter
(Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
((x, pretty (the_default [] (fst (Quickcheck.test_term
- ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
+ ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
+ #> Config.put Quickcheck.tester (!testgen_name))
(ProofContext.init_global usedthy))
- (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
+ false (preprocess usedthy insts x))))) :: acc))
handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Dec 03 17:18:41 2010 +0100
@@ -114,13 +114,14 @@
(** quickcheck **)
fun invoke_quickcheck change_options quickcheck_generator thy t =
- TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
+ TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
(fn _ =>
case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
- (SOME quickcheck_generator, []) [t] of
+ false [] [t] of
(NONE, _) => (NoCex, ([], NONE))
| (SOME _, _) => (GenuineCex, ([], NONE))) ()
- handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
+ handle TimeLimit.TimeOut =>
+ (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
@@ -331,7 +332,7 @@
(Quickcheck.test_goal_terms
((Config.put Quickcheck.finite_types true #>
Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
- (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+ false [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
end
fun is_executable_thm thy th = is_executable_term thy (prop_of th)
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Dec 03 17:18:41 2010 +0100
@@ -33,7 +33,7 @@
lemma
"w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
definition "filter_a = filter (\<lambda>x. x = a)"
@@ -67,7 +67,7 @@
theorem S\<^isub>1_sound:
"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
@@ -91,7 +91,7 @@
theorem S\<^isub>2_sound:
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -113,7 +113,7 @@
lemma S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
oops
@@ -131,7 +131,7 @@
theorem S\<^isub>3_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
-quickcheck[generator = prolog, size=1, iterations=1]
+quickcheck[tester = prolog, size=1, iterations=1]
oops
*)
@@ -156,7 +156,7 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
oops
(*
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Fri Dec 03 17:18:41 2010 +0100
@@ -23,8 +23,8 @@
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 10000, report]
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = random, iterations = 10000, report]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
section {* Manual setup to find the counterexample *}
@@ -39,7 +39,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops
setup {* Code_Prolog.map_code_options (K
@@ -52,7 +52,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
section {* Simulating a global depth limit manually by limiting all predicates *}
@@ -70,7 +70,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops
setup {*
@@ -86,7 +86,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
section {* Using a global limit for limiting the execution *}
@@ -105,7 +105,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops
text {* But a global depth limit of 14 does. *}
@@ -122,7 +122,7 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Fri Dec 03 17:18:41 2010 +0100
@@ -50,8 +50,8 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
-quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Dec 03 17:18:41 2010 +0100
@@ -27,7 +27,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Dec 03 17:18:41 2010 +0100
@@ -30,7 +30,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Dec 03 17:18:41 2010 +0100
@@ -30,7 +30,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
- quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
+ quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Fri Dec 03 17:18:41 2010 +0100
@@ -31,7 +31,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
nitpick (* nitpick fails here! *)
- quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+ quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
oops
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Dec 03 17:18:41 2010 +0100
@@ -92,7 +92,7 @@
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops
text {* Verifying that the found counterexample really is one by means of a proof *}
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Dec 03 17:18:41 2010 +0100
@@ -16,9 +16,9 @@
manual_reorder = []}) *}
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, expect = counterexample]
oops
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Dec 03 17:18:41 2010 +0100
@@ -48,7 +48,7 @@
lemma
"is_ten x = is_eleven x"
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
oops
section {* Context Free Grammar *}
@@ -65,7 +65,7 @@
lemma
"w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = predicate_compile_ff_nofs, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, iterations=1]
oops
theorem S\<^isub>1_sound:
@@ -136,7 +136,7 @@
oops
lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = predicate_compile_ff_fs]
+quickcheck[size=10, tester = predicate_compile_ff_fs]
oops
theorem S\<^isub>3_complete:
@@ -157,12 +157,12 @@
theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
oops
theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
oops
hide_const a b
@@ -202,7 +202,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
- quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
+ quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
oops
subsection {* Lambda *}
@@ -257,7 +257,7 @@
lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10]
+quickcheck[tester = predicate_compile_ff_fs, size = 7, iterations = 10]
oops
subsection {* JAD *}
@@ -341,12 +341,12 @@
"jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"
lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
-quickcheck[generator = predicate_compile_ff_nofs, size = 6]
+quickcheck[tester = predicate_compile_ff_nofs, size = 6]
oops
lemma
"\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v"
-quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_wo_ff]
oops
end
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Dec 03 17:18:41 2010 +0100
@@ -89,9 +89,9 @@
lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*nitpick
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_ff_fs]
oops*)
oops
@@ -115,10 +115,10 @@
prolog-style generation. *}
lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[generator = code, iterations = 100000, expect = counterexample]
-(*quickcheck[generator = predicate_compile_wo_ff]*)
-(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
-(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
+quickcheck[tester = random, iterations = 100000, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
oops
section {* Given a partial solution *}
@@ -130,8 +130,8 @@
assumes "q = Seq (Sym N0) (Sym N0)"
(* assumes "s = [N0, N0]"*)
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
oops
section {* Checking the counterexample *}
@@ -147,7 +147,7 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_wo_ff]*)
oops
lemma
@@ -157,8 +157,8 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
oops
lemma
@@ -168,13 +168,13 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = prolog, expect = counterexample]
oops
lemma "prop_regex a_sol"
-quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, expect = counterexample]
+quickcheck[tester = predicate_compile_ff_fs]
oops
value [code] "prop_regex a_sol"
--- a/src/HOL/Product_Type.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Product_Type.thy Fri Dec 03 17:18:41 2010 +0100
@@ -160,7 +160,7 @@
declare prod.simps(2) [nitpick_simp del]
-declare weak_case_cong [cong del]
+declare prod.weak_case_cong [cong del]
subsubsection {* Tuple syntax *}
@@ -440,7 +440,7 @@
lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
-- {* Prevents simplification of @{term c}: much faster *}
- by (fact weak_case_cong)
+ by (fact prod.weak_case_cong)
lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
by (simp add: split_eta)
@@ -578,7 +578,7 @@
\medskip @{term split} used as a logical connective or set former.
\medskip These rules are for use with @{text blast}; could instead
- call @{text simp} using @{thm [source] split} as rewrite. *}
+ call @{text simp} using @{thm [source] prod.split} as rewrite. *}
lemma splitI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> split c p"
apply (simp only: split_tupled_all)
--- a/src/HOL/Quickcheck.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Quickcheck.thy Fri Dec 03 17:18:41 2010 +0100
@@ -129,6 +129,7 @@
use "Tools/quickcheck_generators.ML"
setup Quickcheck_Generators.setup
+declare [[quickcheck_tester = random]]
subsection {* Code setup *}
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Dec 03 17:18:41 2010 +0100
@@ -275,7 +275,7 @@
proof (cases x, clarify)
fix a b
show "P (a, b)"
- proof (induct a arbitrary: b rule: Nat.induct)
+ proof (induct a arbitrary: b rule: nat.induct)
case zero
show "P (0, b)" using assms by (induct b) auto
next
--- a/src/HOL/Relation.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Relation.thy Fri Dec 03 17:18:41 2010 +0100
@@ -132,6 +132,11 @@
lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)"
by blast
+lemma Id_on_def'[nitpick_def, code]:
+ "(Id_on (A :: 'a => bool)) = (%(x, y). x = y \<and> A x)"
+by (auto simp add: fun_eq_iff
+ elim: Id_onE[unfolded mem_def] intro: Id_onI[unfolded mem_def])
+
lemma Id_on_subset_Times: "Id_on A \<subseteq> A \<times> A"
by blast
--- a/src/HOL/Smallcheck.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Smallcheck.thy Fri Dec 03 17:18:41 2010 +0100
@@ -48,7 +48,7 @@
end
-section {* full small value generator type classes *}
+subsection {* full small value generator type classes *}
class full_small = term_of +
fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
@@ -80,7 +80,7 @@
instantiation prod :: (full_small, full_small) full_small
begin
-ML {* @{const_name "Pair"} *}
+
definition
"full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
%u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
@@ -97,14 +97,16 @@
"full_small_fun' f i d = (if i > 1 then
full_small (%(a, at). full_small (%(b, bt).
full_small_fun' (%(g, gt). f (g(a := b),
- (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in 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]]]]))
-
- (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
- full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
+ (%_. let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = (Typerep.typerep (TYPE('b)))
+ in
+ 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]]]]))
+ (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
+ else (if i > 0 then
+ full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
where
@@ -117,6 +119,11 @@
subsection {* Defining combinators for any first-order data type *}
+definition orelse :: "'a option => 'a option => 'a option"
+where
+ [code_unfold]: "orelse x y = (case x of Some x' => Some x' | None => y)"
+
+
definition catch_match :: "term list option => term list option => term list option"
where
[code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
@@ -126,11 +133,11 @@
use "Tools/smallvalue_generators.ML"
-(* We do not activate smallcheck yet.
setup {* Smallvalue_Generators.setup *}
-*)
+
+declare [[quickcheck_tester = exhaustive]]
-hide_fact catch_match_def
-hide_const (open) catch_match
+hide_fact orelse_def catch_match_def
+hide_const (open) orelse catch_match
end
\ No newline at end of file
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 03 17:18:41 2010 +0100
@@ -628,9 +628,9 @@
val ([dt_induct'], thy7) =
thy6
- |> Sign.add_path big_name
- |> Global_Theory.add_thms [((Binding.name "induct", dt_induct), [case_names_induct])]
- ||> Sign.parent_path
+ |> Global_Theory.add_thms
+ [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
+ [case_names_induct])]
||> Theory.checkpoint;
in
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 03 17:18:41 2010 +0100
@@ -98,18 +98,18 @@
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thmss
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Sign.add_path tname
- #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.add_thms
+ [((Binding.qualify true tname (Binding.name label), thms), atts)]
+ #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Dec 03 17:18:41 2010 +0100
@@ -362,14 +362,14 @@
let
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val prfx = Binding.qualify true (space_implode "_" new_type_names);
val (((inject, distinct), [induct]), thy2) =
thy1
|> store_thmss "inject" new_type_names raw_inject
||>> store_thmss "distinct" new_type_names raw_distinct
- ||> Sign.add_path (space_implode "_" new_type_names)
||>> Global_Theory.add_thms
- [((Binding.name "induct", raw_induct), [mk_case_names_induct descr])]
- ||> Sign.restore_naming thy1;
+ [((prfx (Binding.name "induct"), raw_induct),
+ [mk_case_names_induct descr])];
in
thy2
|> derive_datatype_props config dt_names alt_names [descr] sorts
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Dec 03 17:18:41 2010 +0100
@@ -383,9 +383,8 @@
"set and display the default parameters for Nitpick"
Keyword.thy_decl parse_nitpick_params_command
-fun auto_nitpick state =
- if not (!auto) then (false, state) else pick_nits [] true 1 0 state
+val auto_nitpick = pick_nits [] true 1 0
-val setup = Auto_Tools.register_tool ("nitpick", auto_nitpick)
+val setup = Auto_Tools.register_tool (auto, auto_nitpick)
end;
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Dec 03 17:18:41 2010 +0100
@@ -38,7 +38,7 @@
val write_program : logic_program -> string
val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list
- val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool)
+ val quickcheck : Proof.context -> term -> int -> term list option * Quickcheck.report option
val trace : bool Unsynchronized.ref
@@ -129,8 +129,8 @@
(* general string functions *)
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
(* internal program representation *)
@@ -835,7 +835,7 @@
val parse_term = fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
- o explode
+ o raw_explode
fun parse_solutions sol =
let
@@ -1030,9 +1030,8 @@
case tss of
[ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
| _ => NONE
- val empty_report = ([], false)
in
- (res, empty_report)
+ (res, NONE)
end;
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 03 17:18:41 2010 +0100
@@ -22,7 +22,7 @@
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
- Proof.context -> term -> int -> term list option * (bool list * bool);
+ Proof.context -> term -> int -> term list option * Quickcheck.report option;
(* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
@@ -344,9 +344,8 @@
fun compile_term' compilation options depth ctxt t =
let
val c = compile_term compilation options ctxt t
- val dummy_report = ([], false)
in
- fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
+ fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
end
fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 17:18:41 2010 +0100
@@ -347,14 +347,11 @@
parse_sledgehammer_params_command
fun auto_sledgehammer state =
- if not (!auto) then
- (false, state)
- else
- let val ctxt = Proof.context_of state in
- run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
- (minimize_command [] 1) state
- end
+ let val ctxt = Proof.context_of state in
+ run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
+ (minimize_command [] 1) state
+ end
-val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
+val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
end;
--- a/src/HOL/Tools/inductive.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Dec 03 17:18:41 2010 +0100
@@ -596,7 +596,7 @@
val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
-
+
(* prove induction rule *)
fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
--- a/src/HOL/Tools/inductive_codegen.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Dec 03 17:18:41 2010 +0100
@@ -9,7 +9,7 @@
val add : string option -> int option -> attribute
val test_fn : (int * int * int -> term list option) Unsynchronized.ref
val test_term:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val setup : theory -> theory
val quickcheck_setup : theory -> theory
end;
@@ -842,10 +842,9 @@
val start = Config.get ctxt depth_start;
val offset = Config.get ctxt size_offset;
val test_fn' = !test_fn;
- val dummy_report = ([], false)
fun test k = (deepen bound (fn i =>
(Output.urgent_message ("Search depth: " ^ string_of_int i);
- test_fn' (i, values, k+offset))) start, dummy_report);
+ test_fn' (i, values, k+offset))) start, NONE);
in test end;
val quickcheck_setup =
--- a/src/HOL/Tools/quickcheck_generators.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML Fri Dec 03 17:18:41 2010 +0100
@@ -17,7 +17,7 @@
string list * string list -> typ list * typ list -> theory -> theory)
-> Datatype.config -> string list -> theory -> theory
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> seed -> term list option * seed)
-> Proof.context -> Proof.context
val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed)
@@ -387,25 +387,73 @@
Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check))
end
+(* single quickcheck report *)
+
+datatype single_report = Run of bool list * bool | MatchExc
+
+fun collect_single_report single_report
+ (Quickcheck.Report {iterations = iterations, raised_match_errors = raised_match_errors,
+ satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
+ case single_report
+ of MatchExc =>
+ Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
+ satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
+ | Run (assms, concl) =>
+ Quickcheck.Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
+ satisfied_assms =
+ map2 (fn b => fn s => if b then s + 1 else s) assms
+ (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
+ positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
+
+val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0,
+ satisfied_assms = [], positive_concl_tests = 0 }
+
fun compile_generator_expr ctxt t =
let
val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
- in if Config.get ctxt Quickcheck.report then
- let
- val t' = mk_reporting_generator_expr thy t Ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
- in compile #> Random_Engine.run end
- else
- let
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
- val dummy_report = ([], false)
- in compile #> Random_Engine.run #> rpair dummy_report end
+ val iterations = Config.get ctxt Quickcheck.iterations
+ in
+ if Config.get ctxt Quickcheck.report then
+ let
+ val t' = mk_reporting_generator_expr thy t Ts;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample_Report.get, put_counterexample_report, "Quickcheck_Generators.put_counterexample_report")
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
+ val single_tester = compile #> Random_Engine.run
+ fun iterate_and_collect size 0 report = (NONE, report)
+ | iterate_and_collect size j report =
+ let
+ val (test_result, single_report) = apsnd Run (single_tester size) handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
+ val report = collect_single_report single_report report
+ in
+ case test_result of NONE => iterate_and_collect size (j - 1) report
+ | SOME q => (SOME q, report)
+ end
+ in
+ fn size => apsnd SOME (iterate_and_collect size iterations empty_report)
+ end
+ else
+ let
+ val t' = mk_generator_expr thy t Ts;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample.get, put_counterexample, "Quickcheck_Generators.put_counterexample")
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
+ val single_tester = compile #> Random_Engine.run
+ fun iterate size 0 = NONE
+ | iterate size j =
+ let
+ val result = single_tester size handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ in
+ case result of NONE => iterate size (j - 1) | SOME q => SOME q
+ end
+ in
+ fn size => (rpair NONE (iterate size iterations))
+ end
end;
--- a/src/HOL/Tools/smallvalue_generators.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Fri Dec 03 17:18:41 2010 +0100
@@ -7,15 +7,25 @@
signature SMALLVALUE_GENERATORS =
sig
val compile_generator_expr:
- Proof.context -> term -> int -> term list option * (bool list * bool)
+ Proof.context -> term -> int -> term list option * Quickcheck.report option
val put_counterexample: (unit -> int -> term list option)
-> Proof.context -> Proof.context
+ val smart_quantifier : bool Config.T;
val setup: theory -> theory
end;
structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
struct
+(* static options *)
+
+val define_foundationally = false
+
+(* dynamic options *)
+
+val (smart_quantifier, setup_smart_quantifier) =
+ Attrib.config_bool "quickcheck_smart_quantifier" (K true)
+
(** general term functions **)
fun mk_measure f =
@@ -36,6 +46,8 @@
end
| mk_sumcases _ f T = f T
+fun mk_undefined T = Const(@{const_name undefined}, T)
+
(** abstract syntax **)
@@ -50,8 +62,8 @@
let
val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
in
- Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
- $ y $ Const (@{const_name Some}, T' --> T) $ x
+ Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
+ $ x $ y
end
(** datatypes **)
@@ -70,11 +82,8 @@
fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
-fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
+fun mk_equations thy descr vs tycos smalls (Ts, Us) =
let
- val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
- val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
- smallsN (Ts @ Us)
fun mk_small_call T =
let
val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
@@ -119,44 +128,77 @@
val lhss = map2 (fn t => fn T => t $ test_function T $ size) smalls (Ts @ Us);
val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
in
- (Ts @ Us ~~ (smallsN ~~ eqs))
+ eqs
+ end
+
+(* foundational definition with the function package *)
+
+val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
+
+fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
+ Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
+
+fun mk_termination_measure T =
+ let
+ val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
+ in
+ mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
end
-
-val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
-
+
+fun termination_tac ctxt =
+ Function_Relation.relation_tac ctxt mk_termination_measure 1
+ THEN rtac @{thm wf_measure} 1
+ THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac
+ (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
+ @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
+
+fun pat_completeness_auto ctxt =
+ Pat_Completeness.pat_completeness_tac ctxt 1
+ THEN auto_tac (clasimpset_of ctxt)
+
+
+(* creating the instances *)
+
fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
let
val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
- val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
- fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
- Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
- fun mk_termination_measure T =
- let
- val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
- in
- mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
- end
- fun termination_tac ctxt =
- Function_Relation.relation_tac ctxt mk_termination_measure 1
- THEN rtac @{thm wf_measure} 1
- THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac
- (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
- @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1))
- fun pat_completeness_auto ctxt =
- Pat_Completeness.pat_completeness_tac ctxt 1
- THEN auto_tac (clasimpset_of ctxt)
- in
+ val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
+ in
thy
|> Class.instantiation (tycos, vs, @{sort full_small})
- |> Function.add_function
- (map (fn (T, (name, _)) =>
- Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
- (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
- Function_Common.default_config pat_completeness_auto
- |> snd
- |> Local_Theory.restore
- |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
- |> snd
+ |> (if define_foundationally then
+ let
+ val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us)
+ val eqs = mk_equations thy descr vs tycos smalls (Ts, Us)
+ in
+ Function.add_function
+ (map (fn (name, T) =>
+ Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T)))
+ (smallsN ~~ (Ts @ Us)))
+ (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs)
+ Function_Common.default_config pat_completeness_auto
+ #> snd
+ #> Local_Theory.restore
+ #> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
+ #> snd
+ end
+ else
+ fold_map (fn (name, T) => Local_Theory.define
+ ((Binding.conceal (Binding.name name), NoSyn),
+ (apfst Binding.conceal Attrib.empty_binding, mk_undefined (full_smallT T)))
+ #> apfst fst) (smallsN ~~ (Ts @ Us))
+ #> (fn (smalls, lthy) =>
+ let
+ val eqs_t = mk_equations thy descr vs tycos smalls (Ts, Us)
+ val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
+ (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+ in
+ fold (fn (name, eq) => Local_Theory.note
+ ((Binding.conceal (Binding.qualify true prfx
+ (Binding.qualify true name (Binding.name "simps"))),
+ Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+ [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (smallsN ~~ eqs) lthy
+ end))
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end handle FUNCTION_TYPE =>
(Datatype_Aux.message config
@@ -173,12 +215,50 @@
val target = "Quickcheck";
-fun mk_generator_expr thy prop Ts =
+fun mk_smart_generator_expr ctxt t =
let
+ val ((vnames, Ts), t') = apfst split_list (strip_abs t)
+ val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
+ val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
+ val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
+ val depth = Free (depth_name, @{typ code_numeral})
+ val frees = map2 (curry Free) names Ts
+ val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
+ fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+ | strip_imp A = ([], A)
+ val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
+ val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
+ fun mk_small_closure (free as Free (_, T), term_var) t =
+ Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ lambda free (lambda term_var t)) $ depth
+ fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
+ val none_t = @{term "None :: term list option"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
+ (@{term "If :: bool => term list option => term list option => term list option"}
+ $ cond $ then_t $ else_t) $ none_t;
+ fun mk_test_term bound_vars assms =
+ let
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] =>
+ (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
+ | assm :: assms =>
+ (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_small_closure (map lookup vars) (mk_safe_if check)
+ end
+ in lambda depth (mk_test_term [] assms) end
+
+fun mk_generator_expr ctxt t =
+ let
+ val Ts = (map snd o fst o strip_abs) t;
+ val thy = ProofContext.theory_of ctxt
val bound_max = length Ts - 1;
val bounds = map_index (fn (i, ty) =>
(2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
+ val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
val check =
@{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
@@ -193,26 +273,22 @@
fun compile_generator_expr ctxt t =
let
- val Ts = (map snd o fst o strip_abs) t;
val thy = ProofContext.theory_of ctxt
- in if Config.get ctxt Quickcheck.report then
- error "Compilation with reporting facility is not supported"
- else
- let
- val t' = mk_generator_expr thy t Ts;
- val compile = Code_Runtime.dynamic_value_strict
- (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
- val dummy_report = ([], false)
- in compile #> rpair dummy_report end
- end;
+ val t' =
+ (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
+ ctxt t;
+ val compile = Code_Runtime.dynamic_value_strict
+ (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
+ thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
+ in fn size => rpair NONE (compile size) end;
(** setup **)
val setup =
Datatype.interpretation
(Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
+ #> setup_smart_quantifier
#> Context.theory_map
- (Quickcheck.add_generator ("small", compile_generator_expr));
+ (Quickcheck.add_generator ("exhaustive", compile_generator_expr));
end;
--- a/src/HOL/Tools/try.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/Tools/try.ML Fri Dec 03 17:18:41 2010 +0100
@@ -110,8 +110,8 @@
(Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
o Toplevel.proof_of)))
-fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
+val auto_try = do_try true NONE
-val setup = Auto_Tools.register_tool (tryN, auto_try)
+val setup = Auto_Tools.register_tool (auto, auto_try)
end;
--- a/src/HOL/ex/Quickcheck_Examples.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy Fri Dec 03 17:18:41 2010 +0100
@@ -9,8 +9,6 @@
imports Main
begin
-setup {* Smallvalue_Generators.setup *}
-
text {*
The 'quickcheck' command allows to find counterexamples by evaluating
formulae.
@@ -26,33 +24,33 @@
subsection {* Lists *}
theorem "map g (map f xs) = map (g o f) xs"
- quickcheck[size = 3]
- quickcheck[generator = random, expect = no_counterexample]
- quickcheck[generator = small, size = 3, iterations = 1, report = false, expect = no_counterexample]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, size = 3, expect = no_counterexample]
oops
theorem "map g (map f xs) = map (f o g) xs"
- quickcheck[generator = random, expect = counterexample]
- quickcheck[generator = small, report = false]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
theorem "rev (xs @ ys) = rev ys @ rev xs"
- quickcheck[expect = no_counterexample]
- quickcheck[generator = small, expect = no_counterexample, report = false]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
oops
theorem "rev (xs @ ys) = rev xs @ rev ys"
- quickcheck[generator = small, expect = counterexample, report = false]
- quickcheck[generator = random, expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
theorem "rev (rev xs) = xs"
- quickcheck[expect = no_counterexample]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
oops
theorem "rev xs = xs"
- quickcheck[generator = small, report = false]
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
text {* An example involving functions inside other data structures *}
@@ -62,13 +60,13 @@
| "app (f # fs) x = app fs (f x)"
lemma "app (fs @ gs) x = app gs (app fs x)"
- quickcheck[generator = random, expect = no_counterexample]
- quickcheck[generator = small, iterations = 1, size = 4, report = false, expect = no_counterexample]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, size = 4, expect = no_counterexample]
by (induct fs arbitrary: x) simp_all
lemma "app (fs @ gs) x = app fs (app gs x)"
- quickcheck[generator = random, expect = counterexample]
- quickcheck[generator = small, report = false, expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -82,19 +80,19 @@
text {* A lemma, you'd think to be true from our experience with delAll *}
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
-- {* Wrong. Precondition needed.*}
- quickcheck[generator = small, report = false]
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[generator = small, report = false]
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
-- {* Also wrong.*}
oops
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[generator = small, report = false]
- quickcheck[expect = no_counterexample]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
by (induct xs) auto
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -103,13 +101,14 @@
else (x#(replace a b xs)))"
lemma "occurs a xs = occurs b (replace a b xs)"
- quickcheck[generator = small, report = false]
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
-- {* Wrong. Precondition needed.*}
oops
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
- quickcheck[expect = no_counterexample, report = false]
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
by (induct xs) simp_all
@@ -132,12 +131,14 @@
| "mirror (Branch l r) = Branch (mirror r) (mirror l)"
theorem "plant (rev (leaves xt)) = mirror xt"
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
--{* Wrong! *}
oops
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
--{* Wrong! *}
oops
@@ -152,9 +153,9 @@
| "root (Node f x y) = f"
theorem "hd (inOrder xt) = root xt"
- quickcheck[generator = small, report = false]
- quickcheck[expect = counterexample]
- --{* Wrong! *}
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ --{* Wrong! *}
oops
@@ -165,75 +166,75 @@
lemma
"[] ~= xs ==> hd xs = last (x # xs)"
-quickcheck[generator = random, report = false]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
shows "drop n xs = takeWhile P xs"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, quiet]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[generator = random, iterations = 10000, report = false, quiet]
-quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
oops
lemma
"i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[generator = random, iterations = 1000, report = false, quiet]
-quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
oops
lemma
"ns ! k < length ns ==> k <= listsum ns"
-quickcheck[generator = random, iterations = 10000, report = true, quiet]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000, finite_types = false, quiet]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
oops
lemma
"[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
-quickcheck[generator = random, iterations = 10000, report = true]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
oops
lemma
"(ys = zs) = (xs @ ys = splice xs zs)"
-quickcheck[generator = random]
-quickcheck[generator = small, report = false, expect = counterexample]
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
oops
section {* Examples with quantifiers *}
@@ -243,14 +244,17 @@
*}
lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
- quickcheck[expect = counterexample]
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
oops
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+ quickcheck[random, expect = counterexample]
quickcheck[expect = counterexample]
oops
lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+ quickcheck[random, expect = counterexample]
quickcheck[expect = counterexample]
oops
--- a/src/HOL/ex/set.thy Fri Dec 03 17:16:53 2010 +0100
+++ b/src/HOL/ex/set.thy Fri Dec 03 17:18:41 2010 +0100
@@ -205,7 +205,7 @@
lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
-- {* Example 11: needs a hint. *}
-by(metis Nat.induct)
+by(metis nat.induct)
lemma
"(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)
--- a/src/Pure/codegen.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Pure/codegen.ML Fri Dec 03 17:18:41 2010 +0100
@@ -76,7 +76,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> term list option) Unsynchronized.ref
- val test_term: Proof.context -> term -> int -> term list option * (bool list * bool)
+ val test_term: Proof.context -> term -> int -> term list option
val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -895,8 +895,7 @@
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
- val dummy_report = ([], false)
- in (fn size => (! test_fn size, dummy_report)) end;
+ in (fn size => (! test_fn size)) end;
--- a/src/Pure/library.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Pure/library.ML Fri Dec 03 17:18:41 2010 +0100
@@ -727,7 +727,7 @@
(*simple quoting (does not escape special chars)*)
val quote = enclose "\"" "\"";
-(*space_implode "..." (explode "hello") = "h...e...l...l...o"*)
+(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
fun space_implode a bs = implode (separate a bs);
val commas = space_implode ", ";
--- a/src/Tools/auto_tools.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/auto_tools.ML Fri Dec 03 17:18:41 2010 +0100
@@ -6,10 +6,11 @@
signature AUTO_TOOLS =
sig
- val time_limit: int Unsynchronized.ref
+ val time_limit: real Unsynchronized.ref
val register_tool :
- string * (Proof.state -> bool * Proof.state) -> theory -> theory
+ bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
+ -> theory
end;
structure Auto_Tools : AUTO_TOOLS =
@@ -17,20 +18,20 @@
(* preferences *)
-val time_limit = Unsynchronized.ref 4000
+val time_limit = Unsynchronized.ref 4.0
+val auto_tools_time_limitN = "auto-tools-time-limit"
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (Preferences.nat_pref time_limit
- "auto-tools-time-limit"
- "Time limit for automatic tools (in milliseconds).")
+ (Preferences.real_pref time_limit
+ auto_tools_time_limitN "Time limit for automatic tools (in seconds).")
(* configuration *)
structure Data = Theory_Data
(
- type T = (string * (Proof.state -> bool * Proof.state)) list
+ type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
val empty = []
val extend = I
fun merge data : T = AList.merge (op =) (K true) data
@@ -41,18 +42,30 @@
(* automatic testing *)
+fun run_tools tools state =
+ tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
+ |> Par_List.get_some (fn tool =>
+ case try tool state of
+ SOME (true, state) => SOME state
+ | _ => NONE)
+ |> the_default state
+
+(* Too large values are understood as milliseconds, ensuring compatibility with
+ old setting files. No users can possibly in their right mind want the user
+ interface to block for more than 100 seconds. *)
+fun smart_seconds r =
+ seconds (if r >= 100.0 then
+ (legacy_feature (quote auto_tools_time_limitN ^
+ " expressed in milliseconds -- use seconds instead"); 0.001 * r)
+ else
+ r)
+
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- case !time_limit of
- 0 => state
- | ms =>
- TimeLimit.timeLimit (Time.fromMilliseconds ms)
- (fn () =>
- if interact andalso not (!Toplevel.quiet) then
- fold_rev (fn (_, tool) => fn (true, state) => (true, state)
- | (false, state) => tool state)
- (Data.get (Proof.theory_of state)) (false, state) |> snd
- else
- state) ()
- handle TimeLimit.TimeOut => state))
+ if interact andalso not (!Toplevel.quiet) andalso !time_limit > 0.0 then
+ TimeLimit.timeLimit (smart_seconds (!time_limit))
+ (run_tools (Data.get (Proof.theory_of state))) state
+ handle TimeLimit.TimeOut => state
+ else
+ state))
end;
--- a/src/Tools/quickcheck.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/quickcheck.ML Fri Dec 03 17:18:41 2010 +0100
@@ -10,6 +10,7 @@
(* configuration *)
val auto: bool Unsynchronized.ref
val timing : bool Unsynchronized.ref
+ val tester : string Config.T
val size : int Config.T
val iterations : int Config.T
val no_assms : bool Config.T
@@ -27,16 +28,14 @@
val map_test_params : (typ list * expectation -> typ list * expectation)
-> Context.generic -> Context.generic
val add_generator:
- string * (Proof.context -> term -> int -> term list option * (bool list * bool))
+ string * (Proof.context -> term -> int -> term list option * report option)
-> Context.generic -> Context.generic
(* testing terms and proof states *)
- val test_term_small: Proof.context -> term ->
- (string * term) list option * ((string * int) list * ((int * report list) list) option)
- val test_term: Proof.context -> string option -> term ->
- (string * term) list option * ((string * int) list * ((int * report list) list) option)
+ val test_term: Proof.context -> bool -> term ->
+ (string * term) list option * ((string * int) list * ((int * report) list) option)
val test_goal_terms:
- Proof.context -> string option * (string * typ) list -> term list
- -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
+ Proof.context -> bool -> (string * typ) list -> term list
+ -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
end;
@@ -58,26 +57,10 @@
(* quickcheck report *)
-datatype single_report = Run of bool list * bool | MatchExc
-
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
-fun collect_single_report single_report
- (Report {iterations = iterations, raised_match_errors = raised_match_errors,
- satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
- case single_report
- of MatchExc =>
- Report {iterations = iterations + 1, raised_match_errors = raised_match_errors + 1,
- satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}
- | Run (assms, concl) =>
- Report {iterations = iterations + 1, raised_match_errors = raised_match_errors,
- satisfied_assms =
- map2 (fn b => fn s => if b then s + 1 else s) assms
- (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
- positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
-
(* expectation *)
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
@@ -86,6 +69,7 @@
if expect1 = expect2 then expect1 else No_Expectation
(* quickcheck configuration -- default parameters, test generators *)
+val (tester, setup_tester) = Attrib.config_string "quickcheck_tester" (K "")
val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
@@ -96,8 +80,8 @@
val (finite_type_size, setup_finite_type_size) = Attrib.config_int "quickcheck_finite_type_size" (K 3)
val setup_config =
- setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
- #> setup_finite_types #> setup_finite_type_size
+ setup_tester #> setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet
+ #> setup_timeout #> setup_finite_types #> setup_finite_type_size
datatype test_params = Test_Params of
{default_type: typ list, expect : expectation};
@@ -116,7 +100,7 @@
structure Data = Generic_Data
(
type T =
- (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
+ (string * (Proof.context -> term -> int -> term list option * report option)) list
* test_params;
val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
@@ -137,25 +121,23 @@
(* generating tests *)
-fun mk_tester_select name ctxt =
- case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
- of NONE => error ("No such quickcheck generator: " ^ name)
- | SOME generator => generator ctxt;
-
-fun mk_testers ctxt t =
- (map snd o fst o Data.get o Context.Proof) ctxt
- |> map_filter (fn generator => try (generator ctxt) t);
-
-fun mk_testers_strict ctxt t =
+fun mk_tester ctxt t =
let
- val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
- val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
+ val name = Config.get ctxt tester
+ val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name
+ of NONE => error ("No such quickcheck tester: " ^ name)
+ | SOME tester => tester ctxt;
in
- if forall (is_none o Exn.get_result) testers
- then [(Exn.release o snd o split_last) testers]
- else map_filter Exn.get_result testers
- end;
-
+ if Config.get ctxt quiet then
+ try tester t
+ else
+ let
+ val tester = Exn.interruptible_capture tester t
+ in case Exn.get_result tester of
+ NONE => SOME (Exn.release tester)
+ | SOME tester => SOME tester
+ end
+ end
(* testing propositions *)
@@ -174,96 +156,40 @@
val result = Exn.capture f ()
val time = Time.toMilliseconds (#cpu (end_timing start))
in (Exn.release result, (description, time)) end
-
-fun test_term_small ctxt t =
- let
- val (names, t') = prep_test_term t;
- val current_size = Unsynchronized.ref 0
- fun excipit s =
- "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
- val (tester, comp_time) = cpu_time "compilation"
- (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
- val empty_report = Report { iterations = 0, raised_match_errors = 0,
- satisfied_assms = [], positive_concl_tests = 0 }
- fun with_size k timings =
- if k > Config.get ctxt size then (NONE, timings)
- else
- let
- val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
- val _ = current_size := k
- val (result, timing) = cpu_time ("size " ^ string_of_int k)
- (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE))
- in
- case result of
- NONE => with_size (k + 1) (timing :: timings)
- | SOME q => (SOME q, (timing :: timings))
- end;
- val result = with_size 1 [comp_time]
- in
- apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
- end
-
-(* we actually assume we know the generators and its behaviour *)
-fun is_iteratable "SML" = true
- | is_iteratable "random" = true
- | is_iteratable _ = false
-fun test_term ctxt generator_name t =
+fun test_term ctxt is_interactive t =
let
val (names, t') = prep_test_term t;
val current_size = Unsynchronized.ref 0
fun excipit s =
"Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
- val (testers, comp_time) = cpu_time "quickcheck compilation"
- (fn () => (case generator_name
- of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
- | SOME name => [mk_tester_select name ctxt t']));
- fun iterate f 0 report = (NONE, report)
- | iterate f j report =
- let
- val (test_result, single_report) = apsnd Run (f ()) handle Match =>
- (if Config.get ctxt quiet then ()
- else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
- val report = collect_single_report single_report report
- in
- case test_result of NONE => iterate f (j - 1) report | SOME q => (SOME q, report)
- end
- val empty_report = Report { iterations = 0, raised_match_errors = 0,
- satisfied_assms = [], positive_concl_tests = 0 }
- fun with_testers k [] = (NONE, [])
- | with_testers k (tester :: testers) =
+ val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt t');
+ fun with_size test_fun k reports =
+ if k > Config.get ctxt size then
+ (NONE, reports)
+ else
let
- val niterations = case generator_name of
- SOME generator_name =>
- if is_iteratable generator_name then Config.get ctxt iterations else 1
- | NONE => Config.get ctxt iterations
- val (result, timing) = cpu_time ("size " ^ string_of_int k)
- (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
- in
- case result
- of (NONE, report) => apsnd (cons report) (with_testers k testers)
- | (SOME q, report) => (SOME q, [report])
- end
- fun with_size k reports =
- if k > Config.get ctxt size then (NONE, reports)
- else
- (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
- let
+ val _ = if Config.get ctxt quiet then () else Output.urgent_message
+ ("Test data size: " ^ string_of_int k)
val _ = current_size := k
- val (result, new_report) = with_testers k testers
- val reports = ((k, new_report) :: reports)
- in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
- val ((result, reports), exec_time) =
- TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
- (fn () => apfst
- (fn result => case result of NONE => NONE
- | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
- handle TimeLimit.TimeOut =>
- error (excipit "ran out of time")
- | Exn.Interrupt => error (excipit "was interrupted") (* FIXME violates Isabelle/ML exception model *)
+ val ((result, new_report), timing) =
+ cpu_time ("size " ^ string_of_int k) (fn () => test_fun (k - 1))
+ val reports = case new_report of NONE => reports | SOME rep => (k, rep) :: reports
+ in case result of NONE => with_size test_fun (k + 1) reports | SOME q => (SOME q, reports) end;
in
- (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
+ case test_fun of NONE => (NONE, ([comp_time], NONE))
+ | SOME test_fun =>
+ TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
+ let
+ val ((result, reports), exec_time) =
+ cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
+ in
+ (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
+ ([exec_time, comp_time],
+ if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
+ end) ()
+ handle TimeLimit.TimeOut =>
+ if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
end;
fun get_finite_types ctxt =
@@ -276,33 +202,34 @@
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
+ 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;
datatype wellsorted_error = Wellsorted_Error of string | Term of term
-fun test_goal_terms lthy (generator_name, insts) check_goals =
+fun test_goal_terms lthy is_interactive insts check_goals =
let
val thy = ProofContext.theory_of lthy
+ val default_insts =
+ if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy)
val inst_goals =
- if Config.get lthy finite_types then
- maps (fn check_goal => map (fn T =>
- Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
- handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
- else
- maps (fn check_goal => map (fn T =>
- Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
- handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
+ maps (fn check_goal =>
+ if not (null (Term.add_tfree_names check_goal [])) then
+ map (fn T =>
+ ((Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+ handle WELLSORTED s => Wellsorted_Error s) default_insts
+ else
+ [Term (Object_Logic.atomize_term thy check_goal)]) check_goals
val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
val correct_inst_goals =
case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
@@ -314,9 +241,9 @@
case f t of
(SOME res, report) => (SOME res, rev (report :: reports))
| (NONE, report) => collect_results f (report :: reports) ts
- in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
+ in collect_results (test_term lthy is_interactive) [] correct_inst_goals end;
-fun test_goal (generator_name, insts) i state =
+fun test_goal insts i state =
let
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -337,7 +264,7 @@
| SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
(Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
in
- test_goal_terms lthy (generator_name, insts) check_goals
+ test_goal_terms lthy true insts check_goals
end
(* pretty printing *)
@@ -348,7 +275,7 @@
| pretty_counterex ctxt auto (SOME cex) =
Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
+ Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex));
fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
@@ -362,16 +289,10 @@
@ [pretty_stat "positive conclusion tests" positive_concl_tests])
end
-fun pretty_reports' [report] = [Pretty.chunks (pretty_report report)]
- | pretty_reports' reports =
- map_index (fn (i, report) =>
- Pretty.chunks (Pretty.str (string_of_int (i + 1) ^ ". generator:\n") :: pretty_report report))
- reports
-
fun pretty_reports ctxt (SOME reports) =
- Pretty.chunks (Pretty.str "Quickcheck report:" ::
- maps (fn (size, reports) =>
- Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_reports' reports @ [Pretty.brk 1])
+ Pretty.chunks (Pretty.fbrk :: Pretty.str "Quickcheck report:" ::
+ maps (fn (size, report) =>
+ Pretty.str ("size " ^ string_of_int size ^ ":") :: pretty_report report @ [Pretty.brk 1])
(rev reports))
| pretty_reports ctxt NONE = Pretty.str ""
@@ -382,24 +303,21 @@
(* automatic testing *)
fun auto_quickcheck state =
- if not (!auto) then
- (false, state)
- else
- let
- val ctxt = Proof.context_of state;
- val res =
- state
- |> Proof.map_context (Config.put report false #> Config.put quiet true)
- |> try (test_goal (NONE, []) 1);
- in
- case res of
- NONE => (false, state)
- | SOME (NONE, report) => (false, state)
- | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
- end
+ let
+ val ctxt = Proof.context_of state;
+ val res =
+ state
+ |> Proof.map_context (Config.put report false #> Config.put quiet true)
+ |> try (test_goal [] 1);
+ in
+ case res of
+ NONE => (false, state)
+ | SOME (NONE, report) => (false, state)
+ | SOME (cex, report) => (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
+ Pretty.mark Markup.hilite (pretty_counterex ctxt true cex)])) state)
+ end
-val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
+val setup = Auto_Tools.register_tool (auto, auto_quickcheck)
#> setup_config
(* Isar commands *)
@@ -423,7 +341,16 @@
| read_expectation "counterexample" = Counterexample
| read_expectation s = error ("Not an expectation value: " ^ s)
-fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
+fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt))
+
+fun parse_tester name genctxt =
+ if valid_tester_name genctxt name then
+ Config.put_generic tester name genctxt
+ else
+ error ("Unknown tester: " ^ name)
+
+fun parse_test_param ("tester", [arg]) = parse_tester arg
+ | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
| parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
| parse_test_param ("default_type", arg) = (fn gen_ctxt =>
map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
@@ -434,22 +361,23 @@
| parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
| parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
| parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
- | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
+ | parse_test_param (name, _) = fn genctxt =>
+ if valid_tester_name genctxt name then
+ Config.put_generic tester name genctxt
+ else error ("Unknown tester or test parameter: " ^ name);
-fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
- (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
- | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
+fun parse_test_param_inst (name, arg) (insts, ctxt) =
case try (ProofContext.read_typ ctxt) name
- of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
- (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
- | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
+ of SOME (TFree (v, _)) => (apfst o AList.update (op =))
+ (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt)
+ | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt);
fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
fun gen_quickcheck args i state =
state
- |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
- |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
+ |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
+ |> (fn (insts, state') => test_goal insts i state'
|> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
error ("quickcheck expected to find no counterexample but found one") else ()
| (NONE, _) => if expect (Proof.context_of state') = Counterexample then
--- a/src/Tools/solve_direct.ML Fri Dec 03 17:16:53 2010 +0100
+++ b/src/Tools/solve_direct.ML Fri Dec 03 17:18:41 2010 +0100
@@ -97,9 +97,8 @@
(* hook *)
-fun auto_solve_direct state =
- if not (! auto) then (false, state) else solve_direct true state;
+val auto_solve_direct = solve_direct true
-val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct);
+val setup = Auto_Tools.register_tool (auto, auto_solve_direct);
end;