# HG changeset patch # User bulwahn # Date 1310978061 -7200 # Node ID cabe74eab19afa2ab2ef8832e2b39c1a1b8e42ca # Parent 2eb76746c4081535ae9224e90dfa907d13b157cf changing parser in quickcheck to activate and deactivate the testers diff -r 2eb76746c408 -r cabe74eab19a 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 @@ -225,6 +225,21 @@ val add_batch_validator = Data.map o apfst o apsnd o apsnd o AList.update (op =); +fun active_testers ctxt = + let + val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt + in + map snd (filter (fn (active, _) => Config.get ctxt active) testers) + end + +fun set_active_testers testers gen_ctxt = + let + val registered_testers = (fst o fst o Data.get) gen_ctxt + in + fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name)) + registered_testers gen_ctxt + end + (* generating tests *) fun gen_mk_tester lookup ctxt v = @@ -339,7 +354,8 @@ 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) + val (test_funs, comp_time) = + cpu_time "quickcheck batch compilation" (fn () => mk_batch_tester ctxt ts) fun with_size tester k = if k > size then NONE else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) @@ -367,8 +383,9 @@ fun test_card_size test_fun (card, size) = (* FIXME: why decrement size by one? *) let - val (ts, timing) = cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) - (fn () => fst (test_fun [card, size - 1])) + val (ts, timing) = + cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card) + (fn () => fst (test_fun [card, size - 1])) val _ = add_timing timing current_result in Option.map (pair card) ts @@ -473,21 +490,10 @@ collect_results (test_term compile ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) [] end; - - -fun active_testers ctxt = - let - val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt - in - map snd (filter (fn (active, _) => Config.get ctxt active) testers) - end fun test_goal_terms ctxt (limit_time, is_interactive) insts goals = - (*case lookup_tester ctxt of - SOME test_goal_terms => test_goal_terms ctxt (limit_time, is_interactive) insts goals - | NONE => error ("Unknown tester: " ^ Config.get ctxt tester)*) case active_testers ctxt of - [] => error "No active tester for quickcheck" + [] => error "No active testers for quickcheck" | testers => testers |> Par_List.get_some (fn tester => tester ctxt (limit_time, is_interactive) insts goals |> (fn result => if exists found_counterexample result then SOME result else NONE)) @@ -529,8 +535,8 @@ @ (if null eval_terms then [] else (Pretty.str ("Evaluated terms:\n") :: map (fn (t, u) => - Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) - (rev eval_terms)))); + Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, + Syntax.pretty_term ctxt u]) (rev eval_terms)))); fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors, satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = @@ -589,40 +595,45 @@ fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name -fun parse_tester name genctxt = +fun parse_tester name (testers, genctxt) = if valid_tester_name genctxt name then - Config.put_generic tester name genctxt + (insert (op =) name testers, genctxt) else error ("Unknown tester: " ^ name) -fun parse_test_param ("tester", [arg]) = parse_tester arg - | parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg) - | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg) - | parse_test_param ("default_type", arg) = (fn gen_ctxt => - map_test_params - ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt) - | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg) - | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg)) - | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg) - | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg) - | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg) - | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg) +fun parse_test_param ("tester", args) = fold parse_tester args + | parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg)) + | parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg)) + | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) => + (testers, map_test_params + ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)) + | parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg)) + | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg))) + | parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg)) + | parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg)) + | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg)) + | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg)) | parse_test_param ("finite_type_size", [arg]) = - Config.put_generic finite_type_size (read_nat arg) - | parse_test_param (name, _) = fn genctxt => + apsnd (Config.put_generic finite_type_size (read_nat arg)) + | parse_test_param (name, _) = (fn (testers, genctxt) => if valid_tester_name genctxt name then - Config.put_generic tester name genctxt - else error ("Unknown tester or test parameter: " ^ name); + (insert (op =) name testers, genctxt) + else error ("Unknown tester or test parameter: " ^ name)); -fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) = +fun proof_map_result f = apsnd Context.the_proof o f o Context.Proof; + +fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) = case try (Proof_Context.read_typ ctxt) name of SOME (TFree (v, _)) => - ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt) + ((AList.update (op =) (v, Proof_Context.read_typ ctxt (the_single arg)) insts, eval_terms), + (testers, ctxt)) | NONE => (case name of - "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt) - | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt)); + "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt)) + | _ => ((insts, eval_terms), + proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)); -fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args); +fun quickcheck_params_cmd args = Context.theory_map + (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt))); fun check_expectation state results = (if is_some results andalso expect (Proof.context_of state) = No_Counterexample @@ -636,7 +647,9 @@ fun gen_quickcheck args i state = state - |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt)) + |> Proof.map_context_result (fn ctxt => + apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt) + (fold parse_test_param_inst args (([], []), ([], ctxt)))) |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state' |> tap (check_expectation state'))