--- a/NEWS Sun Jun 14 03:02:25 2009 +0200
+++ b/NEWS Sun Jun 14 09:11:51 2009 +0200
@@ -37,6 +37,9 @@
* New method "linarith" invokes existing linear arithmetic decision
procedure only.
+* Implementation of quickcheck using generic code generator; default generators
+are provided for all suitable HOL types, records and datatypes.
+
*** ML ***
--- a/src/HOL/Quickcheck.thy Sun Jun 14 03:02:25 2009 +0200
+++ b/src/HOL/Quickcheck.thy Sun Jun 14 09:11:51 2009 +0200
@@ -93,15 +93,15 @@
\<Rightarrow> (Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed) \<Rightarrow> (Random.seed \<Rightarrow> Random.seed \<times> Random.seed)
\<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed"
-definition random_fun_lift :: "(code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
- \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
- "random_fun_lift f i = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of (f i) Random.split_seed"
+definition random_fun_lift :: "(Random.seed \<Rightarrow> ('b \<times> (unit \<Rightarrow> term)) \<times> Random.seed)
+ \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
+ "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
begin
definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
- "random = random_fun_lift random"
+ "random i = random_fun_lift (random i)"
instance ..
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 14 03:02:25 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sun Jun 14 09:11:51 2009 +0200
@@ -15,13 +15,7 @@
structure DatatypeCodegen : DATATYPE_CODEGEN =
struct
-(** SML code generator **)
-
-open Codegen;
-
-(**** datatype definition ****)
-
-(* find shortest path to constructor with no recursive arguments *)
+(** find shortest path to constructor with no recursive arguments **)
fun find_nonempty (descr: DatatypeAux.descr) is i =
let
@@ -41,6 +35,13 @@
fun find_shortest_path descr i = find_nonempty descr [i] i;
+
+(** SML code generator **)
+
+open Codegen;
+
+(* datatype definition *)
+
fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
let
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
@@ -210,7 +211,7 @@
end;
-(**** case expressions ****)
+(* case expressions *)
fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
let val i = length constrs
@@ -252,7 +253,7 @@
end;
-(**** constructors ****)
+(* constructors *)
fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
let val i = length args
@@ -271,7 +272,7 @@
end;
-(**** code generators for terms and types ****)
+(* code generators for terms and types *)
fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
(c as Const (s, T), ts) =>
@@ -313,6 +314,18 @@
(** generic code generator **)
+(* liberal addition of code data for datatypes *)
+
+fun mk_constr_consts thy vs dtco cos =
+ let
+ val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+ val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
+ in if is_some (try (Code.constrset_of_consts thy) cs')
+ then SOME cs
+ else NONE
+ end;
+
+
(* case certificates *)
fun mk_case_cert thy tyco =
@@ -371,7 +384,7 @@
val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss
addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms))
addsimprocs [DatatypePackage.distinct_simproc]);
- fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+ fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
|> Simpdata.mk_eq;
in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
@@ -411,16 +424,7 @@
end;
-(* liberal addition of code data for datatypes *)
-
-fun mk_constr_consts thy vs dtco cos =
- let
- val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
- val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
- in if is_some (try (Code.constrset_of_consts thy) cs')
- then SOME cs
- else NONE
- end;
+(* register a datatype etc. *)
fun add_all_code dtcos thy =
let
@@ -433,6 +437,7 @@
in
if null css then thy
else thy
+ |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs
@@ -440,7 +445,6 @@
end;
-
(** theory setup **)
val setup =
--- a/src/HOL/Tools/quickcheck_generators.ML Sun Jun 14 03:02:25 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sun Jun 14 09:11:51 2009 +0200
@@ -170,9 +170,9 @@
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
val ((_, eqs2), lthy') = PrimrecPackage.add_primrec_simple
[((Binding.name random_aux, T), NoSyn)] eqs1 lthy;
- val eq_tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (simp_tac rew_ss)
+ val eq_tac = ALLGOALS (simp_tac rew_ss)
THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)));
- val eqs3 = Goal.prove_multi lthy' [v] [] eqs0 (K eq_tac);
+ val eqs3 = map (fn prop => SkipProof.prove lthy' [v] [] prop (K eq_tac)) eqs0;
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
@@ -180,7 +180,7 @@
[(cT_random_aux, cert t_random_aux), (cT_rhs, cert t_rhs)])
|> (fn thm => thm OF eqs3);
val tac = ALLGOALS (rtac rule);
- val simp = Goal.prove lthy' [v] [] eq (K tac);
+ val simp = SkipProof.prove lthy' [v] [] eq (K tac);
in (simp, lthy') end;
end;
@@ -212,11 +212,11 @@
fun prove_eqs aux_simp proj_defs lthy =
let
val proj_simps = map (snd o snd) proj_defs;
- fun tac { context = ctxt, ... } = ALLGOALS Goal.conjunction_tac
- THEN ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
+ fun tac { context = ctxt, ... } =
+ ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
- in (Goal.prove_multi lthy [v] [] eqs tac, lthy) end;
+ in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
in
lthy
|> random_aux_primrec aux_eq'
@@ -235,10 +235,9 @@
val proto_eqs = map mk_proto_eq eqs;
fun prove_simps proto_simps lthy =
let
- val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
- val tac = ALLGOALS Goal.conjunction_tac
- THEN ALLGOALS (ProofContext.fact_tac ext_simps);
- in (Goal.prove_multi lthy vs [] eqs (K tac), lthy) end;
+ val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
+ val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
+ in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
val b = Binding.qualify true prefix (Binding.name "simps");
in
lthy
@@ -254,8 +253,6 @@
(* constructing random instances on datatypes *)
-exception Datatype_Fun; (*FIXME*)
-
fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
let
val mk_const = curry (Sign.mk_const thy);
@@ -274,19 +271,20 @@
val random_auxT = sizeT o random_resultT;
val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT))
random_auxsN rTs;
-
fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T));
fun mk_random_aux_call fTs (k, _) (tyco, Ts) =
let
- val _ = if null fTs then () else raise Datatype_Fun; (*FIXME*)
- val random = nth random_auxs k;
+ val T = Type (tyco, Ts);
+ fun mk_random_fun_lift [] t = t
+ | mk_random_fun_lift (fT :: fTs) t =
+ mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
+ mk_random_fun_lift fTs t;
+ val t = mk_random_fun_lift fTs (nth random_auxs k $ i1 $ j);
val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
|> the_default 0;
- in (SOME size, (random $ i1 $ j, Type (tyco, Ts))) end;
-
+ in (SOME size, (t, fTs ---> T)) end;
val tss = DatatypeAux.interpret_construction descr vs
{ atyp = mk_random_call, dtyp = mk_random_aux_call };
-
fun mk_consexpr simpleT (c, xs) =
let
val (ks, simple_tTs) = split_list xs;
@@ -324,6 +322,7 @@
fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
let
+ val _ = DatatypeAux.message "Creating quickcheck generators ...";
val i = @{term "i\<Colon>code_numeral"};
val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
@@ -347,35 +346,39 @@
|> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
end;
+fun perhaps_constrain thy insts raw_vs =
+ let
+ fun meet_random (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
+ (Logic.varifyT T, sort);
+ val vtab = Vartab.empty
+ |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
+ |> fold meet_random insts;
+ in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
+ end handle CLASS_ERROR => NONE;
+
fun ensure_random_datatype raw_tycos thy =
let
val pp = Syntax.pp_global thy;
val algebra = Sign.classes_of thy;
val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
DatatypePackage.the_datatype_descr thy raw_tycos;
- val aTs = (flat o maps snd o maps snd) (DatatypeAux.interpret_construction descr raw_vs
- { atyp = single, dtyp = K o K });
- fun meet_random T = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT T, @{sort random});
- val vtab = (Vartab.empty
- |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet_random aTs
- |> SOME) handle CLASS_ERROR => NONE;
- val vconstrain = case vtab of SOME vtab => (fn (v, _) =>
- (v, (the o Vartab.lookup vtab) (v, 0)))
- | NONE => I;
- val vs = map vconstrain raw_vs;
- val constrain = map_atyps (fn TFree v => TFree (vconstrain v));
+ val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
+ (DatatypeAux.interpret_construction descr raw_vs { atyp = single, dtyp = (K o K o K) [] });
+ val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
+ (DatatypeAux.interpret_construction descr raw_vs { atyp = K [], dtyp = K o K });
val has_inst = exists (fn tyco =>
can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
- in if is_some vtab andalso not has_inst then
- (mk_random_datatype descr vs tycos (names, auxnames)
- ((pairself o map) constrain raw_TUs) thy
- (*FIXME ephemeral handles*)
- handle Datatype_Fun => thy
- | e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
- | e as TYPE (msg, _, _) => (tracing msg; raise e)
- | e as ERROR msg => (tracing msg; raise e))
- else thy end;
+ in if has_inst then thy
+ else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
+ of SOME constrain => (mk_random_datatype descr
+ (map constrain raw_vs) tycos (names, auxnames)
+ ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+ (*FIXME ephemeral handles*)
+ handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e)
+ | e as TYPE (msg, _, _) => (tracing msg; raise e)
+ | e as ERROR msg => (tracing msg; raise e))
+ | NONE => thy
+ end;
(** setup **)