# HG changeset patch # User bulwahn # Date 1310978061 -7200 # Node ID b8fa7287ee4ca2797312602a06da2a19b40816a9 # Parent 485d2ad43528bc35abcba7699028918a91c3c228 parametrized test_term functions in quickcheck diff -r 485d2ad43528 -r b8fa7287ee4c src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Library/SML_Quickcheck.thy Mon Jul 18 10:34:21 2011 +0200 @@ -6,9 +6,8 @@ begin setup {* - Inductive_Codegen.quickcheck_setup #> - Context.theory_map (Quickcheck.add_generator ("SML", - fn ctxt => fn [(t, eval_terms)] => + let + fun compile_generator_expr ctxt [(t, eval_terms)] = let val prop = list_abs_free (Term.add_frees t [], t) val test_fun = Codegen.test_term ctxt prop @@ -22,8 +21,13 @@ in case result of NONE => iterate size (j - 1) | SOME q => SOME q end - in fn [_, size] => (iterate size iterations, NONE) end)) - #> Context.theory_map (Quickcheck.add_tester ("SML", Quickcheck.generator_test_goal_terms)) + in fn [_, size] => (iterate size iterations, NONE) end)) + val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr + in + Inductive_Codegen.quickcheck_setup + #> Context.theory_map (Quickcheck.add_generator ("SML", compile_generator_expr)) + #> Context.theory_map (Quickcheck.add_tester ("SML", test_goals)) + end *} end diff -r 485d2ad43528 -r b8fa7287ee4c src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Jul 18 10:34:21 2011 +0200 @@ -488,7 +488,7 @@ thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] end; -val test_goals = Quickcheck.generator_test_goal_terms; +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr; (* setup *) diff -r 485d2ad43528 -r b8fa7287ee4c src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Jul 18 10:34:21 2011 +0200 @@ -438,7 +438,7 @@ end end; -val test_goals = Quickcheck.generator_test_goal_terms; +val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr; (** setup **) diff -r 485d2ad43528 -r b8fa7287ee4c src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200 +++ b/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200 @@ -56,17 +56,18 @@ string * (Proof.context -> term list -> (int -> bool) list) -> Context.generic -> Context.generic (* basic operations *) + type compile_generator = + Proof.context -> (term * term list) list -> int list -> term list option * report option val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list -> (typ option * (term * term list)) list list val collect_results: ('a -> result) -> 'a list -> result list -> result list - val generator_test_goal_terms: Proof.context -> bool * bool -> (string * typ) list -> - (term * term list) list -> result list + val generator_test_goal_terms: compile_generator -> + Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list (* testing terms and proof states *) - val test_term: Proof.context -> bool * bool -> term * term list -> result + val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result val test_goal_terms: - Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list - -> result list + Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option (* testing a batch of terms *) val test_terms: @@ -246,9 +247,10 @@ | SOME tester => SOME tester end end - +(* val mk_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o fst o fst o Data.get o Context.Proof) ctxt)) +*) val mk_batch_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt)) val mk_batch_validator = @@ -259,6 +261,9 @@ (* testing propositions *) +type compile_generator = + Proof.context -> (term * term list) list -> int list -> term list option * report option + fun check_test_term t = let val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse @@ -279,7 +284,7 @@ else f () -fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) = +fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) = let fun message s = if Config.get ctxt quiet then () else Output.urgent_message s val _ = check_test_term t @@ -306,21 +311,14 @@ limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => let val (test_fun, comp_time) = cpu_time "quickcheck compilation" - (fn () => mk_tester ctxt [(t, eval_terms)]); + (fn () => compile ctxt [(t, eval_terms)]); val _ = add_timing comp_time current_result - in - case test_fun of NONE => !current_result - | SOME test_fun => - let - val (response, exec_time) = - cpu_time "quickcheck execution" (fn () => with_size test_fun 1) - val _ = add_response names eval_terms response current_result - val _ = add_timing exec_time current_result - in - !current_result - end - end) - (fn () => (message (excipit ()); !current_result)) () + val (response, exec_time) = + cpu_time "quickcheck execution" (fn () => with_size test_fun 1) + val _ = add_response names eval_terms response current_result + val _ = add_timing exec_time current_result + in !current_result end) + (fn () => (message (excipit ()); !current_result)) () end; fun validate_terms ctxt ts = @@ -361,7 +359,7 @@ (* FIXME: this function shows that many assumptions are made upon the generation *) (* In the end there is probably no generic quickcheck interface left... *) -fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts = +fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts = let val thy = Proof_Context.theory_of ctxt fun message s = if Config.get ctxt quiet then () else Output.urgent_message s @@ -390,18 +388,12 @@ in limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () => let - val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts) - val _ = add_timing comp_time current_result - in - case test_fun of - NONE => !current_result - | SOME test_fun => - let - val _ = case get_first (test_card_size test_fun) enumeration_card_size of - SOME (card, ts) => add_response names (nth eval_terms (card - 1)) (SOME ts) current_result - | NONE => () - in !current_result end - end) + val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => compile ctxt ts) + val _ = add_timing comp_time current_result + val _ = case get_first (test_card_size test_fun) enumeration_card_size of + SOME (card, ts) => 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)) () end @@ -471,18 +463,18 @@ collect_results f ts (result :: results) end -fun generator_test_goal_terms ctxt (limit_time, is_interactive) insts goals = +fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals = let fun test_term' goal = case goal of - [(NONE, t)] => test_term ctxt (limit_time, is_interactive) t - | ts => test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) (map snd ts) + [(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) val correct_inst_goals = instantiate_goals ctxt insts goals in if Config.get ctxt finite_types then collect_results test_term' correct_inst_goals [] else - collect_results (test_term ctxt (limit_time, is_interactive)) + collect_results (test_term compile ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] end;