src/Tools/quickcheck.ML
changeset 42025 cb5b1e85b32e
parent 41862 a38536bf2736
child 42026 da9b58f1db42
equal deleted inserted replaced
42024:51df23535105 42025:cb5b1e85b32e
   456   | parse_test_param (name, _) = fn genctxt =>
   456   | parse_test_param (name, _) = fn genctxt =>
   457     if valid_tester_name genctxt name then
   457     if valid_tester_name genctxt name then
   458       Config.put_generic tester name genctxt
   458       Config.put_generic tester name genctxt
   459     else error ("Unknown tester or test parameter: " ^ name);
   459     else error ("Unknown tester or test parameter: " ^ name);
   460 
   460 
   461 fun parse_test_param_inst (name, arg) (insts, ctxt) =
   461 fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) =
   462       case try (ProofContext.read_typ ctxt) name
   462       case try (ProofContext.read_typ ctxt) name
   463        of SOME (TFree (v, _)) => (apfst o AList.update (op =))
   463        of SOME (TFree (v, _)) =>
   464               (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt)
   464          ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt)
   465         | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt);
   465         | NONE => (case name of
       
   466             "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt)
       
   467           | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt));
   466 
   468 
   467 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
   469 fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
   468 
   470 
   469 fun gen_quickcheck args i state =
   471 fun gen_quickcheck args i state =
   470   state
   472   state
   471   |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
   473   |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt))
   472   |> (fn (insts, state') => test_goal (true, true) insts i state'
   474   |> (fn ((insts, eval_terms), state') => test_goal (true, true) insts i state'
   473   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   475   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
   474                error ("quickcheck expected to find no counterexample but found one") else ()
   476                error ("quickcheck expected to find no counterexample but found one") else ()
   475            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
   477            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
   476                error ("quickcheck expected to find a counterexample but did not find one") else ()))
   478                error ("quickcheck expected to find a counterexample but did not find one") else ()))
   477 
   479