# HG changeset patch # User wenzelm # Date 1288343241 -7200 # Node ID f99ec71de82db6486451075945df4159f2003863 # Parent 029400b6c8939df698f0333eb1b9c4fb9884e797# Parent bb433b0668b898acaaea1734e8a61af86559dd8d merged diff -r bb433b0668b8 -r f99ec71de82d NEWS --- a/NEWS Thu Oct 28 23:54:39 2010 +0200 +++ b/NEWS Fri Oct 29 11:07:21 2010 +0200 @@ -76,6 +76,11 @@ *** HOL *** +* Quickcheck now has a configurable time limit which is set to 30 seconds +by default. This can be changed by adding [timeout = n] to the quickcheck +command. The time limit for auto quickcheck is still set independently, +by default to 5 seconds. + * New command 'partial_function' provides basic support for recursive function definitions over complete partial orders. Concrete instances are provided for i) the option type, ii) tail recursion on arbitrary diff -r bb433b0668b8 -r f99ec71de82d doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Oct 28 23:54:39 2010 +0200 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 29 11:07:21 2010 +0200 @@ -950,6 +950,20 @@ \item[no\_assms] specifies whether assumptions in structured proofs should be ignored. + \item[timeout] sets the time limit in seconds. + + \item[default\_type] sets the type(s) generally used to instantiate + type variables. + + \item[report] if set quickcheck reports how many tests fulfilled + the preconditions. + + \item[quiet] if not set quickcheck informs about the current size + for assignment values. + + \item[expect] can be used to check if the user's expectation was met + (no\_expectation, no\_counterexample, or counterexample) + \end{description} These option can be given within square brackets. diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Complete_Partial_Order.thy --- a/src/HOL/Complete_Partial_Order.thy Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Complete_Partial_Order.thy Fri Oct 29 11:07:21 2010 +0200 @@ -258,6 +258,6 @@ end - +hide_const (open) lub iterates fixp admissible end diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Oct 29 11:07:21 2010 +0200 @@ -1279,7 +1279,7 @@ subsubsection {* Monotonicity of multiset union *} lemma mult1_union: - "(B, D) \ mult1 r ==> trans r ==> (C + B, C + D) \ mult1 r" + "(B, D) \ mult1 r ==> (C + B, C + D) \ mult1 r" apply (unfold mult1_def) apply auto apply (rule_tac x = a in exI) @@ -1290,8 +1290,8 @@ lemma union_less_mono2: "B \# D ==> C + B \# C + (D::'a::order multiset)" apply (unfold less_multiset_def mult_def) apply (erule trancl_induct) - apply (blast intro: mult1_union transI order_less_trans r_into_trancl) -apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans) + apply (blast intro: mult1_union) +apply (blast intro: mult1_union trancl_trans) done lemma union_less_mono1: "B \# D ==> B + C \# D + (C::'a::order multiset)" diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle.ML Fri Oct 29 11:07:21 2010 +0200 @@ -497,15 +497,19 @@ (map_types (inst_type insts) (freeze t)); fun is_executable thy insts th = - (Quickcheck.test_term - (ProofContext.init_global thy) false (SOME (!testgen_name)) 1 1 (preprocess thy insts (prop_of th)); - Output.urgent_message "executable"; true) handle ERROR s => - (Output.urgent_message ("not executable: " ^ s); false); + ((Quickcheck.test_term + (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 1)))) (ProofContext.init_global thy)) + (SOME (!testgen_name)) (preprocess thy insts (prop_of th)); + Output.urgent_message "executable"; true) handle ERROR s => + (Output.urgent_message ("not executable: " ^ s); false)); fun qc_recursive usedthy [] insts sz qciter acc = rev acc | 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 [] (Quickcheck.test_term - (ProofContext.init_global usedthy) false (SOME (!testgen_name)) sz qciter (preprocess usedthy insts x)))) :: acc)) + (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); + ((x, pretty (the_default [] (fst (Quickcheck.test_term + (Context.proof_map (Quickcheck.map_test_params (apfst (K (sz, qciter)))) + (ProofContext.init_global usedthy)) + (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc)) handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc); diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Oct 29 11:07:21 2010 +0200 @@ -53,8 +53,6 @@ (* quickcheck options *) (*val quickcheck_generator = "SML"*) -val iterations = 10 -val size = 5 exception RANDOM; @@ -96,8 +94,8 @@ fun invoke_quickcheck quickcheck_generator thy t = TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit)) (fn _ => - case Quickcheck.gen_test_term (ProofContext.init_global thy) true (SOME quickcheck_generator) - size iterations (preprocess thy [] t) of + case Quickcheck.test_term (ProofContext.init_global thy) + (SOME quickcheck_generator) (preprocess thy [] t) of (NONE, (time_report, report)) => (NoCex, (time_report, report)) | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) () handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE)) @@ -249,8 +247,12 @@ exists (member (op =) forbidden_mutant_constnames) consts end -fun is_executable_term thy t = can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) (Quickcheck.test_term - (ProofContext.init_global thy) false (SOME "SML") 1 0)) (preprocess thy [] t) +fun is_executable_term thy t = + can (TimeLimit.timeLimit (Time.fromMilliseconds 2000) + (Quickcheck.test_term + (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy)) + (SOME "SML"))) (preprocess thy [] t) + fun is_executable_thm thy th = is_executable_term thy (prop_of th) val freezeT = @@ -422,6 +424,7 @@ fun mutate_theorems_and_write_report thy mtds thms file_name = let val _ = Output.urgent_message "Starting Mutabelle..." + val Quickcheck.Test_Params test_params = Quickcheck.test_params_of (ProofContext.init_global thy) val path = Path.explode file_name (* for normal report: *) (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*) @@ -437,8 +440,8 @@ "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^ "QC options = " ^ (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*) - "size: " ^ string_of_int size ^ - "; iterations: " ^ string_of_int iterations ^ "\n"); + "size: " ^ string_of_int (#size test_params) ^ + "; iterations: " ^ string_of_int (#iterations test_params) ^ "\n"); map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms; () end diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Partial_Function.thy --- a/src/HOL/Partial_Function.thy Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Partial_Function.thy Fri Oct 29 11:07:21 2010 +0200 @@ -242,6 +242,7 @@ show "option_ord (Option.bind (B f) (\y. C y f)) (Option.bind (B g) (\y'. C y' g))" . qed +hide_const (open) chain end diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Predicate_Compile_Examples/ROOT.ML --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Fri Oct 29 11:07:21 2010 +0200 @@ -12,11 +12,12 @@ if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then (warning "No prolog system found - skipping some example theories"; ()) else - (use_thys [ - "Code_Prolog_Examples", - "Context_Free_Grammar_Example", - "Hotel_Example_Prolog", - "Lambda_Example", - "List_Examples"]; - Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]); - + if not (getenv "EXEC_SWIPL" = "") orelse (getenv "SWIPL_VERSION" = "5.10.1") then + (use_thys [ + "Code_Prolog_Examples", + "Context_Free_Grammar_Example", + "Hotel_Example_Prolog", + "Lambda_Example", + "List_Examples"]; + Unsynchronized.setmp quick_and_dirty true use_thys ["Reg_Exp_Example"]) + else (warning "Unsupported SWI-Prolog version - skipping some example theories"; ()); diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Tools/Predicate_Compile/etc/settings --- a/src/HOL/Tools/Predicate_Compile/etc/settings Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/etc/settings Fri Oct 29 11:07:21 2010 +0200 @@ -1,13 +1,16 @@ EXEC_SWIPL=$(choosefrom \ - "$ISABELLE_HOME/contrib/swipl/bin/swipl" \ - "$ISABELLE_HOME/contrib_devel/swipl/bin/swipl" \ + "$ISABELLE_HOME/contrib/swipl/$ISABELLE_PLATFORM/bin/swipl" \ + "$ISABELLE_HOME/contrib_devel/swipl/$ISABELLE_PLATFORM/bin/swipl" \ "$ISABELLE_HOME/../swipl" \ $(type -p swipl) \ "") EXEC_YAP=$(choosefrom \ - "$ISABELLE_HOME/contrib/yap" \ + "$ISABELLE_HOME/contrib/yap/$ISABELLE_PLATFORM/bin/yap" \ + "$ISABELLE_HOME/contrib_devel/yap/$ISABELLE_PLATFORM/bin/yap" \ "$ISABELLE_HOME/../yap" \ $(type -p yap) \ "") + +SWIPL_VERSION=$("$COMPONENT/lib/scripts/swipl_version") diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Fri Oct 29 11:07:21 2010 +0200 @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +# +# Author: Lukas Bulwahn, TU Muenchen, 2010 +# +# Determine SWI-Prolog version + +if [ "$EXEC_SWIPL" = "" ]; then + echo "" +else + VERSION=`$EXEC_SWIPL --version` + echo `expr match "$VERSION" 'SWI-Prolog version \([0-9\.]*\)'` +fi diff -r bb433b0668b8 -r f99ec71de82d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Oct 28 23:54:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Oct 29 11:07:21 2010 +0200 @@ -87,8 +87,8 @@ val theory_const_suffix = Long_Name.separator ^ " 1" fun needs_quoting reserved s = - Symtab.defined reserved s orelse - exists (not o Syntax.is_identifier) (Long_Name.explode s) + Symtab.defined reserved s (* FIXME: orelse + exists (not o Syntax.is_identifier) (Long_Name.explode s) *) fun repair_name reserved multi j name = (name |> needs_quoting reserved name ? quote) ^ diff -r bb433b0668b8 -r f99ec71de82d src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Oct 28 23:54:39 2010 +0200 +++ b/src/Tools/quickcheck.ML Fri Oct 29 11:07:21 2010 +0200 @@ -1,5 +1,5 @@ (* Title: Tools/quickcheck.ML - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + Author: Stefan Berghofer, Florian Haftmann, Lukas Bulwahn, TU Muenchen Generic counterexample search engine. *) @@ -16,18 +16,19 @@ 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}; - val test_params_of: Proof.context -> test_params + expect : expectation, report: bool, quiet : bool, timeout : int}; + val test_params_of : Proof.context -> test_params val report : Proof.context -> bool - val set_reporting : bool -> Context.generic -> Context.generic + val map_test_params : + ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int))) + -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * int)))) + -> Context.generic -> Context.generic val add_generator: string * (Proof.context -> term -> int -> term list option * (bool list * bool)) -> Context.generic -> Context.generic (* testing terms and proof states *) - val gen_test_term: Proof.context -> bool -> string option -> int -> int -> term -> + 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 -> string option -> int -> int -> term -> - (string * term) list option val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option end; @@ -80,26 +81,31 @@ datatype test_params = Test_Params of { size: int, iterations: int, default_type: typ list, no_assms: bool, - expect : expectation, report: bool, quiet : bool}; + expect : expectation, report: bool, quiet : bool, timeout : int}; -fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = - ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))); +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)))); -fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) = +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 }; + no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout }; -fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = - make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)))); +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 merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1, - no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 }, + 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 }) = + 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))); + ((merge_expectation (expect1, expect2), report1 orelse report2), + (quiet1 orelse quiet2, Int.min (timeout1, timeout2))))); structure Data = Generic_Data ( @@ -108,7 +114,7 @@ * test_params; val empty = ([], Test_Params { size = 10, iterations = 100, default_type = [], no_assms = false, - expect = No_Expectation, report = false, quiet = false}); + expect = No_Expectation, report = false, quiet = false, timeout = 30}); val extend = I; fun merge ((generators1, params1), (generators2, params2)) : T = (AList.merge (op =) (K true) (generators1, generators2), @@ -117,12 +123,37 @@ 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 -fun map_report f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) = - make_test_params ((size, iterations), ((default_type, no_assms), ((expect, f report), quiet))); +val quiet = fst o snd o snd o snd 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 set_reporting report = Data.map (apsnd (map_report (K report))) +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 map_test_params = Data.map o apsnd o map_test_params' val add_generator = Data.map o apfst o AList.update (op =); @@ -166,17 +197,17 @@ val time = Time.toMilliseconds (#cpu (end_timing start)) in (Exn.release result, (description, time)) end -fun gen_test_term ctxt quiet generator_name size i t = +fun test_term ctxt generator_name t = let val (names, t') = prep_test_term t; val (testers, comp_time) = cpu_time "quickcheck compilation" (fn () => (case generator_name - of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' + of NONE => if quiet ctxt 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 then () + val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then () else warning "Exception Match raised during quickcheck"; (NONE, MatchExc)) val report = collect_single_report single_report report in @@ -186,19 +217,19 @@ satisfied_assms = [], positive_concl_tests = 0 } fun with_testers k [] = (NONE, []) | with_testers k (tester :: testers) = - case iterate (fn () => tester (k - 1)) i empty_report + case iterate (fn () => tester (k - 1)) (iterations ctxt) 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 then (NONE, reports) + if k > size ctxt then (NONE, reports) else - (if quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k); + (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k); let 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 (Time.fromSeconds 20) (fn () => cpu_time "quickcheck execution" + TimeLimit.timeLimit (Time.fromSeconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution" (fn () => apfst (fn result => case result of NONE => NONE | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) () @@ -207,11 +238,6 @@ (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE)) end; -fun test_term ctxt quiet generator_name size i t = - ctxt - |> Context.proof_map (set_reporting false) - |> (fn ctxt' => fst (gen_test_term ctxt' quiet generator_name size i t)) - exception WELLSORTED of string fun monomorphic_term thy insts default_T = @@ -232,7 +258,7 @@ datatype wellsorted_error = Wellsorted_Error of string | Term of term -fun test_goal quiet generator_name size iterations default_Ts no_assms insts i state = +fun test_goal generator_name insts i state = let val lthy = Proof.context_of state; val thy = Proof.theory_of state; @@ -244,28 +270,29 @@ of NONE => NONE | SOME "" => NONE | SOME locale => SOME locale; - val assms = if no_assms then [] else case some_locale + val assms = if no_assms lthy 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)); val check_goals = case some_locale of NONE => [proto_goal] - | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); + | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) + (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); val inst_goals = 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_Ts) check_goals + handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) 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 [] => error error_msg | xs => xs - val _ = if quiet then () else warning error_msg + val _ = if quiet lthy then () else warning error_msg fun collect_results f reports [] = (NONE, rev reports) | collect_results f reports (t :: ts) = case f t of (SOME res, report) => (SOME res, rev (report :: reports)) | (NONE, report) => collect_results f (report :: reports) ts - in collect_results (gen_test_term lthy quiet generator_name size iterations) [] correct_inst_goals end; + in collect_results (test_term lthy generator_name) [] correct_inst_goals end; (* pretty printing *) @@ -314,12 +341,10 @@ else let val ctxt = Proof.context_of state; - val Test_Params {size, iterations, default_type, no_assms, ...} = - (snd o Data.get o Context.Proof) ctxt; val res = state - |> Proof.map_context (Context.proof_map (set_reporting false)) - |> try (test_goal true NONE size iterations default_type no_assms [] 1); + |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true)) + |> try (test_goal NONE [] 1); in case res of NONE => (false, state) @@ -360,7 +385,9 @@ | 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 K) (read_bool 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_nat arg) | parse_test_param ctxt (name, _) = error ("Unknown test parameter: " ^ name); @@ -378,7 +405,7 @@ val f = fold (parse_test_param ctxt) args; in thy - |> (Context.theory_map o Data.map o apsnd o map_test_params) f + |> (Context.theory_map o map_test_params) f end; fun gen_quickcheck args i state = @@ -386,16 +413,15 @@ 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 (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) = - f (default_params, (NONE, [])); + val (test_params, (generator_name, insts)) = f (default_params, (NONE, [])); in state - |> Proof.map_context (Context.proof_map (set_reporting report)) - |> test_goal quiet generator_name size iterations default_type no_assms insts i - |> tap (fn (SOME x, _) => if expect = No_Counterexample then + |> 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 = Counterexample then - error ("quickcheck expected to find a counterexample but did not find 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; fun quickcheck args i state = fst (gen_quickcheck args i state);