--- 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 \<Colon> 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:
+ "(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))"
+proof
+ fix n :: int
+ assume "\<And>n\<Colon>code_int. PROP P n"
+ then show "PROP P (of_int n)" .
+next
+ fix n :: code_int
+ assume "\<And>n\<Colon>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 \<longleftrightarrow> k = l"
by (rule int_of_inject)
+lemma of_int_inject [simp]:
+ "of_int n = of_int m \<longleftrightarrow> n = m"
+ by (rule of_int_inject) (rule UNIV_I)+
+
+instantiation code_int :: equal
+begin
+
+definition
+ "HOL.equal k l \<longleftrightarrow> 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 \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
definition [simp, code del]:
"n < m \<longleftrightarrow> 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 \<Rightarrow> code_int \<Rightarrow> code_int \<times> 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 \<or> 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 \<Colon> code_int"
(Haskell "0")
@@ -78,6 +177,12 @@
code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
(Haskell "(_/ -/ _)")
+code_const div_mod_code_int
+ (Haskell "divMod")
+
+code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
+ (Haskell infix 4 "==")
+
code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> 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"
--- 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
--- 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);
--- 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)
--- 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 |
--- 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 |
--- 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 |
--- 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)
--- 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 **)
--- 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))
--- 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 =
--- 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 #>
--- 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:
"\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> 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
--- 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)