--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML Sat Jun 13 10:01:00 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML Sat Jun 13 10:01:01 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 Sat Jun 13 10:01:00 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Sat Jun 13 10:01:01 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
@@ -323,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