# HG changeset patch # User haftmann # Date 1242632854 -7200 # Node ID 7d43c7d3a15cd41e98bf17532d21db47c13bfa55 # Parent e5d01f8a916db1c71b905407a7409dd22bee0749# Parent 92e0ed53db251e2fb27d8e1dcd4525e73e572d66 merged diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/HOL.thy --- 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) *} diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Nominal/nominal_inductive.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Nominal/nominal_inductive2.ML --- 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))]), diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Nominal/nominal_primrec.ML --- 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') diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/String.thy --- 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 *} diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Tools/inductive_package.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Tools/inductive_realizer.ML --- 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)), []), diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Tools/primrec_package.ML --- 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) => diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/Tools/recdef_package.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOL/ex/predicate_compile.ML --- 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; + diff -r e5d01f8a916d -r 7d43c7d3a15c src/HOLCF/Tools/fixrec_package.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/Pure/Isar/attrib.ML --- 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; diff -r e5d01f8a916d -r 7d43c7d3a15c src/Pure/Thy/thm_deps.ML --- 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 diff -r e5d01f8a916d -r 7d43c7d3a15c src/Pure/more_thm.ML --- 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;