# HG changeset patch # User bulwahn # Date 1298916384 -3600 # Node ID a38536bf273629abc0ae79cc0474e0fb6ff02249 # Parent 77d87dc50e5a0de7371897cb3f664435286aa16b adding function Quickcheck.test_terms to provide checking a batch of terms diff -r 77d87dc50e5a -r a38536bf2736 src/HOL/Tools/smallvalue_generators.ML --- a/src/HOL/Tools/smallvalue_generators.ML Mon Feb 28 19:06:23 2011 +0100 +++ b/src/HOL/Tools/smallvalue_generators.ML Mon Feb 28 19:06:24 2011 +0100 @@ -9,7 +9,7 @@ val compile_generator_expr: Proof.context -> term -> int -> term list option * Quickcheck.report option val compile_generator_exprs: - Proof.context -> term list -> (int -> term list option * Quickcheck.report option) list + Proof.context -> term list -> (int -> term list option) list val put_counterexample: (unit -> int -> term list option) -> Proof.context -> Proof.context val put_counterexample_batch: (unit -> (int -> term list option) list) @@ -365,8 +365,7 @@ thy (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc)) (HOLogic.mk_list @{typ "code_numeral => term list option"} ts') []; in - map (fn compile => fn size => rpair NONE (compile size |> Option.map (map post_process_term))) - compiles + map (fn compile => fn size => compile size |> Option.map (map post_process_term)) compiles end; @@ -377,6 +376,8 @@ (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype)) #> setup_smart_quantifier #> Context.theory_map - (Quickcheck.add_generator ("exhaustive", compile_generator_expr)); + (Quickcheck.add_generator ("exhaustive", compile_generator_expr)) + #> Context.theory_map + (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs)); end; diff -r 77d87dc50e5a -r a38536bf2736 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Mon Feb 28 19:06:23 2011 +0100 +++ b/src/Tools/quickcheck.ML Mon Feb 28 19:06:24 2011 +0100 @@ -30,6 +30,9 @@ val add_generator: string * (Proof.context -> term -> int -> term list option * report option) -> Context.generic -> Context.generic + val add_batch_generator: + string * (Proof.context -> term list -> (int -> term list option) list) + -> Context.generic -> Context.generic (* testing terms and proof states *) val test_term: Proof.context -> bool * bool -> term -> (string * term) list option * ((string * int) list * ((int * report) list) option) @@ -37,6 +40,8 @@ Proof.context -> bool * bool -> (string * typ) list -> term list -> (string * term) list option * ((string * int) list * ((int * report) list) option) list val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option + (* testing a batch of terms *) + val test_terms: Proof.context -> term list -> (string * term) list option list option end; structure Quickcheck : QUICKCHECK = @@ -104,12 +109,14 @@ structure Data = Generic_Data ( type T = - (string * (Proof.context -> term -> int -> term list option * report option)) list + ((string * (Proof.context -> term -> int -> term list option * report option)) list + * (string * (Proof.context -> term list -> (int -> term list option) list)) list) * test_params; - val empty = ([], Test_Params {default_type = [], expect = No_Expectation}); + 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), + fun merge (((generators1, batch_generators1), params1), ((generators2, batch_generators2), params2)) : T = + ((AList.merge (op =) (K true) (generators1, generators2), + AList.merge (op =) (K true) (batch_generators1, batch_generators2)), merge_test_params (params1, params2)); ); @@ -121,28 +128,34 @@ val map_test_params = Data.map o apsnd o map_test_params' -val add_generator = Data.map o apfst o AList.update (op =); +val add_generator = Data.map o apfst o apfst o AList.update (op =); + +val add_batch_generator = Data.map o apfst o apsnd o AList.update (op =); (* generating tests *) -fun mk_tester ctxt t = +fun gen_mk_tester lookup ctxt v = let val name = Config.get ctxt tester - val tester = case AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) name + val tester = case lookup ctxt name of NONE => error ("No such quickcheck tester: " ^ name) | SOME tester => tester ctxt; in if Config.get ctxt quiet then - try tester t + try tester v else let - val tester = Exn.interruptible_capture tester t + val tester = Exn.interruptible_capture tester v in case Exn.get_result tester of NONE => SOME (Exn.release tester) | SOME tester => SOME tester end end +val mk_tester = gen_mk_tester (fn ctxt => + AList.lookup (op =) ((fst o fst o Data.get o Context.Proof) ctxt)) +val mk_batch_tester = gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o fst o Data.get o Context.Proof) ctxt)) + (* testing propositions *) fun prep_test_term t = @@ -204,6 +217,21 @@ end) (fn () => error (excipit "ran out of time")) () end; +fun test_terms ctxt ts = + let + val (namess, ts') = split_list (map (fn t => apfst (map fst) (prep_test_term t)) ts) + val test_funs = mk_batch_tester ctxt ts' + fun with_size tester k = + if k > Config.get ctxt size then NONE + else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) + val results = + Option.map (map (fn test_fun => TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) + (fn () => with_size test_fun 1) () + handle TimeLimit.TimeOut => NONE)) test_funs + in + Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results + end + (* FIXME: this function shows that many assumptions are made upon the generation *) (* In the end there is probably no generic quickcheck interface left... *) @@ -403,7 +431,7 @@ | read_expectation "counterexample" = Counterexample | read_expectation s = error ("Not an expectation value: " ^ s) -fun valid_tester_name genctxt = AList.defined (op =) (fst (Data.get genctxt)) +fun valid_tester_name genctxt = AList.defined (op =) (fst (fst (Data.get genctxt))) fun parse_tester name genctxt = if valid_tester_name genctxt name then