1.1 --- a/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200
1.2 +++ b/src/Tools/quickcheck.ML Mon Jul 18 10:34:21 2011 +0200
1.3 @@ -225,6 +225,21 @@
1.4
1.5 val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =);
1.6
1.7 +fun active_testers ctxt =
1.8 + let
1.9 + val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
1.10 + in
1.11 + map snd (filter (fn (active, _) => Config.get ctxt active) testers)
1.12 + end
1.13 +
1.14 +fun set_active_testers testers gen_ctxt =
1.15 + let
1.16 + val registered_testers = (fst o fst o Data.get) gen_ctxt
1.17 + in
1.18 + fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
1.19 + registered_testers gen_ctxt
1.20 + end
1.21 +
1.22 (* generating tests *)
1.23
1.24 fun gen_mk_tester lookup ctxt v =
1.25 @@ -339,7 +354,8 @@
1.26 val _ = map check_test_term ts
1.27 val size = Config.get ctxt size
1.28 val namess = map (fn t => Term.add_free_names t []) ts
1.29 - val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts)
1.30 + val (test_funs, comp_time) =
1.31 + cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts)
1.32 fun with_size tester k =
1.33 if k > size then NONE
1.34 else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
1.35 @@ -367,8 +383,9 @@
1.36 fun test_card_size test_fun (card, size) =
1.37 (* FIXME: why decrement size by one? *)
1.38 let
1.39 - val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
1.40 - (fn () => fst (test_fun [card, size - 1]))
1.41 + val (ts, timing) =
1.42 + cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
1.43 + (fn () => fst (test_fun [card, size - 1]))
1.44 val _ = add_timing timing current_result
1.45 in
1.46 Option.map (pair card) ts
1.47 @@ -473,21 +490,10 @@
1.48 collect_results (test_term compile ctxt (limit_time, is_interactive))
1.49 (maps (map snd) correct_inst_goals) []
1.50 end;
1.51 -
1.52 -
1.53 -fun active_testers ctxt =
1.54 - let
1.55 - val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
1.56 - in
1.57 - map snd (filter (fn (active, _) => Config.get ctxt active) testers)
1.58 - end
1.59
1.60 fun test_goal_terms ctxt (limit_time, is_interactive) insts goals =
1.61 - (*case lookup_tester ctxt of
1.62 - SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals
1.63 - | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)*)
1.64 case active_testers ctxt of
1.65 - [] => error "No active tester for quickcheck"
1.66 + [] => error "No active testers for quickcheck"
1.67 | testers => testers |> Par_List.get_some (fn tester =>
1.68 tester ctxt (limit_time, is_interactive) insts goals |>
1.69 (fn result => if exists found_counterexample result then SOME result else NONE))
1.70 @@ -529,8 +535,8 @@
1.71 @ (if null eval_terms then []
1.72 else (Pretty.str ("Evaluated terms:\n") ::
1.73 map (fn (t, u) =>
1.74 - Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
1.75 - (rev eval_terms))));
1.76 + Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
1.77 + Syntax.pretty_term ctxt u]) (rev eval_terms))));
1.78
1.79 fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
1.80 satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
1.81 @@ -589,40 +595,45 @@
1.82
1.83 fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name
1.84
1.85 -fun parse_tester name genctxt =
1.86 +fun parse_tester name (testers, genctxt) =
1.87 if valid_tester_name genctxt name then
1.88 - Config.put_generic tester name genctxt
1.89 + (insert (op =) name testers, genctxt)
1.90 else
1.91 error ("Unknown tester: " ^ name)
1.92
1.93 -fun parse_test_param ("tester", [arg]) = parse_tester arg
1.94 - | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
1.95 - | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
1.96 - | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
1.97 - map_test_params
1.98 - ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
1.99 - | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
1.100 - | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
1.101 - | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
1.102 - | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
1.103 - | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
1.104 - | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
1.105 +fun parse_test_param ("tester", args) = fold parse_tester args
1.106 + | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
1.107 + | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
1.108 + | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
1.109 + (testers, map_test_params
1.110 + ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
1.111 + | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
1.112 + | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
1.113 + | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
1.114 + | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
1.115 + | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
1.116 + | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
1.117 | parse_test_param ("finite_type_size", [arg]) =
1.118 - Config.put_generic finite_type_size (read_nat arg)
1.119 - | parse_test_param (name, _) = fn genctxt =>
1.120 + apsnd (Config.put_generic finite_type_size (read_nat arg))
1.121 + | parse_test_param (name, _) = (fn (testers, genctxt) =>
1.122 if valid_tester_name genctxt name then
1.123 - Config.put_generic tester name genctxt
1.124 - else error ("Unknown tester or test parameter: " ^ name);
1.125 + (insert (op =) name testers, genctxt)
1.126 + else error ("Unknown tester or test parameter: " ^ name));
1.127
1.128 -fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) =
1.129 +fun proof_map_result f = apsnd Context.the_proof o f o Context.Proof;
1.130 +
1.131 +fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) =
1.132 case try (Proof_Context.read_typ ctxt) name
1.133 of SOME (TFree (v, _)) =>
1.134 - ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt)
1.135 + ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms),
1.136 + (testers, ctxt))
1.137 | NONE => (case name of
1.138 - "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt)
1.139 - | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt));
1.140 + "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
1.141 + | _ => ((insts, eval_terms),
1.142 + proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt));
1.143
1.144 -fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
1.145 +fun quickcheck_params_cmd args = Context.theory_map
1.146 + (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
1.147
1.148 fun check_expectation state results =
1.149 (if is_some results andalso expect (Proof.context_of state) = No_Counterexample
1.150 @@ -636,7 +647,9 @@
1.151
1.152 fun gen_quickcheck args i state =
1.153 state
1.154 - |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
1.155 + |> Proof.map_context_result (fn ctxt =>
1.156 + apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
1.157 + (fold parse_test_param_inst args (([], []), ([], ctxt))))
1.158 |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
1.159 |> tap (check_expectation state'))
1.160