src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43585 ea959ab7bbe3
parent 43379 8c4b383e5143
child 43602 8c89a1fb30f2
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 28 12:48:00 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 28 14:36:43 2011 +0200
     1.3 @@ -214,9 +214,15 @@
     1.4    let val ({elapsed, ...}, result) = Timing.timing e ()
     1.5    in (result, (description, Time.toMilliseconds elapsed)) end
     1.6    
     1.7 -fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
     1.8 +fun value (contains_existentials, opts) ctxt cookie (code, value_name) =
     1.9    let
    1.10 +    val (limit_time, is_interactive, timeout, quiet, size) = opts
    1.11 +    val (get, put, put_ml) = cookie
    1.12      fun message s = if quiet then () else Output.urgent_message s
    1.13 +    val current_size = Unsynchronized.ref 0
    1.14 +    val current_result = Unsynchronized.ref Quickcheck.empty_result 
    1.15 +    fun excipit () =
    1.16 +      "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size)
    1.17      val tmp_prefix = "Quickcheck_Narrowing"
    1.18      val with_tmp_dir =
    1.19        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    1.20 @@ -242,34 +248,39 @@
    1.21            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.22            " -o " ^ executable ^ ";"
    1.23          val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd) 
    1.24 +        val _ = Quickcheck.add_timing compilation_time current_result
    1.25          val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.26 -        fun with_size k exec_times =
    1.27 +        fun with_size k =
    1.28            if k > size then
    1.29 -            (NONE, exec_times)
    1.30 +            (NONE, !current_result)
    1.31            else
    1.32              let
    1.33                val _ = message ("Test data size: " ^ string_of_int k)
    1.34 -              val ((response, _), exec_time) = elapsed_time ("execution of size " ^ string_of_int k)
    1.35 +              val _ = current_size := k
    1.36 +              val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    1.37                  (fn () => bash_output (executable ^ " " ^ string_of_int k))
    1.38 +              val _ = Quickcheck.add_timing timing current_result
    1.39              in
    1.40 -              if response = "NONE\n" then with_size (k + 1) (exec_time :: exec_times)
    1.41 -                else (SOME response, exec_time :: exec_times)
    1.42 -            end
    1.43 -      in case with_size 0 [compilation_time] of
    1.44 -           (NONE, exec_times) => (NONE, exec_times)
    1.45 -         | (SOME response, exec_times) =>
    1.46 -           let
    1.47 -             val output_value = the_default "NONE"
    1.48 -               (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
    1.49 -               |> translate_string (fn s => if s = "\\" then "\\\\" else s)
    1.50 -             val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.51 -               ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    1.52 -             val ctxt' = ctxt
    1.53 -               |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.54 -               |> Context.proof_map (exec false ml_code);
    1.55 -           in (get ctxt' (), exec_times) end     
    1.56 -      end
    1.57 -  in with_tmp_dir tmp_prefix run end;
    1.58 +              if response = "NONE\n" then
    1.59 +                with_size (k + 1)
    1.60 +              else
    1.61 +                let
    1.62 +                  val output_value = the_default "NONE"
    1.63 +                    (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
    1.64 +                    |> translate_string (fn s => if s = "\\" then "\\\\" else s)
    1.65 +                  val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.66 +                    ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    1.67 +                  val ctxt' = ctxt
    1.68 +                    |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.69 +                    |> Context.proof_map (exec false ml_code);
    1.70 +                in (get ctxt' (), !current_result) end
    1.71 +            end 
    1.72 +      in with_size 0 end
    1.73 +  in
    1.74 +    Quickcheck.limit timeout (limit_time, is_interactive) 
    1.75 +      (fn () => with_tmp_dir tmp_prefix run)
    1.76 +      (fn () => (message (excipit ()); (NONE, !current_result))) ()
    1.77 +  end;
    1.78  
    1.79  fun dynamic_value_strict opts cookie thy postproc t =
    1.80    let
    1.81 @@ -380,7 +391,10 @@
    1.82    
    1.83  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    1.84    let
    1.85 -    val opts = (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    1.86 +    fun dest_result (Quickcheck.Result r) = r 
    1.87 +    val opts =
    1.88 +      (limit_time, is_interactive, seconds (Config.get ctxt Quickcheck.timeout),
    1.89 +        Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    1.90      val thy = Proof_Context.theory_of ctxt
    1.91      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    1.92      val pnf_t = make_pnf_term thy t'
    1.93 @@ -396,14 +410,15 @@
    1.94          val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
    1.95            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    1.96          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    1.97 -        val (result, timings) = dynamic_value_strict (true, opts)
    1.98 +        val (counterexample, result) = dynamic_value_strict (true, opts)
    1.99            (Existential_Counterexample.get, Existential_Counterexample.put,
   1.100              "Narrowing_Generators.put_existential_counterexample")
   1.101            thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
   1.102 -        val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
   1.103        in
   1.104 -        Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
   1.105 -          timings = timings, reports = []}
   1.106 +        Quickcheck.Result
   1.107 +         {counterexample = Option.map (mk_terms ctxt' qs) counterexample,
   1.108 +          evaluation_terms = Option.map (K []) counterexample,
   1.109 +          timings = #timings (dest_result result), reports = #reports (dest_result result)}
   1.110        end
   1.111      else
   1.112        let
   1.113 @@ -412,12 +427,14 @@
   1.114          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   1.115          fun ensure_testable t =
   1.116            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   1.117 -        val (result, timings) = dynamic_value_strict (false, opts)
   1.118 +        val (counterexample, result) = dynamic_value_strict (false, opts)
   1.119            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   1.120            thy (apfst o Option.map o map) (ensure_testable (finitize t'))
   1.121        in
   1.122 -        Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   1.123 -          evaluation_terms = Option.map (K []) result, timings = timings, reports = []}
   1.124 +        Quickcheck.Result
   1.125 +         {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
   1.126 +          evaluation_terms = Option.map (K []) counterexample,
   1.127 +          timings = #timings (dest_result result), reports = #reports (dest_result result)}
   1.128        end
   1.129    end;
   1.130