adding timeout to quickcheck narrowing
authorbulwahn
Tue Jun 28 14:36:43 2011 +0200 (2011-06-28)
changeset 43585ea959ab7bbe3
parent 43583 4d375d0fa4b0
child 43586 eb64d8e00a62
adding timeout to quickcheck narrowing
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Tools/quickcheck.ML
     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  
     2.1 --- a/src/Tools/quickcheck.ML	Tue Jun 28 12:48:00 2011 +0100
     2.2 +++ b/src/Tools/quickcheck.ML	Tue Jun 28 14:36:43 2011 +0200
     2.3 @@ -39,6 +39,7 @@
     2.4        timings : (string * int) list,
     2.5        reports : (int * report) list}
     2.6    val empty_result : result
     2.7 +  val add_timing : (string * int) -> result Unsynchronized.ref -> unit
     2.8    val counterexample_of : result -> (string * term) list option
     2.9    val timings_of : result -> (string * int) list
    2.10    (* registering generators *)
    2.11 @@ -55,6 +56,7 @@
    2.12      string * (Proof.context -> term list -> (int -> bool) list)
    2.13        -> Context.generic -> Context.generic
    2.14    (* basic operations *)
    2.15 +  val limit : Time.time -> (bool * bool) -> (unit -> 'a) -> (unit -> 'a) -> unit -> 'a  
    2.16    val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
    2.17      -> (typ option * (term * term list)) list list
    2.18    val collect_results: ('a -> result) -> 'a list -> result list -> result list
    2.19 @@ -125,6 +127,15 @@
    2.20    end
    2.21    | set_reponse _ _ NONE result = result
    2.22  
    2.23 +
    2.24 +fun set_counterexample counterexample (Result r) =
    2.25 +  Result {counterexample = counterexample,  evaluation_terms = #evaluation_terms r,
    2.26 +    timings = #timings r, reports = #reports r}
    2.27 +
    2.28 +fun set_evaluation_terms evaluation_terms (Result r) =
    2.29 +  Result {counterexample = #counterexample r,  evaluation_terms = evaluation_terms,
    2.30 +    timings = #timings r, reports = #reports r}
    2.31 +
    2.32  fun cons_timing timing (Result r) =
    2.33    Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
    2.34      timings = cons timing (#timings r), reports = #reports r}
    2.35 @@ -258,9 +269,9 @@
    2.36    let val ({cpu, ...}, result) = Timing.timing e ()
    2.37    in (result, (description, Time.toMilliseconds cpu)) end
    2.38  
    2.39 -fun limit ctxt (limit_time, is_interactive) f exc () =
    2.40 +fun limit timeout (limit_time, is_interactive) f exc () =
    2.41    if limit_time then
    2.42 -      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f ()
    2.43 +      TimeLimit.timeLimit timeout f ()
    2.44      handle TimeLimit.TimeOut =>
    2.45        if is_interactive then exc () else raise TimeLimit.TimeOut
    2.46    else
    2.47 @@ -290,7 +301,7 @@
    2.48            case result of NONE => with_size test_fun (k + 1) | SOME q => SOME q
    2.49          end;
    2.50    in
    2.51 -    limit ctxt (limit_time, is_interactive) (fn () =>
    2.52 +    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
    2.53        let
    2.54          val (test_fun, comp_time) = cpu_time "quickcheck compilation"
    2.55            (fn () => mk_tester ctxt [(t, eval_terms)]);
    2.56 @@ -375,7 +386,7 @@
    2.57          map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt size))
    2.58          |> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
    2.59    in
    2.60 -    limit ctxt (limit_time, is_interactive) (fn () =>
    2.61 +    limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive) (fn () =>
    2.62        let
    2.63          val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => mk_tester ctxt ts)
    2.64          val _ = add_timing comp_time current_result