--- a/src/HOL/HOL.thy Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/HOL.thy Mon May 18 09:47:34 2009 +0200
@@ -1987,6 +1987,18 @@
subsubsection {* Quickcheck *}
+ML {*
+structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
+(
+ val name = "quickcheck_recfun_simp"
+ val description = "simplification rules of recursive functions as needed by Quickcheck"
+)
+*}
+
+setup {*
+ Quickcheck_RecFun_Simp_Thms.setup
+*}
+
setup {*
Quickcheck.add_generator ("SML", Codegen.test_term)
*}
--- a/src/HOL/Nominal/nominal_inductive.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon May 18 09:47:34 2009 +0200
@@ -561,7 +561,7 @@
(strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
[ind_case_names, RuleCases.consumes 1]);
- val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
+ val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
((rec_qualified (Binding.name "strong_induct"),
map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
ctxt;
@@ -569,12 +569,12 @@
ProjectRule.projects ctxt (1 upto length names) strong_induct'
in
ctxt' |>
- LocalTheory.note Thm.theoremK
+ LocalTheory.note Thm.generated_theoremK
((rec_qualified (Binding.name "strong_inducts"),
[Attrib.internal (K ind_case_names),
Attrib.internal (K (RuleCases.consumes 1))]),
strong_inducts) |> snd |>
- LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
+ LocalTheory.notes Thm.generated_theoremK (map (fn ((name, elim), (_, cases)) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
[Attrib.internal (K (RuleCases.case_names (map snd cases))),
Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
@@ -664,7 +664,7 @@
end) atoms
in
ctxt |>
- LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
+ LocalTheory.notes Thm.generated_theoremK (map (fn (name, ths) =>
((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
[Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
(names ~~ transp thss)) |> snd
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Mon May 18 09:47:34 2009 +0200
@@ -461,7 +461,7 @@
(strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
else (strong_raw_induct RSN (2, rev_mp),
[ind_case_names, RuleCases.consumes 1]);
- val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.theoremK
+ val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generated_theoremK
((rec_qualified (Binding.name "strong_induct"),
map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
ctxt;
@@ -469,7 +469,7 @@
ProjectRule.projects ctxt' (1 upto length names) strong_induct'
in
ctxt' |>
- LocalTheory.note Thm.theoremK
+ LocalTheory.note Thm.generated_theoremK
((rec_qualified (Binding.name "strong_inducts"),
[Attrib.internal (K ind_case_names),
Attrib.internal (K (RuleCases.consumes 1))]),
--- a/src/HOL/Nominal/nominal_primrec.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon May 18 09:47:34 2009 +0200
@@ -367,11 +367,11 @@
(fn thss => fn goal_ctxt =>
let
val simps = ProofContext.export goal_ctxt lthy' (flat thss);
- val (simps', lthy'') = fold_map (LocalTheory.note Thm.theoremK)
+ val (simps', lthy'') = fold_map (LocalTheory.note Thm.generated_theoremK)
(names_atts' ~~ map single simps) lthy'
in
lthy''
- |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
+ |> LocalTheory.note Thm.generated_theoremK ((qualify (Binding.name "simps"),
map (Attrib.internal o K)
[Simplifier.simp_add, Nitpick_Const_Simp_Thms.add]),
maps snd simps')
--- a/src/HOL/String.thy Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/String.thy Mon May 18 09:47:34 2009 +0200
@@ -55,7 +55,7 @@
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
nibbles nibbles;
in
- PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
+ PureThy.note_thmss Thm.definitionK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
end
*}
--- a/src/HOL/Tools/function_package/fundef_package.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon May 18 09:47:34 2009 +0200
@@ -37,14 +37,15 @@
val simp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Code.add_default_eqn_attribute,
- Nitpick_Const_Simp_Thms.add]
+ Nitpick_Const_Simp_Thms.add,
+ Quickcheck_RecFun_Simp_Thms.add]
val psimp_attribs = map (Attrib.internal o K)
[Simplifier.simp_add,
Nitpick_Const_Psimp_Thms.add]
fun note_theorem ((name, atts), ths) =
- LocalTheory.note Thm.theoremK ((Binding.qualified_name name, atts), ths)
+ LocalTheory.note Thm.generated_theoremK ((Binding.qualified_name name, atts), ths)
fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
@@ -55,7 +56,7 @@
|> map (apfst (apfst extra_qualify))
val (saved_spec_simps, lthy) =
- fold_map (LocalTheory.note Thm.theoremK) spec lthy
+ fold_map (LocalTheory.note Thm.generated_theoremK) spec lthy
val saved_simps = flat (map snd saved_spec_simps)
val simps_by_f = sort saved_simps
--- a/src/HOL/Tools/inductive_package.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Tools/inductive_package.ML Mon May 18 09:47:34 2009 +0200
@@ -454,7 +454,7 @@
val facts = args |> map (fn ((a, atts), props) =>
((a, map (prep_att thy) atts),
map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
- in lthy |> LocalTheory.notes Thm.theoremK facts |>> map snd end;
+ in lthy |> LocalTheory.notes Thm.generated_theoremK facts |>> map snd end;
val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
@@ -849,7 +849,7 @@
|> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
val (cs, ps) = chop (length cnames_syn) vars;
val monos = Attrib.eval_thms lthy raw_monos;
- val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
+ val flags = {quiet_mode = false, verbose = verbose, kind = Thm.generated_theoremK,
alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false,
skip_mono = false, fork_mono = not int};
in
--- a/src/HOL/Tools/inductive_realizer.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon May 18 09:47:34 2009 +0200
@@ -349,7 +349,7 @@
val (ind_info, thy3') = thy2 |>
InductivePackage.add_inductive_global (serial_string ())
- {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
+ {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
rlzpreds rlzparams (map (fn (rintr, intr) =>
((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
--- a/src/HOL/Tools/primrec_package.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML Mon May 18 09:47:34 2009 +0200
@@ -247,14 +247,14 @@
val spec' = (map o apfst)
(fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
val simp_atts = map (Attrib.internal o K)
- [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
+ [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add];
in
lthy
|> set_group ? LocalTheory.set_group (serial_string ())
|> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
|-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
- |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
- |-> (fn simps' => LocalTheory.note Thm.theoremK
+ |-> (fn simps => fold_map (LocalTheory.note Thm.generated_theoremK) simps)
+ |-> (fn simps' => LocalTheory.note Thm.generated_theoremK
((qualify (Binding.qualified_name "simps"), simp_atts), maps snd simps'))
|>> snd
end handle PrimrecError (msg, some_eqn) =>
--- a/src/HOL/Tools/recdef_package.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/Tools/recdef_package.ML Mon May 18 09:47:34 2009 +0200
@@ -208,7 +208,7 @@
congs wfs name R eqs;
val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
- Code.add_default_eqn_attribute] else [];
+ Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
val ((simps' :: rules', [induct']), thy) =
thy
--- a/src/HOL/ex/predicate_compile.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Mon May 18 09:47:34 2009 +0200
@@ -18,8 +18,9 @@
val code_pred_cmd: string -> Proof.context -> Proof.state
val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*)
val do_proofs: bool ref
- val pred_intros: theory -> string -> thm list
- val get_nparams: theory -> string -> int
+ val pred_intros : theory -> string -> thm list
+ val get_nparams : theory -> string -> int
+ val pred_term_of : theory -> term -> term option
end;
structure Predicate_Compile : PREDICATE_COMPILE =
@@ -270,7 +271,7 @@
datatype hmode = Mode of mode * int list * hmode option list; (*FIXME don't understand
why there is another mode type!?*)
-fun modes_of modes t =
+fun modes_of_term modes t =
let
val ks = 1 upto length (binder_types (fastype_of t));
val default = [Mode (([], ks), ks, [])];
@@ -288,7 +289,7 @@
in map (fn x => Mode (m, is', x)) (cprods (map
(fn (NONE, _) => [NONE]
| (SOME js, arg) => map SOME (filter
- (fn Mode (_, js', _) => js=js') (modes_of modes arg)))
+ (fn Mode (_, js', _) => js=js') (modes_of_term modes arg)))
(iss ~~ args1)))
end
end)) (AList.lookup op = modes name)
@@ -317,13 +318,13 @@
term_vs t subset vs andalso
forall is_eqT dupTs
end)
- (modes_of modes t handle Option =>
+ (modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
| Negprem (us, t) => find_first (fn Mode (_, is, _) =>
length us = length is andalso
terms_vs us subset vs andalso
term_vs t subset vs)
- (modes_of modes t handle Option =>
+ (modes_of_term modes t handle Option =>
error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
| Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
else NONE
@@ -1392,7 +1393,7 @@
val (predname, _) = dest_Const pred
fun after_qed [[th]] lthy'' =
lthy''
- |> LocalTheory.note Thm.theoremK
+ |> LocalTheory.note Thm.generated_theoremK
((Binding.empty, [Attrib.internal (K add_elim_attrib)]), [th])
|> snd
|> LocalTheory.theory (prove_equation predname NONE)
@@ -1426,4 +1427,27 @@
- Naming of auxiliary rules necessary?
*)
+(* transformation for code generation *)
+
+fun pred_term_of thy t = let
+ val (vars, body) = strip_abs t
+ val (pred, all_args) = strip_comb body
+ val (name, T) = dest_Const pred
+ val (params, args) = chop (get_nparams thy name) all_args
+ val user_mode = flat (map_index
+ (fn (i, t) => case t of Bound j => if j < length vars then [] else [i+1] | _ => [i+1])
+ args)
+ val (inargs, _) = get_args user_mode args
+ val all_modes = Symtab.dest (#modes (IndCodegenData.get thy))
+ val modes = filter (fn Mode (_, is, _) => is = user_mode) (modes_of_term all_modes (list_comb (pred, params)))
+ fun compile m = list_comb (compile_expr thy all_modes (SOME m, list_comb (pred, params)), inargs)
+ in
+ case modes of
+ [] => (let val _ = error "No mode possible for this term" in NONE end)
+ | [m] => SOME (compile m)
+ | ms => (let val _ = warning "Multiple modes possible for this term"
+ in SOME (compile (hd ms)) end)
+ end;
+
end;
+
--- a/src/HOLCF/Tools/fixrec_package.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML Mon May 18 09:47:34 2009 +0200
@@ -195,7 +195,7 @@
val unfold_thms = unfolds names tuple_unfold_thm;
fun mk_note (n, thm) = ((Binding.name n, []), [thm]);
val (thmss, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.theoremK o mk_note)
+ |> fold_map (LocalTheory.note Thm.generated_theoremK o mk_note)
((all_names ^ "_induct", tuple_induct_thm) :: unfold_thms);
in
(lthy'', names, fixdef_thms, map snd unfold_thms)
@@ -373,7 +373,7 @@
val simps2 : (Attrib.binding * thm list) list =
map (apsnd (fn thm => [thm])) (List.concat simps);
val (_, lthy'') = lthy'
- |> fold_map (LocalTheory.note Thm.theoremK) (simps1 @ simps2);
+ |> fold_map (LocalTheory.note Thm.generated_theoremK) (simps1 @ simps2);
in
lthy''
end
--- a/src/Pure/Isar/attrib.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/Pure/Isar/attrib.ML Mon May 18 09:47:34 2009 +0200
@@ -123,7 +123,7 @@
fun attribute thy = attribute_i thy o intern_src thy;
-fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
+fun eval_thms ctxt args = ProofContext.note_thmss Thm.generated_theoremK
[(Thm.empty_binding, args |> map (fn (a, atts) =>
(ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
|> fst |> maps snd;
--- a/src/Pure/Thy/thm_deps.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML Mon May 18 09:47:34 2009 +0200
@@ -66,7 +66,7 @@
case Thm.get_group thm of
NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
- if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
+ if member (op =) [Thm.theoremK, Thm.generated_theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
andalso is_unused p
then
(case Thm.get_group thm of
--- a/src/Pure/more_thm.ML Sat May 16 20:18:29 2009 +0200
+++ b/src/Pure/more_thm.ML Mon May 18 09:47:34 2009 +0200
@@ -70,6 +70,7 @@
val assumptionK: string
val definitionK: string
val theoremK: string
+ val generated_theoremK : string
val lemmaK: string
val corollaryK: string
val internalK: string
@@ -388,6 +389,7 @@
val assumptionK = "assumption";
val definitionK = "definition";
val theoremK = "theorem";
+val generated_theoremK = "generated_theoremK"
val lemmaK = "lemma";
val corollaryK = "corollary";
val internalK = Markup.internalK;