# HG changeset patch # User bulwahn # Date 1300468782 -3600 # Node ID bd6515e113b257ffdc73578348944b3e97363e59 # Parent 5e40c152c3963c34f4db00cfa77eb0fe43f16c0f 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 diff -r 5e40c152c396 -r bd6515e113b2 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- 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 **) diff -r 5e40c152c396 -r bd6515e113b2 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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; diff -r 5e40c152c396 -r bd6515e113b2 src/HOL/Tools/Quickcheck/random_generators.ML --- 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 = diff -r 5e40c152c396 -r bd6515e113b2 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 5e40c152c396 -r bd6515e113b2 src/Tools/quickcheck.ML --- 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)