# HG changeset patch # User bulwahn # Date 1300468782 -3600 # Node ID cb5b1e85b32e5441af1b5fe6b3bb0b9bdc948adb # Parent 51df2353510541276cfa2767d9fba2d2ce01bd9b adding eval option to quickcheck diff -r 51df23535105 -r cb5b1e85b32e src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/Tools/quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 @@ -458,18 +458,20 @@ Config.put_generic tester name genctxt else error ("Unknown tester or test parameter: " ^ name); -fun parse_test_param_inst (name, arg) (insts, ctxt) = +fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) = case try (ProofContext.read_typ ctxt) name - of SOME (TFree (v, _)) => (apfst o AList.update (op =)) - (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt) - | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt); + of SOME (TFree (v, _)) => + ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), 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)); fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args); fun gen_quickcheck args i state = state - |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt)) - |> (fn (insts, state') => test_goal (true, true) insts i state' + |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt)) + |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state' |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then error ("quickcheck expected to find no counterexample but found one") else () | (NONE, _) => if expect (Proof.context_of state') = Counterexample then