# HG changeset patch # User bulwahn # Date 1301658576 -7200 # Node ID bd416284a432f92ef107f44b11d1ba0b1ab4f62c # Parent 8eed749527b6c72d844fdb403026c5a666202e31 adding general interface for batch validators in quickcheck diff -r 8eed749527b6 -r bd416284a432 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Apr 01 13:21:21 2011 +0200 +++ b/src/Tools/quickcheck.ML Fri Apr 01 13:49:36 2011 +0200 @@ -34,6 +34,9 @@ val add_batch_generator: string * (Proof.context -> term list -> (int -> term list option) list) -> Context.generic -> Context.generic + val add_batch_validator: + string * (Proof.context -> term list -> (int -> bool) list) + -> Context.generic -> Context.generic (* quickcheck's result *) datatype result = Result of @@ -52,6 +55,7 @@ (* testing a batch of terms *) val test_terms: Proof.context -> term list -> (string * term) list option list option * (string * int) list + val validate_terms: Proof.context -> term list -> bool list option * (string * int) list end; structure Quickcheck : QUICKCHECK = @@ -163,13 +167,16 @@ ( type T = ((string * (Proof.context -> (term * term list) list -> int list -> term list option * report option)) list - * (string * (Proof.context -> term list -> (int -> term list option) list)) list) + * ((string * (Proof.context -> term list -> (int -> term list option) list)) list + * ((string * (Proof.context -> term list -> (int -> bool) 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, batch_generators1), params1), ((generators2, batch_generators2), params2)) : T = + fun merge (((generators1, (batch_generators1, batch_validators1)), params1), + ((generators2, (batch_generators2, batch_validators2)), params2)) : T = ((AList.merge (op =) (K true) (generators1, generators2), - AList.merge (op =) (K true) (batch_generators1, batch_generators2)), + (AList.merge (op =) (K true) (batch_generators1, batch_generators2), + AList.merge (op =) (K true) (batch_validators1, batch_validators2))), merge_test_params (params1, params2)); ); @@ -183,7 +190,9 @@ 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 =); +val add_batch_generator = Data.map o apfst o apsnd o apfst o AList.update (op =); + +val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =); (* generating tests *) @@ -205,10 +214,13 @@ 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)) - +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 =) ((fst o snd o fst o Data.get o Context.Proof) ctxt)) +val mk_batch_validator = + gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt)) + (* testing propositions *) fun check_test_term t = @@ -275,17 +287,35 @@ (fn () => (message (excipit ()); !current_result)) () end; +fun validate_terms ctxt ts = + let + val _ = map check_test_term ts + val size = Config.get ctxt size + val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" + (fn () => mk_batch_validator ctxt ts) + fun with_size tester k = + 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 timeout)) + (fn () => with_size test_fun 1) () + handle TimeLimit.TimeOut => true)) test_funs) + in + (results, [comp_time, exec_time]) + end + fun test_terms ctxt ts = let val _ = map check_test_term ts + val size = Config.get ctxt size val namess = map (fn t => Term.add_free_names t []) ts val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) fun with_size tester k = - if k > Config.get ctxt size then NONE + 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 timeout)) - (fn () => with_size test_fun 1) () + (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,