# HG changeset patch # User huffman # Date 1320849214 -3600 # Node ID 1006cba234e3be5682a8bfe4e3c5c473d7cc0eb9 # Parent 958d19d3405bf152ab01dbc8c379956249f9b064# Parent d17556b9a89bb38d390e575bae21cf20104266f7 merged diff -r 958d19d3405b -r 1006cba234e3 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 09 15:33:24 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Wed Nov 09 15:33:34 2011 +0100 @@ -488,7 +488,7 @@ thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] end; -val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; +val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr); (* setup *) diff -r 958d19d3405b -r 1006cba234e3 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 15:33:24 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 15:33:34 2011 +0100 @@ -10,7 +10,7 @@ val finite_functions : bool Config.T val overlord : bool Config.T val active : bool Config.T - val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result + val test_term: Proof.context -> term * term list -> Quickcheck.result datatype counterexample = Universal_Counterexample of (term * counterexample) | Existential_Counterexample of (term * counterexample) list | Empty_Assignment @@ -222,9 +222,8 @@ let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end -fun value (contains_existentials, opts) ctxt cookie (code, value_name) = +fun value (contains_existentials, (quiet, size)) ctxt cookie (code, value_name) = let - val (limit_time, is_interactive, timeout, quiet, size) = opts val (get, put, put_ml) = cookie fun message s = if quiet then () else Output.urgent_message s val current_size = Unsynchronized.ref 0 @@ -264,7 +263,7 @@ (NONE, !current_result) else let - val _ = message ("[Quickcheck-Narrowing] Test data size: " ^ string_of_int k) + val _ = message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k) val _ = current_size := k val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k) (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k)) @@ -286,9 +285,7 @@ end in with_size 0 end in - (*Quickcheck.limit timeout (limit_time, is_interactive) - (fn () =>*) with_tmp_dir tmp_prefix run - (*(fn () => (message (excipit ()); (NONE, !current_result))) ()*) + with_tmp_dir tmp_prefix run end; fun dynamic_value_strict opts cookie thy postproc t = @@ -414,12 +411,11 @@ |> map (apsnd post_process) end -fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = +fun test_term ctxt (t, eval_terms) = let fun dest_result (Quickcheck.Result r) = r val opts = - (limit_time, is_interactive, seconds (Config.get ctxt Quickcheck.timeout), - Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size) + (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size) val thy = Proof_Context.theory_of ctxt val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t val pnf_t = make_pnf_term thy t' @@ -460,12 +456,12 @@ end end; -fun test_goals ctxt (limit_time, is_interactive) insts goals = +fun test_goals ctxt _ insts goals = if (not (getenv "ISABELLE_GHC" = "")) then let val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals in - Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] + Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) [] end else (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message diff -r 958d19d3405b -r 1006cba234e3 src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 15:33:24 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 15:33:34 2011 +0100 @@ -16,8 +16,9 @@ val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list type compile_generator = Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option - val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool - -> (string * typ) list -> (term * term list) list -> Quickcheck.result list + val generator_test_goal_terms : + string * compile_generator -> Proof.context -> bool -> (string * typ) list + -> (term * term list) list -> Quickcheck.result list val ensure_sort_datatype: ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory) @@ -27,7 +28,8 @@ -> Proof.context -> (term * term list) list -> term val mk_fun_upd : typ -> typ -> term * term -> term -> term val post_process_term : term -> term - val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result + val test_term : string * compile_generator + -> Proof.context -> bool -> term * term list -> Quickcheck.result end; structure Quickcheck_Common : QUICKCHECK_COMMON = @@ -61,7 +63,7 @@ let val ({cpu, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds cpu)) end -fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) = +fun test_term (name, compile) ctxt catch_code_errors (t, eval_terms) = let val _ = check_test_term t val names = Term.add_free_names t [] @@ -74,7 +76,8 @@ NONE else let - val _ = Quickcheck.message ctxt ("Test data size: " ^ string_of_int k) + val _ = Quickcheck.message ctxt + ("[Quickcheck-" ^ name ^ "]Test data size: " ^ string_of_int k) val _ = current_size := k val ((result, report), timing) = cpu_time ("size " ^ string_of_int k) (fn () => test_fun [1, k - 1]) @@ -83,18 +86,21 @@ in case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q end; + val act = if catch_code_errors then try else (fn f => SOME o f) + val (test_fun, comp_time) = cpu_time "quickcheck compilation" + (fn () => act (compile ctxt) [(t, eval_terms)]); + val _ = Quickcheck.add_timing comp_time current_result in - (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( + case test_fun of + NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); + !current_result) + | SOME test_fun => let - val (test_fun, comp_time) = cpu_time "quickcheck compilation" - (fn () => compile ctxt [(t, eval_terms)]); - val _ = Quickcheck.add_timing comp_time current_result val (response, exec_time) = cpu_time "quickcheck execution" (fn () => with_size test_fun 1) val _ = Quickcheck.add_response names eval_terms response current_result val _ = Quickcheck.add_timing exec_time current_result - in !current_result end) -(* (fn () => (message (excipit ()); !current_result)) ()*) + in !current_result end end; fun validate_terms ctxt ts = @@ -107,7 +113,8 @@ if k > size then true else if tester k then with_size tester (k + 1) else false val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) + Option.map (map (fn test_fun => + TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) (fn () => with_size test_fun 1) () handle TimeLimit.TimeOut => true)) test_funs) in @@ -125,7 +132,8 @@ if k > size then NONE else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) + Option.map (map (fn test_fun => + TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) (fn () => with_size test_fun 1) () handle TimeLimit.TimeOut => NONE)) test_funs) in @@ -134,7 +142,7 @@ end -fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts = +fun test_term_with_cardinality (name, compile) ctxt catch_code_errors ts = let val thy = Proof_Context.theory_of ctxt val (ts', eval_terms) = split_list ts @@ -160,22 +168,25 @@ (* size does matter *) map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size)) |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2))) + val act = if catch_code_errors then try else (fn f => SOME o f) + val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts) + val _ = Quickcheck.add_timing comp_time current_result in - (*limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>*)( + case test_fun of + NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name); + !current_result) + | SOME test_fun => let - val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts) - val _ = Quickcheck.add_timing comp_time current_result val _ = case get_first (test_card_size test_fun) enumeration_card_size of SOME (card, ts) => Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME ts) current_result | NONE => () - in !current_result end) - (*(fn () => (message "Quickcheck ran out of time"; !current_result)) ()*) + in !current_result end end fun get_finite_types ctxt = fst (chop (Config.get ctxt Quickcheck.finite_type_size) - (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3", - "Enum.finite_4", "Enum.finite_5"])) + [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"}, + @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}]) exception WELLSORTED of string @@ -203,14 +214,14 @@ fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) val thy = Proof_Context.theory_of lthy val default_insts = - if Config.get lthy Quickcheck.finite_types then (get_finite_types lthy) else (Quickcheck.default_type lthy) + if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type val inst_goals = map (fn (check_goal, eval_terms) => if not (null (Term.add_tfree_names check_goal [])) then map (fn T => (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) - handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts + handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) else [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals val error_msg = @@ -243,19 +254,19 @@ SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs]) | NONE => (t, eval_terms) -fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals = +fun generator_test_goal_terms (name, compile) ctxt catch_code_errors insts goals = let fun test_term' goal = case goal of - [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t - | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts) + [(NONE, t)] => test_term (name, compile) ctxt catch_code_errors t + | ts => test_term_with_cardinality (name, compile) ctxt catch_code_errors (map snd ts) val goals' = instantiate_goals ctxt insts goals |> map (map (apsnd add_equation_eval_terms)) in if Config.get ctxt Quickcheck.finite_types then collect_results test_term' goals' [] else - collect_results (test_term compile ctxt (limit_time, is_interactive)) + collect_results (test_term (name, compile) ctxt catch_code_errors) (maps (map snd) goals') [] end; @@ -407,6 +418,5 @@ | NONE => process_args t) | _ => process_args t end - end; diff -r 958d19d3405b -r 1006cba234e3 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Wed Nov 09 15:33:24 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Wed Nov 09 15:33:34 2011 +0100 @@ -438,7 +438,7 @@ end end; -val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; +val test_goals = Quickcheck_Common.generator_test_goal_terms ("random", compile_generator_expr); (** setup **) diff -r 958d19d3405b -r 1006cba234e3 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Wed Nov 09 15:33:24 2011 +0100 +++ b/src/Tools/quickcheck.ML Wed Nov 09 15:33:34 2011 +0100 @@ -50,7 +50,7 @@ val timings_of : result -> (string * int) list (* registering testers & generators *) type tester = - Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list + Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic val add_batch_generator : string * (Proof.context -> term list -> (int -> term list option) list) @@ -192,7 +192,7 @@ (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2)); type tester = - Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list + Proof.context -> bool -> (string * typ) list -> (term * term list) list -> result list structure Data = Generic_Data ( @@ -288,7 +288,7 @@ [] => error "No active testers for quickcheck" | testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => Par_List.get_some (fn tester => - tester ctxt (limit_time, is_interactive) insts goals |> + tester ctxt (length testers > 1) insts goals |> (fn result => if exists found_counterexample result then SOME result else NONE)) testers) (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();