# HG changeset patch # User bulwahn # Date 1300692556 -3600 # Node ID 143f3719491102573f678ae3e5a2b05d58883694 # Parent 2de57cda5b24187b10aaa0aa8eada96358940e4c# Parent 878f33040280b91677181bc8b6b738e49a839d39 merged diff -r 878f33040280 -r 143f37194911 src/HOL/Library/Quickcheck_Narrowing.thy --- a/src/HOL/Library/Quickcheck_Narrowing.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy Mon Mar 21 08:29:16 2011 +0100 @@ -25,15 +25,67 @@ typedef (open) code_int = "UNIV \ int set" morphisms int_of of_int by rule +lemma of_int_int_of [simp]: + "of_int (int_of k) = k" + by (rule int_of_inverse) + +lemma int_of_of_int [simp]: + "int_of (of_int n) = n" + by (rule of_int_inverse) (rule UNIV_I) + +lemma code_int: + "(\n\code_int. PROP P n) \ (\n\int. PROP P (of_int n))" +proof + fix n :: int + assume "\n\code_int. PROP P n" + then show "PROP P (of_int n)" . +next + fix n :: code_int + assume "\n\int. PROP P (of_int n)" + then have "PROP P (of_int (int_of n))" . + then show "PROP P n" by simp +qed + + lemma int_of_inject [simp]: "int_of k = int_of l \ k = l" by (rule int_of_inject) +lemma of_int_inject [simp]: + "of_int n = of_int m \ n = m" + by (rule of_int_inject) (rule UNIV_I)+ + +instantiation code_int :: equal +begin + +definition + "HOL.equal k l \ HOL.equal (int_of k) (int_of l)" + +instance proof +qed (auto simp add: equal_code_int_def equal_int_def eq_int_refl) + +end + +instantiation code_int :: number +begin + +definition + "number_of = of_int" + +instance .. + +end + +lemma int_of_number [simp]: + "int_of (number_of k) = number_of k" + by (simp add: number_of_code_int_def number_of_is_id) + + definition nat_of :: "code_int => nat" where "nat_of i = nat (int_of i)" -instantiation code_int :: "{zero, one, minus, linorder}" +instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}" begin definition [simp, code del]: @@ -43,16 +95,29 @@ "1 = of_int 1" definition [simp, code del]: + "n + m = of_int (int_of n + int_of m)" + +definition [simp, code del]: "n - m = of_int (int_of n - int_of m)" definition [simp, code del]: + "n * m = of_int (int_of n * int_of m)" + +definition [simp, code del]: + "n div m = of_int (int_of n div int_of m)" + +definition [simp, code del]: + "n mod m = of_int (int_of n mod int_of m)" + +definition [simp, code del]: "n \ m \ int_of n \ int_of m" definition [simp, code del]: "n < m \ int_of n < int_of m" -instance proof qed (auto) +instance proof +qed (auto simp add: code_int left_distrib zmult_zless_mono2) end (* @@ -69,6 +134,40 @@ using one_code_numeral_code .. *) +definition div_mod_code_int :: "code_int \ code_int \ code_int \ code_int" where + [code del]: "div_mod_code_int n m = (n div m, n mod m)" + +lemma [code]: + "div_mod_code_int n m = (if m = 0 then (0, n) else (n div m, n mod m))" + unfolding div_mod_code_int_def by auto + +lemma [code]: + "n div m = fst (div_mod_code_int n m)" + unfolding div_mod_code_int_def by simp + +lemma [code]: + "n mod m = snd (div_mod_code_int n m)" + unfolding div_mod_code_int_def by simp + +lemma int_of_code [code]: + "int_of k = (if k = 0 then 0 + else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))" +proof - + have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k" + by (rule mod_div_equality) + have "int_of k mod 2 = 0 \ int_of k mod 2 = 1" by auto + from this show ?thesis + apply auto + apply (insert 1) by (auto simp add: mult_ac) +qed + + +code_instance code_numeral :: equal + (Haskell -) + +setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int} + false Code_Printer.literal_numeral) ["Haskell"] *} + code_const "0 \ code_int" (Haskell "0") @@ -78,6 +177,12 @@ code_const "minus \ code_int \ code_int \ code_int" (Haskell "(_/ -/ _)") +code_const div_mod_code_int + (Haskell "divMod") + +code_const "HOL.equal \ code_int \ code_int \ bool" + (Haskell infix 4 "==") + code_const "op \ \ code_int \ code_int \ bool" (Haskell infix 4 "<=") @@ -87,6 +192,8 @@ code_type code_int (Haskell "Int") +code_abort of_int + subsubsection {* Narrowing's deep representation of types and terms *} datatype type = SumOfProd "type list list" @@ -207,7 +314,20 @@ definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing" where "cons2 f = apply (apply (cons f) narrowing) narrowing" - + +definition drawn_from :: "'a list => 'a cons" +where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)" + +instantiation int :: narrowing +begin + +definition + "narrowing_int d = (let i = Quickcheck_Narrowing.int_of d in drawn_from [-i .. i])" + +instance .. + +end + instantiation unit :: narrowing begin @@ -338,6 +458,27 @@ declare simp_thms(17,19)[code del] +subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *} + +datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun" + +primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b" +where + "eval_ffun (Constant c) x = c" +| "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)" + +hide_type (open) ffun +hide_const (open) Constant Update eval_ffun + +datatype 'b cfun = Constant 'b + +primrec eval_cfun :: "'b cfun => 'a => 'b" +where + "eval_cfun (Constant c) y = c" + +hide_type (open) cfun +hide_const (open) Constant eval_cfun + subsubsection {* Setting up the counterexample generator *} use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML" diff -r 878f33040280 -r 143f37194911 src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Library/SML_Quickcheck.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,7 +8,7 @@ setup {* Inductive_Codegen.quickcheck_setup #> Context.theory_map (Quickcheck.add_generator ("SML", - fn ctxt => fn t => + fn ctxt => fn (t, eval_terms) => let val test_fun = Codegen.test_term ctxt t val iterations = Config.get ctxt Quickcheck.iterations diff -r 878f33040280 -r 143f37194911 src/HOL/Mutabelle/mutabelle.ML --- a/src/HOL/Mutabelle/mutabelle.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle.ML Mon Mar 21 08:29:16 2011 +0100 @@ -500,18 +500,18 @@ |> Config.put Quickcheck.size 1 |> Config.put Quickcheck.iterations 1 |> Config.put Quickcheck.tester (!testgen_name)) - (true, 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)); fun qc_recursive usedthy [] insts sz qciter acc = rev acc | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs)); - ((x, pretty (the_default [] (fst (Quickcheck.test_term + ((x, pretty (the_default [] (Option.map fst (fst (Quickcheck.test_term ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter #> Config.put Quickcheck.tester (!testgen_name)) (ProofContext.init_global usedthy)) - (true, 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); diff -r 878f33040280 -r 143f37194911 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Mar 21 08:29:16 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, 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, false) [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt))) + (false, false) [])) (map (rpair [] o 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) diff -r 878f33040280 -r 143f37194911 src/HOL/Predicate_Compile_Examples/IMP_1.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF. *} -types - var = unit - state = bool +type_synonym var = unit +type_synonym state = bool datatype com = Skip | diff -r 878f33040280 -r 143f37194911 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While. *} -types - var = unit - state = bool +type_synonym var = unit +type_synonym state = bool datatype com = Skip | diff -r 878f33040280 -r 143f37194911 src/HOL/Predicate_Compile_Examples/IMP_3.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Mon Mar 21 08:29:16 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While. *} -types - var = unit - state = int +type_synonym var = unit +type_synonym state = int datatype com = Skip | diff -r 878f33040280 -r 143f37194911 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Mar 21 08:29:16 2011 +0100 @@ -22,7 +22,7 @@ val tracing : bool Unsynchronized.ref; val quiet : bool Unsynchronized.ref; val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int -> - Proof.context -> term -> int -> term list option * Quickcheck.report option; + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option; (* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *) val nrandom : int Unsynchronized.ref; val debug : bool Unsynchronized.ref; @@ -215,11 +215,12 @@ let val ({cpu, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds cpu)) end -fun compile_term compilation options ctxt t = +fun compile_term compilation options ctxt (t, eval_terms) = let + val t' = list_abs_free (Term.add_frees t [], t) val thy = Theory.copy (ProofContext.theory_of ctxt) val ((((full_constname, constT), vs'), intro), thy1) = - Predicate_Compile_Aux.define_quickcheck_predicate t thy + Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 val (thy3, preproc_time) = cpu_time "predicate preprocessing" (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2) diff -r 878f33040280 -r 143f37194911 src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Mon Mar 21 08:29:16 2011 +0100 @@ -7,7 +7,7 @@ signature EXHAUSTIVE_GENERATORS = sig val compile_generator_expr: - Proof.context -> term -> int -> term list option * Quickcheck.report option + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option val compile_generator_exprs: Proof.context -> term list -> (int -> term list option) list val put_counterexample: (unit -> int -> term list option) @@ -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 = +fun compile_generator_expr ctxt (t, eval_terms) = 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 = - 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 878f33040280 -r 143f37194911 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 21 08:29:16 2011 +0100 @@ -7,14 +7,21 @@ signature NARROWING_GENERATORS = sig val compile_generator_expr: - Proof.context -> term -> int -> term list option * Quickcheck.report option + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context + val finite_functions : bool Config.T val setup: theory -> theory end; structure Narrowing_Generators : NARROWING_GENERATORS = struct +(* configurations *) + +val (finite_functions, setup_finite_functions) = + Attrib.config_bool "quickcheck_finite_functions" (K true) + + fun mk_undefined T = Const(@{const_name undefined}, T) (* narrowing specific names and types *) @@ -118,7 +125,7 @@ fun exec verbose code = ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) -fun value ctxt (get, put, put_ml) (code, value) = +fun value ctxt (get, put, put_ml) (code, value) size = let val tmp_prefix = "Quickcheck_Narrowing" fun run in_path = @@ -129,7 +136,7 @@ val main = "module Main where {\n\n" ^ "import Narrowing_Engine;\n" ^ "import Code;\n\n" ^ - "main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^ + "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^ "}\n" val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n" (unprefix "module Code where {" code) @@ -147,6 +154,7 @@ val result = Isabelle_System.with_tmp_dir tmp_prefix run val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result) + |> translate_string (fn s => if s = "\\" then "\\\\" else s) val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))"; val ctxt' = ctxt @@ -154,18 +162,18 @@ |> Context.proof_map (exec false ml_code); in get ctxt' () end; -fun evaluation cookie thy evaluator vs_t args = +fun evaluation cookie thy evaluator vs_t args size = let val ctxt = ProofContext.init_global thy; val (program_code, value_name) = evaluator vs_t; val value_code = space_implode " " (value_name :: "()" :: map (enclose "(" ")") args); - in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; + in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end; -fun dynamic_value_strict cookie thy postproc t args = +fun dynamic_value_strict cookie thy postproc t args size = let fun evaluator naming program ((_, vs_ty), t) deps = - evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args; + evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size; in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; (* counterexample generator *) @@ -176,24 +184,54 @@ fun init _ () = error "Counterexample" ) -val put_counterexample = Counterexample.put - -fun compile_generator_expr ctxt t size = +val put_counterexample = Counterexample.put + +fun finitize_functions t = + let + val ((names, Ts), t') = apfst split_list (strip_abs t) + fun mk_eval_ffun dT rT = + Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, + Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT) + fun mk_eval_cfun dT rT = + Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, + Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT) + fun eval_function (T as Type (@{type_name fun}, [dT, rT])) = + let + val (rt', rT') = eval_function rT + in + case dT of + Type (@{type_name fun}, _) => + (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)), + Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT'])) + | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)), + Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT'])) + end + | eval_function T = (I, T) + val (tt, Ts') = split_list (map eval_function Ts) + val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t') + in + list_abs (names ~~ Ts', t'') + end + +fun compile_generator_expr ctxt (t, eval_terms) size = let val thy = ProofContext.theory_of ctxt + 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 t = dynamic_value_strict + val result = dynamic_value_strict (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample") - thy (Option.map o map) (ensure_testable t) [] + thy (Option.map o map) (ensure_testable t'') [] size in - (t, NONE) + (result, NONE) end; val setup = Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype)) + #> setup_finite_functions #> Context.theory_map (Quickcheck.add_generator ("narrowing", compile_generator_expr)) diff -r 878f33040280 -r 143f37194911 src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Mon Mar 21 08:29:16 2011 +0100 @@ -11,7 +11,7 @@ -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) -> seed -> (('a -> 'b) * (unit -> term)) * seed val compile_generator_expr: - Proof.context -> term -> int -> term list option * Quickcheck.report option + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option val put_counterexample: (unit -> int -> seed -> term list option * seed) -> Proof.context -> Proof.context val put_counterexample_report: (unit -> int -> seed -> (term list option * (bool list * bool)) * seed) @@ -375,18 +375,19 @@ val empty_report = Quickcheck.Report { iterations = 0, raised_match_errors = 0, satisfied_assms = [], positive_concl_tests = 0 } -fun compile_generator_expr ctxt t = +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 878f33040280 -r 143f37194911 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Mar 21 08:29:16 2011 +0100 @@ -9,7 +9,7 @@ val add : string option -> int option -> attribute val test_fn : (int * int * int -> term list option) Unsynchronized.ref (* FIXME *) val test_term: - Proof.context -> term -> int -> term list option * Quickcheck.report option + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option val setup : theory -> theory val quickcheck_setup : theory -> theory end; @@ -808,10 +808,11 @@ val (random_values, setup_random_values) = Attrib.config_int "ind_quickcheck_random" (K 5); val (size_offset, setup_size_offset) = Attrib.config_int "ind_quickcheck_size_offset" (K 0); -fun test_term ctxt t = +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; @@ -854,7 +855,8 @@ fun test k = (deepen bound (fn i => (Output.urgent_message ("Search depth: " ^ string_of_int i); test_fn' (i, values, k+offset))) start, NONE); - in test end; + in test end + | test_term ctxt (t, _) = error "Option eval is not supported by tester SML_inductive"; val quickcheck_setup = setup_depth_bound #> diff -r 878f33040280 -r 143f37194911 src/HOL/ex/Quickcheck_Narrowing_Examples.thy --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Sun Mar 20 23:07:06 2011 +0100 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Mon Mar 21 08:29:16 2011 +0100 @@ -9,16 +9,62 @@ imports "~~/src/HOL/Library/Quickcheck_Narrowing" begin +subsection {* Minimalistic examples *} +(* +lemma + "x = y" +quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] +oops +*) +(* +lemma + "x = y" +quickcheck[tester = narrowing, finite_types = true, expect = counterexample] +oops +*) + subsection {* Simple list examples *} lemma "rev xs = xs" -quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] + quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample] +oops + +lemma "rev xs = xs" + quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample] +oops + +lemma "rev xs = xs" + quickcheck[tester = narrowing, finite_types = true, expect = counterexample] +oops + +subsection {* Simple examples with functions *} + +declare [[quickcheck_finite_functions]] + +lemma "map f xs = map g xs" + quickcheck[tester = narrowing, finite_types = true, expect = counterexample] oops -text {* Example fails due to some strange thing... *} -(* -lemma "rev xs = xs" -quickcheck[tester = lazy_exhaustive, finite_types = true] +lemma "map f xs = map f ys ==> xs = ys" + quickcheck[tester = narrowing, finite_types = true, expect = counterexample] +oops + +lemma + "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)" + quickcheck[tester = narrowing, expect = counterexample] +oops + +lemma "map f xs = F f xs" + quickcheck[tester = narrowing, finite_types = true, expect = counterexample] +oops + +lemma "map f xs = F f xs" + quickcheck[tester = narrowing, finite_types = false, expect = counterexample] +oops + +(* requires some work... +lemma "R O S = S O R" + quickcheck[tester = narrowing, size = 2] oops *) @@ -117,7 +163,7 @@ lemma is_ord_l_bal: "\ is_ord(MKT (x :: nat) l r h); height l = height r + 2 \ \ is_ord(l_bal(x,l,r))" -quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample] +quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 100, expect = counterexample] oops diff -r 878f33040280 -r 143f37194911 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Sun Mar 20 23:07:06 2011 +0100 +++ b/src/Tools/quickcheck.ML Mon Mar 21 08:29:16 2011 +0100 @@ -28,17 +28,17 @@ val map_test_params : (typ list * expectation -> typ list * expectation) -> Context.generic -> Context.generic val add_generator: - string * (Proof.context -> term -> int -> term list option * report option) + string * (Proof.context -> term * term list -> int -> term list option * report option) -> Context.generic -> Context.generic val add_batch_generator: string * (Proof.context -> term list -> (int -> term list option) list) -> Context.generic -> Context.generic (* testing terms and proof states *) - val test_term: Proof.context -> bool * bool -> term -> - (string * term) list option * ((string * int) list * ((int * report) list) option) + val test_term: Proof.context -> bool * bool -> term * term list -> + ((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 list - -> (string * term) list option * ((string * int) list * ((int * report) list) option) list + Proof.context -> bool * bool -> (string * typ) list -> (term * term list) 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 @@ -109,7 +109,7 @@ structure Data = Generic_Data ( type T = - ((string * (Proof.context -> term -> int -> term list option * report option)) list + ((string * (Proof.context -> term * term list -> int -> term list option * report option)) list * (string * (Proof.context -> term list -> (int -> term list option) list)) list) * test_params; val empty = (([], []), Test_Params {default_type = [], expect = No_Expectation}); @@ -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 e = let val ({cpu, ...}, result) = Timing.timing e () @@ -179,13 +178,22 @@ else f () -fun test_term ctxt (limit_time, is_interactive) t = +fun mk_result names eval_terms ts = let - val (names, t') = apfst (map fst) (prep_test_term t); + 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 _ = 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'); + val (test_fun, comp_time) = cpu_time "quickcheck compilation" + (fn () => mk_tester ctxt (t, eval_terms)); fun with_size test_fun k reports = if k > Config.get ctxt size then (NONE, reports) @@ -208,7 +216,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")) () @@ -216,8 +224,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) @@ -235,14 +244,16 @@ 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) - val Ts = map snd (hd freess) + val (ts, eval_terms) = split_list ts + 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') + (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 @@ -287,22 +298,23 @@ | subst T = T; in (map_types o map_atyps) subst end; -datatype wellsorted_error = Wellsorted_Error of string | Term of term +datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list fun test_goal_terms lthy (limit_time, is_interactive) insts check_goals = let + fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) val thy = ProofContext.theory_of lthy val default_insts = if Config.get lthy finite_types then (get_finite_types lthy) else (default_type lthy) val inst_goals = - map (fn check_goal => + map (fn (check_goal, eval_terms) => if not (null (Term.add_tfree_names check_goal [])) then map (fn T => - (pair (SOME T) o Term o Object_Logic.atomize_term thy o monomorphic_term thy insts T) - check_goal + (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) + (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) handle WELLSORTED s => (SOME T, Wellsorted_Error s)) default_insts else - [(NONE, Term (Object_Logic.atomize_term thy check_goal))]) check_goals + [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) check_goals val error_msg = cat_lines (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) @@ -329,7 +341,7 @@ collect_results (test_term lthy (limit_time, is_interactive)) [] (maps (map snd) correct_inst_goals) end; -fun test_goal (time_limit, is_interactive) insts i state = +fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state = let val lthy = Proof.context_of state; val thy = Proof.theory_of state; @@ -346,9 +358,10 @@ | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy); val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi)); val check_goals = case some_locale - of NONE => [proto_goal] - | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) - (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); + of NONE => [(proto_goal, eval_terms)] + | SOME locale => + map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms)) + (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale); in test_goal_terms lthy (time_limit, is_interactive) insts check_goals end @@ -358,10 +371,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}) = @@ -395,7 +412,7 @@ val res = state |> Proof.map_context (Config.put report false #> Config.put quiet true) - |> try (test_goal (false, false) [] 1); + |> try (test_goal (false, false) ([], []) 1); in case res of NONE => (false, state) @@ -455,24 +472,26 @@ Config.put_generic tester name genctxt else error ("Unknown tester or test parameter: " ^ name); -fun parse_test_param_inst (name, arg) (insts, ctxt) = +fun parse_test_param_inst (name, arg) ((insts, eval_terms), ctxt) = case try (ProofContext.read_typ ctxt) name - of SOME (TFree (v, _)) => (apfst o AList.update (op =)) - (v, ProofContext.read_typ ctxt (the_single arg)) (insts, ctxt) - | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) (insts, ctxt); + of SOME (TFree (v, _)) => + ((AList.update (op =) (v, ProofContext.read_typ ctxt (the_single arg)) insts, eval_terms), ctxt) + | NONE => (case name of + "eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), ctxt) + | _ => ((insts, eval_terms), Context.proof_map (parse_test_param (name, arg)) ctxt)); fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args); 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, true) insts i state' + |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args (([], []), ctxt)) + |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) 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 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)