merged

--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Feb 11 11:54:24 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Feb 11 15:31:19 2011 +0100
@@ -500,7 +500,7 @@
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
       |> Config.put Quickcheck.tester (!testgen_name))
-      false (preprocess thy insts (prop_of th));
+      (true, false) (preprocess thy insts (prop_of th));
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
 
@@ -511,7 +511,7 @@
        ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
         #> Config.put Quickcheck.tester (!testgen_name))
          (ProofContext.init_global usedthy))
-       false (preprocess usedthy insts x))))) :: acc))
+       (true, false) (preprocess usedthy insts x))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 11 11:54:24 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 11 15:31:19 2011 +0100
@@ -122,7 +122,7 @@
   TimeLimit.timeLimit (seconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              false [] [t] of
+              (false, false) [] [t] of
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut =>
@@ -315,7 +315,7 @@
         ((Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.finite_type_size 1 #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
-        false [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+        (false, false) [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
   end
 
 fun is_executable_thm thy th = is_executable_term thy (prop_of th)

--- a/src/Tools/quickcheck.ML	Fri Feb 11 11:54:24 2011 +0100
+++ b/src/Tools/quickcheck.ML	Fri Feb 11 15:31:19 2011 +0100
@@ -31,10 +31,10 @@
     string * (Proof.context -> term -> int -> term list option * report option)
       -> Context.generic -> Context.generic
   (* testing terms and proof states *)
-  val test_term: Proof.context -> bool -> term ->
+  val test_term: Proof.context -> bool * bool -> term ->
     (string * term) list option * ((string * int) list * ((int * report) list) option)
   val test_goal_terms:
-    Proof.context -> bool -> (string * typ) list -> term list
+    Proof.context -> bool * bool -> (string * typ) list -> term list
       -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
   val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
 end;
@@ -161,7 +161,15 @@
     val time = Time.toMilliseconds (#cpu (end_timing start))
   in (Exn.release result, (description, time)) end
 
-fun test_term ctxt is_interactive t =
+fun limit ctxt (limit_time, is_interactive) f exc () =
+  if limit_time then
+      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) f ()
+    handle TimeLimit.TimeOut =>
+      if is_interactive then exc () else raise TimeLimit.TimeOut
+  else
+    f ()
+
+fun test_term ctxt (limit_time, is_interactive) t =
   let
     val (names, t') = apfst (map fst) (prep_test_term t);
     val current_size = Unsynchronized.ref 0
@@ -185,7 +193,7 @@
   in
     case test_fun of NONE => (NONE, ([comp_time], NONE))
       | SOME test_fun =>
-        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
+        limit ctxt (limit_time, is_interactive) (fn () =>
           let
             val ((result, reports), exec_time) =
               cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
@@ -193,15 +201,13 @@
             (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
               ([exec_time, comp_time],
                if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
-          end) ()
-        handle TimeLimit.TimeOut =>
-          if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
+          end) (fn () => error (excipit "ran out of time")) ()
   end;
 
 (* FIXME: this function shows that many assumptions are made upon the generation *)
 (* In the end there is probably no generic quickcheck interface left... *)
 
-fun test_term_with_increasing_cardinality ctxt is_interactive ts =
+fun test_term_with_increasing_cardinality ctxt (limit_time, is_interactive) ts =
   let
     val thy = ProofContext.theory_of ctxt
     val (freess, ts') = split_list (map prep_test_term ts)
@@ -225,10 +231,9 @@
       if (forall is_none test_funs) then
         (NONE, ([comp_time], NONE))
       else if (forall is_some test_funs) then
-        TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () =>
-          (get_first test_card_size enumeration_card_size, ([comp_time], NONE))) ()
-        handle TimeLimit.TimeOut =>
-          if is_interactive then error ("Quickcheck ran out of time") else raise TimeLimit.TimeOut
+        limit ctxt (limit_time, is_interactive) (fn () =>
+          (get_first test_card_size enumeration_card_size, ([comp_time], NONE)))
+          (fn () => error "Quickcheck ran out of time") ()
       else
         error "Unexpectedly, testers of some cardinalities are executable but others are not"
     end
@@ -259,7 +264,7 @@
 
 datatype wellsorted_error = Wellsorted_Error of string | Term of term
 
-fun test_goal_terms lthy is_interactive insts check_goals =
+fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals =
   let
     val thy = ProofContext.theory_of lthy
     val default_insts =
@@ -290,16 +295,16 @@
         | (NONE, report) => collect_results f (report :: reports) ts
     fun test_term' goal =
       case goal of
-        [(NONE, t)] => test_term lthy is_interactive t
-      | ts => test_term_with_increasing_cardinality lthy is_interactive (map snd ts)
+        [(NONE, t)] => test_term lthy (limit_time, is_interactive) t
+      | ts => test_term_with_increasing_cardinality lthy (limit_time, is_interactive) (map snd ts)
   in
     if Config.get lthy finite_types then
       collect_results test_term' [] correct_inst_goals
     else
-      collect_results (test_term lthy is_interactive) [] (maps (map snd) correct_inst_goals)
+      collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals)
   end;
 
-fun test_goal is_interactive insts i state =
+fun test_goal (time_limit, is_interactive) insts i state =
   let
     val lthy = Proof.context_of state;
     val thy = Proof.theory_of state;
@@ -320,7 +325,7 @@
       | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
         (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   in
-    test_goal_terms lthy is_interactive insts check_goals
+    test_goal_terms lthy (time_limit, is_interactive) insts check_goals
   end
 
 (* pretty printing *)
@@ -365,7 +370,7 @@
     val res =
       state
       |> Proof.map_context (Config.put report false #> Config.put quiet true)
-      |> try (test_goal false [] 1);
+      |> try (test_goal (false, false) [] 1);
   in
     case res of
       NONE => (false, state)
@@ -436,7 +441,7 @@
 fun gen_quickcheck args i state =
   state
   |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ([], ctxt))
-  |> (fn (insts, state') => test_goal true insts i state'
+  |> (fn (insts, state') => test_goal (true, true) insts i state'
   |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
                error ("quickcheck expected to find no counterexample but found one") else ()
            | (NONE, _) => if expect (Proof.context_of state') = Counterexample then