--- a/src/Tools/quickcheck.ML Mon Nov 22 10:42:06 2010 +0100
+++ b/src/Tools/quickcheck.ML Mon Nov 22 10:42:07 2010 +0100
@@ -10,18 +10,19 @@
(* configuration *)
val auto: bool Unsynchronized.ref
val timing : bool Unsynchronized.ref
+ val size : int Config.T
+ val iterations : int Config.T
+ val no_assms : bool Config.T
+ val report : bool Config.T
+ val quiet : bool Config.T
+ val timeout : real Config.T
datatype report = Report of
{ iterations : int, raised_match_errors : int,
satisfied_assms : int list, positive_concl_tests : int }
- datatype expectation = No_Expectation | No_Counterexample | Counterexample;
- datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : real};
+ datatype expectation = No_Expectation | No_Counterexample | Counterexample;
+ datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
val test_params_of : Proof.context -> test_params
- val report : Proof.context -> bool
- val map_test_params :
- ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
- -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
+ 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))
@@ -80,43 +81,36 @@
if expect1 = expect2 then expect1 else No_Expectation
(* quickcheck configuration -- default parameters, test generators *)
-
-datatype test_params = Test_Params of
- { size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool, timeout : real};
-
-fun dest_test_params
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))));
+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)
+val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
+val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
+val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
-fun make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) =
- Test_Params { size = size, iterations = iterations, default_type = default_type,
- no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout };
+val setup_config =
+ setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
+
+datatype test_params = Test_Params of
+ {default_type: typ list, expect : expectation};
-fun map_test_params' f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))));
+fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
+
+fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect};
+
+fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
fun merge_test_params
- (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 },
- Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) =
- make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
- ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
- ((merge_expectation (expect1, expect2), report1 orelse report2),
- (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
+ (Test_Params {default_type = default_type1, expect = expect1},
+ Test_Params {default_type = default_type2, expect = expect2}) =
+ make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
structure Data = Generic_Data
(
type T =
(string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
* test_params;
- val empty = ([], Test_Params
- { size = 10, iterations = 100, default_type = [], no_assms = false,
- expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
+ val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
fun merge ((generators1, params1), (generators2, params2)) : T =
(AList.merge (op =) (K true) (generators1, generators2),
@@ -125,35 +119,9 @@
val test_params_of = snd o Data.get o Context.Proof;
-val size = fst o fst o dest_test_params o test_params_of
-
-val iterations = snd o fst o dest_test_params o test_params_of
-
-val default_type = fst o fst o snd o dest_test_params o test_params_of
-
-val no_assms = snd o fst o snd o dest_test_params o test_params_of
-
-val expect = fst o fst o snd o snd o dest_test_params o test_params_of
-
-val report = snd o fst o snd o snd o dest_test_params o test_params_of
-
-val quiet = fst o snd o snd o snd o dest_test_params o test_params_of
+val default_type = fst o dest_test_params o test_params_of
-val timeout = snd o snd o snd o snd o dest_test_params o test_params_of
-
-fun map_report f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout))));
-
-fun map_quiet f
- (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
- make_test_params
- ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout))));
-
-fun set_report report = Data.map (apsnd (map_report (K report)))
-
-fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet)))
+val expect = snd o dest_test_params o test_params_of
val map_test_params = Data.map o apsnd o map_test_params'
@@ -210,12 +178,13 @@
val empty_report = Report { iterations = 0, raised_match_errors = 0,
satisfied_assms = [], positive_concl_tests = 0 }
fun with_size k timings =
- if k > size ctxt then (NONE, timings)
+ if k > Config.get ctxt size then (NONE, timings)
else
let
- val _ = if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+ 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 quiet ctxt then ()
+ 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
@@ -235,12 +204,13 @@
"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 quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
+ 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 quiet ctxt then ()
+ 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
@@ -250,20 +220,20 @@
satisfied_assms = [], positive_concl_tests = 0 }
fun with_testers k [] = (NONE, [])
| with_testers k (tester :: testers) =
- case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report
+ case iterate (fn () => tester (k - 1)) (Config.get ctxt iterations) empty_report
of (NONE, report) => apsnd (cons report) (with_testers k testers)
| (SOME q, report) => (SOME q, [report]);
fun with_size k reports =
- if k > size ctxt then (NONE, reports)
+ if k > Config.get ctxt size then (NONE, reports)
else
- (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
+ (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
let
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 (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
+ 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 []))) ()
@@ -271,7 +241,7 @@
error (excipit "ran out of time")
| Exn.Interrupt => error (excipit "was interrupted") (* FIXME violates Isabelle/ML exception model *)
in
- (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
+ (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
end;
exception WELLSORTED of string
@@ -294,7 +264,7 @@
datatype wellsorted_error = Wellsorted_Error of string | Term of term
-fun test_goal generator_name insts i state =
+fun test_goal (generator_name, insts) i state =
let
val lthy = Proof.context_of state;
val thy = Proof.theory_of state;
@@ -306,7 +276,7 @@
of NONE => NONE
| SOME "" => NONE
| SOME locale => SOME locale;
- val assms = if no_assms lthy then [] else case some_locale
+ val assms = if Config.get lthy no_assms then [] else case some_locale
of NONE => Assumption.all_assms_of lthy
| SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
@@ -322,7 +292,7 @@
case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
[] => error error_msg
| xs => xs
- val _ = if quiet lthy then () else warning error_msg
+ val _ = if Config.get lthy quiet then () else warning error_msg
fun collect_results f reports [] = (NONE, rev reports)
| collect_results f reports (t :: ts) =
case f t of
@@ -379,8 +349,8 @@
val ctxt = Proof.context_of state;
val res =
state
- |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true))
- |> try (test_goal NONE [] 1);
+ |> Proof.map_context (Config.put report false #> Config.put quiet true)
+ |> try (test_goal (NONE, []) 1);
in
case res of
NONE => (false, state)
@@ -390,7 +360,7 @@
end
val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
-
+ #> setup_config
(* Isar commands *)
@@ -413,57 +383,35 @@
| read_expectation "counterexample" = Counterexample
| read_expectation s = error ("Not an expectation value: " ^ s)
-fun parse_test_param ctxt ("size", [arg]) =
- (apfst o apfst o K) (read_nat arg)
- | parse_test_param ctxt ("iterations", [arg]) =
- (apfst o apsnd o K) (read_nat arg)
- | parse_test_param ctxt ("default_type", arg) =
- (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
- | parse_test_param ctxt ("no_assms", [arg]) =
- (apsnd o apfst o apsnd o K) (read_bool arg)
- | parse_test_param ctxt ("expect", [arg]) =
- (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
- | parse_test_param ctxt ("report", [arg]) =
- (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
- | parse_test_param ctxt ("quiet", [arg]) =
- (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
- | parse_test_param ctxt ("timeout", [arg]) =
- (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
- | parse_test_param ctxt (name, _) =
- error ("Unknown test parameter: " ^ name);
+fun 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)
+ | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
+ | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
+ | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
+ | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
+ | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
+ | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
-fun parse_test_param_inst ctxt ("generator", [arg]) =
- (apsnd o apfst o K o SOME) arg
- | parse_test_param_inst ctxt (name, arg) =
+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) =
case try (ProofContext.read_typ ctxt) name
- of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
- (v, ProofContext.read_typ ctxt (the_single arg))
- | _ => (apfst o parse_test_param ctxt) (name, arg);
+ 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);
-fun quickcheck_params_cmd args thy =
- let
- val ctxt = ProofContext.init_global thy
- val f = fold (parse_test_param ctxt) args;
- in
- thy
- |> (Context.theory_map o map_test_params) f
- end;
-
+fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
+
fun gen_quickcheck args i state =
- let
- val ctxt = Proof.context_of state;
- val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
- val f = fold (parse_test_param_inst ctxt) args;
- val (test_params, (generator_name, insts)) = f (default_params, (NONE, []));
- in
- state
- |> Proof.map_context (Context.proof_map (map_test_params (K test_params)))
- |> (fn state' => test_goal generator_name 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
- error ("quickcheck expected to find a counterexample but did not find one") else ()))
- end;
+ 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'
+ |> 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
+ error ("quickcheck expected to find a counterexample but did not find one") else ()))
fun quickcheck args i state = fst (gen_quickcheck args i state);