passing a term with free variables to the quickcheck tester functions instead of an lambda expression because this is more natural with passing further evaluation terms; added output of evaluation terms; added evaluation of terms in the exhaustive testing
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -211,6 +211,61 @@
(** building and compiling generator expressions **)
+fun mk_generator_expr ctxt (t, eval_terms) =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val ctxt' = Variable.auto_fixes t ctxt
+ val names = Term.add_free_names t []
+ val frees = map Free (Term.add_frees t [])
+ val ([depth_name], ctxt'') = Variable.variant_fixes ["depth"] ctxt'
+ val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") names) ctxt''
+ val depth = Free (depth_name, @{typ code_numeral})
+ val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
+ val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
+ val appendC = @{term "List.append :: term list => term list => term list"}
+ val return = @{term "Some :: term list => term list option"} $ (appendC $ terms $
+ (HOLogic.mk_list @{typ "term"} (map (fn t => HOLogic.mk_term_of (fastype_of t) t) eval_terms)))
+ fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
+ if Sign.of_sort thy (T, @{sort enum}) then
+ Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ lambda free (lambda term_var t))
+ else
+ Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ lambda free (lambda term_var t)) $ depth
+ val none_t = @{term "None :: term list option"}
+ fun mk_safe_if (cond, then_t, else_t) =
+ @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
+ (@{term "If :: bool => term list option => term list option => term list option"}
+ $ cond $ then_t $ else_t) $ none_t;
+ fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+ | strip_imp A = ([], A)
+ fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
+ fun mk_naive_test_term t =
+ fold_rev mk_exhaustive_closure (frees ~~ term_vars) (mk_safe_if (t, none_t, return))
+ fun mk_smart_test_term' concl bound_vars assms =
+ let
+ fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
+ val (vars, check) =
+ case assms of [] => (vars_of concl, (concl, none_t, return))
+ | assm :: assms => (vars_of assm, (assm,
+ mk_smart_test_term' concl (union (op =) (vars_of assm) bound_vars) assms, none_t))
+ in
+ fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
+ end
+ fun mk_smart_test_term t =
+ let
+ val (assms, concl) = strip_imp t
+ in
+ mk_smart_test_term' concl [] assms
+ end
+ val mk_test_term =
+ if Config.get ctxt smart_quantifier then mk_smart_test_term else mk_naive_test_term
+ in lambda depth (mk_test_term t) end
+
+(** generator compiliation **)
+
structure Counterexample = Proof_Data
(
type T = unit -> int -> term list option
@@ -229,76 +284,10 @@
val target = "Quickcheck";
-fun mk_smart_generator_expr ctxt t =
- let
- val thy = ProofContext.theory_of ctxt
- val ((vnames, Ts), t') = apfst split_list (strip_abs t)
- val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
- val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
- val (term_names, ctxt''') = Variable.variant_fixes (map (prefix "t_") vnames) ctxt''
- val depth = Free (depth_name, @{typ code_numeral})
- val frees = map2 (curry Free) names Ts
- val term_vars = map (fn n => Free (n, @{typ "unit => term"})) term_names
- fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
- | strip_imp A = ([], A)
- val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
- val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
- fun mk_exhaustive_closure (free as Free (_, T), term_var) t =
- if Sign.of_sort thy (T, @{sort enum}) then
- Const (@{const_name "Quickcheck_Exhaustive.check_all_class.check_all"}, check_allT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
- $ lambda free (lambda term_var t))
- else
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
- $ lambda free (lambda term_var t)) $ depth
- fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
- val none_t = @{term "None :: term list option"}
- fun mk_safe_if (cond, then_t, else_t) =
- @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
- (@{term "If :: bool => term list option => term list option => term list option"}
- $ cond $ then_t $ else_t) $ none_t;
- fun mk_test_term bound_vars assms =
- let
- fun vars_of t = subtract (op =) bound_vars (Term.add_free_names t [])
- val (vars, check) =
- case assms of [] =>
- (vars_of concl, (concl, none_t, @{term "Some :: term list => term list option"} $ terms))
- | assm :: assms =>
- (vars_of assm, (assm, mk_test_term (union (op =) (vars_of assm) bound_vars) assms, none_t))
- in
- fold_rev mk_exhaustive_closure (map lookup vars) (mk_safe_if check)
- end
- in lambda depth (mk_test_term [] assms) end
-
-fun mk_generator_expr ctxt t =
- let
- val Ts = (map snd o fst o strip_abs) t;
- val thy = ProofContext.theory_of ctxt
- val bound_max = length Ts - 1;
- val bounds = map_index (fn (i, ty) =>
- (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
- val result = list_comb (t, map (fn (i, _, _, _) => Bound i) bounds);
- val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
- val check =
- @{term "Quickcheck_Exhaustive.catch_match :: term list option => term list option => term list option"} $
- (@{term "If :: bool => term list option => term list option => term list option"}
- $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
- $ @{term "None :: term list option"};
- fun mk_exhaustive_closure (_, _, i, T) t =
- Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
- $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
- in Abs ("d", @{typ code_numeral}, fold_rev mk_exhaustive_closure bounds check) end
-
-(** generator compiliation **)
-
fun compile_generator_expr ctxt (t, eval_terms) =
let
val thy = ProofContext.theory_of ctxt
- val t' =
- (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
- ctxt t;
+ val t' = mk_generator_expr ctxt (t, eval_terms);
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
@@ -311,9 +300,7 @@
fun compile_generator_exprs ctxt ts =
let
val thy = ProofContext.theory_of ctxt
- val mk_generator_expr =
- if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr
- val ts' = map (mk_generator_expr ctxt) ts;
+ val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
val compiles = Code_Runtime.dynamic_value_strict
(Counterexample_Batch.get, put_counterexample_batch,
"Exhaustive_Generators.put_counterexample_batch")
@@ -323,7 +310,7 @@
map (fn compile => fn size => compile size
|> Option.map (map Quickcheck_Common.post_process_term)) compiles
end;
-
+
(** setup **)
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -216,12 +216,13 @@
fun compile_generator_expr ctxt (t, eval_terms) size =
let
val thy = ProofContext.theory_of ctxt
- val t' = if Config.get ctxt finite_functions then finitize_functions t else t
+ val t' = list_abs_free (Term.add_frees t [], t)
+ val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
val result = dynamic_value_strict
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
- thy (Option.map o map) (ensure_testable t') [] size
+ thy (Option.map o map) (ensure_testable t'') [] size
in
(result, NONE)
end;
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Fri Mar 18 18:19:42 2011 +0100
@@ -377,16 +377,17 @@
fun compile_generator_expr ctxt (t, eval_terms) =
let
- val Ts = (map snd o fst o strip_abs) t;
+ val t' = list_abs_free (Term.add_frees t [], t)
+ val Ts = (map snd o fst o strip_abs) t';
val thy = ProofContext.theory_of ctxt
val iterations = Config.get ctxt Quickcheck.iterations
in
if Config.get ctxt Quickcheck.report then
let
- val t' = mk_reporting_generator_expr thy t Ts;
+ val t'' = mk_reporting_generator_expr thy t' Ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (apfst o Option.map o map) proc) t'' [];
val single_tester = compile #> Random_Engine.run
fun iterate_and_collect size 0 report = (NONE, report)
| iterate_and_collect size j report =
@@ -404,10 +405,10 @@
end
else
let
- val t' = mk_generator_expr thy t Ts;
+ val t'' = mk_generator_expr thy t' Ts;
val compile = Code_Runtime.dynamic_value_strict
(Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
- thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t' [];
+ thy (SOME target) (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) t'' [];
val single_tester = compile #> Random_Engine.run
fun iterate size 0 = NONE
| iterate size j =
--- a/src/HOL/Tools/inductive_codegen.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Mar 18 18:19:42 2011 +0100
@@ -810,8 +810,9 @@
fun test_term ctxt (t, []) =
let
+ val t' = list_abs_free (Term.add_frees t [], t)
val thy = ProofContext.theory_of ctxt;
- val (xs, p) = strip_abs t;
+ val (xs, p) = strip_abs t';
val args' = map_index (fn (i, (_, T)) => ("arg" ^ string_of_int i, T)) xs;
val args = map Free args';
val (ps, q) = strip_imp p;
--- a/src/Tools/quickcheck.ML Fri Mar 18 18:19:42 2011 +0100
+++ b/src/Tools/quickcheck.ML Fri Mar 18 18:19:42 2011 +0100
@@ -35,10 +35,10 @@
-> Context.generic -> Context.generic
(* testing terms and proof states *)
val test_term: Proof.context -> bool * bool -> term * term list ->
- (string * term) list option * ((string * int) list * ((int * report) list) option)
+ ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option)
val test_goal_terms:
Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
- -> (string * term) list option * ((string * int) list * ((int * report) list) option) list
+ -> ((string * term) list * (term * term) list) option * ((string * int) list * ((int * report) list) option) list
val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
(* testing a batch of terms *)
val test_terms: Proof.context -> term list -> (string * term) list option list option
@@ -158,14 +158,13 @@
(* testing propositions *)
-fun prep_test_term t =
+fun check_test_term t =
let
val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
error "Term to be tested contains type variables";
val _ = null (Term.add_vars t []) orelse
error "Term to be tested contains schematic variables";
- val frees = Term.add_frees t [];
- in (frees, list_abs_free (frees, t)) end
+ in () end
fun cpu_time description f =
let
@@ -182,14 +181,22 @@
else
f ()
+fun mk_result names eval_terms ts =
+ let
+ val (ts1, ts2) = chop (length names) ts
+ in
+ (names ~~ ts1, eval_terms ~~ ts2)
+ end
+
fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
let
- val (names, t') = apfst (map fst) (prep_test_term t);
+ val _ = check_test_term t
+ val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
fun excipit s =
"Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
val (test_fun, comp_time) = cpu_time "quickcheck compilation"
- (fn () => mk_tester ctxt (t', eval_terms));
+ (fn () => mk_tester ctxt (t, eval_terms));
fun with_size test_fun k reports =
if k > Config.get ctxt size then
(NONE, reports)
@@ -212,7 +219,7 @@
val ((result, reports), exec_time) =
cpu_time "quickcheck execution" (fn () => with_size test_fun 1 [])
in
- (case result of NONE => NONE | SOME ts => SOME (names ~~ ts),
+ (Option.map (mk_result names eval_terms) result,
([exec_time, comp_time],
if Config.get ctxt report andalso not (null reports) then SOME reports else NONE))
end) (fn () => error (excipit "ran out of time")) ()
@@ -220,8 +227,9 @@
fun test_terms ctxt ts =
let
- val (namess, ts') = split_list (map (fn t => apfst (map fst) (prep_test_term t)) ts)
- val test_funs = mk_batch_tester ctxt ts'
+ val _ = map check_test_term ts
+ val namess = map (fn t => Term.add_free_names t []) ts
+ val test_funs = mk_batch_tester ctxt ts
fun with_size tester k =
if k > Config.get ctxt size then NONE
else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1)
@@ -240,14 +248,15 @@
let
val thy = ProofContext.theory_of ctxt
val (ts, eval_terms) = split_list ts
- val (freess, ts') = split_list (map prep_test_term ts)
- val Ts = map snd (hd freess)
+ val _ = map check_test_term ts
+ val names = Term.add_free_names (hd ts) []
+ val Ts = map snd (Term.add_frees (hd ts) [])
val (test_funs, comp_time) = cpu_time "quickcheck compilation"
- (fn () => map (mk_tester ctxt) (ts' ~~ eval_terms))
+ (fn () => map (mk_tester ctxt) (ts ~~ eval_terms))
fun test_card_size (card, size) =
(* FIXME: why decrement size by one? *)
case fst (the (nth test_funs (card - 1)) (size - 1)) of
- SOME ts => SOME (map fst (nth freess (card - 1)) ~~ ts)
+ SOME ts => SOME (mk_result names (nth eval_terms (card - 1)) ts)
| NONE => NONE
val enumeration_card_size =
if forall (fn T => Sign.of_sort thy (T, ["Enum.enum"])) Ts then
@@ -365,10 +374,14 @@
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck"
fun pretty_counterex ctxt auto NONE = Pretty.str (tool_name auto ^ " found no counterexample.")
- | pretty_counterex ctxt auto (SOME cex) =
- Pretty.chunks (Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
+ | pretty_counterex ctxt auto (SOME (cex, eval_terms)) =
+ Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex));
+ Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
+ @ (Pretty.str ("Evaluated terms:\n") ::
+ map (fn (t, u) =>
+ Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
+ (rev eval_terms)));
fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
@@ -481,7 +494,7 @@
| (NONE, _) => if expect (Proof.context_of state') = Counterexample then
error ("quickcheck expected to find a counterexample but did not find one") else ()))
-fun quickcheck args i state = fst (gen_quickcheck args i state);
+fun quickcheck args i state = Option.map fst (fst (gen_quickcheck args i state));
fun quickcheck_cmd args i state =
gen_quickcheck args i (Toplevel.proof_of state)