src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46309 693d8d7bc3cd
parent 46219 426ed18eba43
child 46316 1c9a548c0402
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jan 20 09:28:53 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jan 20 09:28:54 2012 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4    val finite_functions : bool Config.T
     1.5    val overlord : bool Config.T
     1.6    val active : bool Config.T
     1.7 -  val test_term: Proof.context -> term * term list -> Quickcheck.result
     1.8    datatype counterexample = Universal_Counterexample of (term * counterexample)
     1.9      | Existential_Counterexample of (term * counterexample) list
    1.10      | Empty_Assignment
    1.11 @@ -430,7 +429,7 @@
    1.12        |> map (apsnd post_process)
    1.13      end
    1.14    
    1.15 -fun test_term ctxt (t, eval_terms) =
    1.16 +fun test_term ctxt catch_code_errors (t, eval_terms) =
    1.17    let
    1.18      fun dest_result (Quickcheck.Result r) = r 
    1.19      val opts =
    1.20 @@ -448,15 +447,20 @@
    1.21            apfst (map2 pair qs1) (f (qs2, t)) end
    1.22          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.23          val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
    1.24 -        val (counterexample, result) = dynamic_value_strict (true, opts)
    1.25 +        val act = if catch_code_errors then try else (fn f => SOME o f)
    1.26 +        val execute = dynamic_value_strict (true, opts)
    1.27            ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
    1.28              "Narrowing_Generators.put_existential_counterexample"))
    1.29 -          thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
    1.30 -      in
    1.31 -        Quickcheck.Result
    1.32 -         {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
    1.33 -          evaluation_terms = Option.map (K []) counterexample,
    1.34 -          timings = #timings (dest_result result), reports = #reports (dest_result result)}
    1.35 +          thy (apfst o Option.map o map_counterexample)
    1.36 +      in  
    1.37 +        case act execute (mk_property qs prop_t) of 
    1.38 +          SOME (counterexample, result) => Quickcheck.Result
    1.39 +            {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
    1.40 +            evaluation_terms = Option.map (K []) counterexample,
    1.41 +            timings = #timings (dest_result result), reports = #reports (dest_result result)}
    1.42 +        | NONE =>
    1.43 +          (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
    1.44 +           Quickcheck.empty_result)
    1.45        end
    1.46      else
    1.47        let
    1.48 @@ -469,25 +473,33 @@
    1.49          fun is_genuine (SOME (true, _)) = true 
    1.50            | is_genuine _ = false
    1.51          val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
    1.52 -        val (counterexample, result) = dynamic_value_strict (false, opts)
    1.53 +        val act = if catch_code_errors then try else (fn f => SOME o f)
    1.54 +        val execute = dynamic_value_strict (false, opts)
    1.55            ((is_genuine, counterexample_of),
    1.56              (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
    1.57 -          thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
    1.58 +          thy (apfst o Option.map o apsnd o map)
    1.59        in
    1.60 -        Quickcheck.Result
    1.61 -         {counterexample = counterexample_of counterexample,
    1.62 -          evaluation_terms = Option.map (K []) counterexample,
    1.63 -          timings = #timings (dest_result result), reports = #reports (dest_result result)}
    1.64 +        case act execute (ensure_testable (finitize t')) of 
    1.65 +          SOME (counterexample, result) =>
    1.66 +            Quickcheck.Result
    1.67 +             {counterexample = counterexample_of counterexample,
    1.68 +              evaluation_terms = Option.map (K []) counterexample,
    1.69 +              timings = #timings (dest_result result),
    1.70 +              reports = #reports (dest_result result)}
    1.71 +        | NONE =>
    1.72 +          (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
    1.73 +           Quickcheck.empty_result)
    1.74        end
    1.75    end;
    1.76  
    1.77 -fun test_goals ctxt _ insts goals =
    1.78 +fun test_goals ctxt catch_code_errors insts goals =
    1.79    if (not (getenv "ISABELLE_GHC" = "")) then
    1.80      let
    1.81        val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
    1.82        val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
    1.83      in
    1.84 -      Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
    1.85 +      Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
    1.86 +        (maps (map snd) correct_inst_goals) []
    1.87      end
    1.88    else
    1.89      (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message