adding eval option to quickcheck
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 42025cb5b1e85b32e
parent 42024 51df23535105
child 42026 da9b58f1db42
adding eval option to quickcheck
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -458,18 +458,20 @@
     1.4        Config.put_generic tester name genctxt
     1.5      else error ("Unknown tester or test parameter: " ^ name);
     1.6  
     1.7 -fun parse_test_param_inst (name, arg) (insts, ctxt) =
     1.8 +fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) =
     1.9        case try (ProofContext.read_typ ctxt) name
    1.10 -       of SOME (TFree (v, _)) => (apfst o AList.update (op =))
    1.11 -              (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt)
    1.12 -        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt);
    1.13 +       of SOME (TFree (v, _)) =>
    1.14 +         ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt)
    1.15 +        | NONE => (case name of
    1.16 +            "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt)
    1.17 +          | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt));
    1.18  
    1.19  fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
    1.20  
    1.21  fun gen_quickcheck args i state =
    1.22    state
    1.23 -  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
    1.24 -  |> (fn (insts, state') => test_goal (true, true) insts i state'
    1.25 +  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
    1.26 +  |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state'
    1.27    |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
    1.28                 error ("quickcheck expected to find no counterexample but found one") else ()
    1.29             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then