--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 11:34:55 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Nov 09 11:34:57 2011 +0100
@@ -10,7 +10,7 @@
val finite_functions : bool Config.T
val overlord : bool Config.T
val active : bool Config.T
- val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
+ val test_term: Proof.context -> term * term list -> Quickcheck.result
datatype counterexample = Universal_Counterexample of (term * counterexample)
| Existential_Counterexample of (term * counterexample) list
| Empty_Assignment
@@ -222,9 +222,8 @@
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
-fun value (contains_existentials, opts) ctxt cookie (code, value_name) =
+fun value (contains_existentials, (quiet, size)) ctxt cookie (code, value_name) =
let
- val (limit_time, is_interactive, timeout, quiet, size) = opts
val (get, put, put_ml) = cookie
fun message s = if quiet then () else Output.urgent_message s
val current_size = Unsynchronized.ref 0
@@ -286,9 +285,7 @@
end
in with_size 0 end
in
- (*Quickcheck.limit timeout (limit_time, is_interactive)
- (fn () =>*) with_tmp_dir tmp_prefix run
- (*(fn () => (message (excipit ()); (NONE, !current_result))) ()*)
+ with_tmp_dir tmp_prefix run
end;
fun dynamic_value_strict opts cookie thy postproc t =
@@ -414,12 +411,11 @@
|> map (apsnd post_process)
end
-fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
+fun test_term ctxt (t, eval_terms) =
let
fun dest_result (Quickcheck.Result r) = r
val opts =
- (limit_time, is_interactive, seconds (Config.get ctxt Quickcheck.timeout),
- Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
+ (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
val thy = Proof_Context.theory_of ctxt
val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
val pnf_t = make_pnf_term thy t'
@@ -460,12 +456,12 @@
end
end;
-fun test_goals ctxt (limit_time, is_interactive) insts goals =
+fun test_goals ctxt insts goals =
if (not (getenv "ISABELLE_GHC" = "")) then
let
val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
in
- Quickcheck_Common.collect_results (test_term ctxt (limit_time, is_interactive)) (maps (map snd) correct_inst_goals) []
+ Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
end
else
(if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 11:34:55 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Wed Nov 09 11:34:57 2011 +0100
@@ -16,8 +16,8 @@
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
type compile_generator =
Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
- val generator_test_goal_terms : compile_generator -> Proof.context -> bool * bool
- -> (string * typ) list -> (term * term list) list -> Quickcheck.result list
+ val generator_test_goal_terms : compile_generator -> Proof.context -> (string * typ) list
+ -> (term * term list) list -> Quickcheck.result list
val ensure_sort_datatype:
((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list
-> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory)
@@ -27,7 +27,7 @@
-> Proof.context -> (term * term list) list -> term
val mk_fun_upd : typ -> typ -> term * term -> term -> term
val post_process_term : term -> term
- val test_term : compile_generator -> Proof.context -> bool * bool -> term * term list -> Quickcheck.result
+ val test_term : compile_generator -> Proof.context -> term * term list -> Quickcheck.result
end;
structure Quickcheck_Common : QUICKCHECK_COMMON =
@@ -61,7 +61,7 @@
let val ({cpu, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds cpu)) end
-fun test_term compile ctxt (limit_time, is_interactive) (t, eval_terms) =
+fun test_term compile ctxt (t, eval_terms) =
let
val _ = check_test_term t
val names = Term.add_free_names t []
@@ -135,7 +135,7 @@
end
-fun test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) ts =
+fun test_term_with_increasing_cardinality compile ctxt ts =
let
val thy = Proof_Context.theory_of ctxt
val (ts', eval_terms) = split_list ts
@@ -245,19 +245,19 @@
SOME (lhs, rhs) => (t, eval_terms @ [rhs, lhs])
| NONE => (t, eval_terms)
-fun generator_test_goal_terms compile ctxt (limit_time, is_interactive) insts goals =
+fun generator_test_goal_terms compile ctxt insts goals =
let
fun test_term' goal =
case goal of
- [(NONE, t)] => test_term compile ctxt (limit_time, is_interactive) t
- | ts => test_term_with_increasing_cardinality compile ctxt (limit_time, is_interactive) (map snd ts)
+ [(NONE, t)] => test_term compile ctxt t
+ | ts => test_term_with_increasing_cardinality compile ctxt (map snd ts)
val goals' = instantiate_goals ctxt insts goals
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then
collect_results test_term' goals' []
else
- collect_results (test_term compile ctxt (limit_time, is_interactive))
+ collect_results (test_term compile ctxt)
(maps (map snd) goals') []
end;
--- a/src/Tools/quickcheck.ML Wed Nov 09 11:34:55 2011 +0100
+++ b/src/Tools/quickcheck.ML Wed Nov 09 11:34:57 2011 +0100
@@ -50,7 +50,7 @@
val timings_of : result -> (string * int) list
(* registering testers & generators *)
type tester =
- Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+ Proof.context -> (string * typ) list -> (term * term list) list -> result list
val add_tester : string * (bool Config.T * tester) -> Context.generic -> Context.generic
val add_batch_generator :
string * (Proof.context -> term list -> (int -> term list option) list)
@@ -192,7 +192,7 @@
(merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
type tester =
- Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
+ Proof.context -> (string * typ) list -> (term * term list) list -> result list
structure Data = Generic_Data
(
@@ -288,7 +288,7 @@
[] => error "No active testers for quickcheck"
| testers => limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
(fn () => Par_List.get_some (fn tester =>
- tester ctxt (limit_time, is_interactive) insts goals |>
+ tester ctxt insts goals |>
(fn result => if exists found_counterexample result then SOME result else NONE)) testers)
(fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();