--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jan 20 09:28:53 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jan 20 09:28:54 2012 +0100
@@ -10,7 +10,6 @@
val finite_functions : bool Config.T
val overlord : bool Config.T
val active : bool Config.T
- val test_term: Proof.context -> term * term list -> Quickcheck.result
datatype counterexample = Universal_Counterexample of (term * counterexample)
| Existential_Counterexample of (term * counterexample) list
| Empty_Assignment
@@ -430,7 +429,7 @@
|> map (apsnd post_process)
end
-fun test_term ctxt (t, eval_terms) =
+fun test_term ctxt catch_code_errors (t, eval_terms) =
let
fun dest_result (Quickcheck.Result r) = r
val opts =
@@ -448,15 +447,20 @@
apfst (map2 pair qs1) (f (qs2, t)) end
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
- val (counterexample, result) = dynamic_value_strict (true, opts)
+ val act = if catch_code_errors then try else (fn f => SOME o f)
+ val execute = dynamic_value_strict (true, opts)
((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample"))
- thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
- in
- Quickcheck.Result
- {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
- evaluation_terms = Option.map (K []) counterexample,
- timings = #timings (dest_result result), reports = #reports (dest_result result)}
+ thy (apfst o Option.map o map_counterexample)
+ in
+ case act execute (mk_property qs prop_t) of
+ SOME (counterexample, result) => Quickcheck.Result
+ {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
+ evaluation_terms = Option.map (K []) counterexample,
+ timings = #timings (dest_result result), reports = #reports (dest_result result)}
+ | NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
+ Quickcheck.empty_result)
end
else
let
@@ -469,25 +473,33 @@
fun is_genuine (SOME (true, _)) = true
| is_genuine _ = false
val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
- val (counterexample, result) = dynamic_value_strict (false, opts)
+ val act = if catch_code_errors then try else (fn f => SOME o f)
+ val execute = dynamic_value_strict (false, opts)
((is_genuine, counterexample_of),
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
- thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
+ thy (apfst o Option.map o apsnd o map)
in
- Quickcheck.Result
- {counterexample = counterexample_of counterexample,
- evaluation_terms = Option.map (K []) counterexample,
- timings = #timings (dest_result result), reports = #reports (dest_result result)}
+ case act execute (ensure_testable (finitize t')) of
+ SOME (counterexample, result) =>
+ Quickcheck.Result
+ {counterexample = counterexample_of counterexample,
+ evaluation_terms = Option.map (K []) counterexample,
+ timings = #timings (dest_result result),
+ reports = #reports (dest_result result)}
+ | NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
+ Quickcheck.empty_result)
end
end;
-fun test_goals ctxt _ insts goals =
+fun test_goals ctxt catch_code_errors insts goals =
if (not (getenv "ISABELLE_GHC" = "")) then
let
val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
in
- Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
+ Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
+ (maps (map snd) correct_inst_goals) []
end
else
(if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message