quickcheck_narrowing returns some timing information
authorbulwahn
Tue Jun 14 08:30:19 2011 +0200 (2011-06-14)
changeset 433798c4b383e5143
parent 43378 d7ae1fae113b
child 43380 809de915155f
quickcheck_narrowing returns some timing information
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 14 08:30:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 14 08:30:19 2011 +0200
     1.3 @@ -209,6 +209,10 @@
     1.4      val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
     1.5      val _ = Isabelle_System.mkdirs path;
     1.6    in Exn.release (Exn.capture f path) end;
     1.7 +
     1.8 +fun elapsed_time description e =
     1.9 +  let val ({elapsed, ...}, result) = Timing.timing e ()
    1.10 +  in (result, (description, Time.toMilliseconds elapsed)) end
    1.11    
    1.12  fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
    1.13    let
    1.14 @@ -237,20 +241,23 @@
    1.15          val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
    1.16            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.17            " -o " ^ executable ^ ";"
    1.18 +        val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd) 
    1.19          val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.20 -        fun with_size k =
    1.21 +        fun with_size k exec_times =
    1.22            if k > size then
    1.23 -            NONE
    1.24 +            (NONE, exec_times)
    1.25            else
    1.26              let
    1.27                val _ = message ("Test data size: " ^ string_of_int k)
    1.28 -              val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
    1.29 +              val ((response, _), exec_time) = elapsed_time ("execution of size " ^ string_of_int k)
    1.30 +                (fn () => bash_output (executable ^ " " ^ string_of_int k))
    1.31              in
    1.32 -              if response = "NONE\n" then with_size (k + 1) else SOME response
    1.33 +              if response = "NONE\n" then with_size (k + 1) (exec_time :: exec_times)
    1.34 +                else (SOME response, exec_time :: exec_times)
    1.35              end
    1.36 -      in case with_size 0 of
    1.37 -           NONE => NONE
    1.38 -         | SOME response =>
    1.39 +      in case with_size 0 [compilation_time] of
    1.40 +           (NONE, exec_times) => (NONE, exec_times)
    1.41 +         | (SOME response, exec_times) =>
    1.42             let
    1.43               val output_value = the_default "NONE"
    1.44                 (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
    1.45 @@ -260,7 +267,7 @@
    1.46               val ctxt' = ctxt
    1.47                 |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.48                 |> Context.proof_map (exec false ml_code);
    1.49 -           in get ctxt' () end     
    1.50 +           in (get ctxt' (), exec_times) end     
    1.51        end
    1.52    in with_tmp_dir tmp_prefix run end;
    1.53  
    1.54 @@ -389,14 +396,14 @@
    1.55          val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
    1.56            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    1.57          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    1.58 -        val result = dynamic_value_strict (true, opts)
    1.59 +        val (result, timings) = dynamic_value_strict (true, opts)
    1.60            (Existential_Counterexample.get, Existential_Counterexample.put,
    1.61              "Narrowing_Generators.put_existential_counterexample")
    1.62 -          thy' (Option.map o map_counterexample) (mk_property qs prop_def')
    1.63 +          thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
    1.64          val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
    1.65        in
    1.66          Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
    1.67 -          timings = [], reports = []}
    1.68 +          timings = timings, reports = []}
    1.69        end
    1.70      else
    1.71        let
    1.72 @@ -405,12 +412,12 @@
    1.73          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.74          fun ensure_testable t =
    1.75            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.76 -        val result = dynamic_value_strict (false, opts)
    1.77 +        val (result, timings) = dynamic_value_strict (false, opts)
    1.78            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.79 -          thy (Option.map o map) (ensure_testable (finitize t'))
    1.80 +          thy (apfst o Option.map o map) (ensure_testable (finitize t'))
    1.81        in
    1.82          Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
    1.83 -          evaluation_terms = Option.map (K []) result, timings = [], reports = []}
    1.84 +          evaluation_terms = Option.map (K []) result, timings = timings, reports = []}
    1.85        end
    1.86    end;
    1.87