src/Tools/quickcheck.ML
changeset 42025 cb5b1e85b32e
parent 41862 a38536bf2736
child 42026 da9b58f1db42
--- 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