--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Dec 03 08:40:47 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/Tools/Predicate_Compile/code_prolog.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Dec 03 08:40:47 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 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Dec 03 08:40:47 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 =