# HG changeset patch # User haftmann # Date 1190093775 -7200 # Node ID b8383b1bbae39cd73725d67bf7ef7f241bdcd400 # Parent 7b2bc73405b87888c8e7949c63be220552ea2ac6 distinction between regular and default code theorems diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Sep 18 07:36:15 2007 +0200 @@ -629,7 +629,7 @@ let val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco in - fold_rev (Code.add_func true) case_rewrites thy + fold_rev Code.add_default_func case_rewrites thy end; val setup = diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/datatype_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -329,7 +329,7 @@ PureThy.add_thmss [(("simps", simps), []), (("", flat case_thms @ size_thms @ flat distinct @ rec_thms), [Simplifier.simp_add]), - (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]), + (("", size_thms @ rec_thms), [RecfunCodegen.add_default]), (("", flat inject), [iff_add]), (("", map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), (("", weak_case_congs), [cong_att])] diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -131,7 +131,7 @@ val tinduct = map remove_domain_condition pinducts val has_guards = exists ((fn (Const ("Trueprop", _) $ _) => false | _ => true) o prop_of) tsimps - val allatts = if has_guards then [] else [Attrib.internal (K (RecfunCodegen.add NONE))] + val allatts = if has_guards then [] else [Attrib.internal (K RecfunCodegen.add_default)] val qualify = NameSpace.qualified defname; in diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/primrec_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -298,7 +298,7 @@ val simps'' = maps snd simps'; in thy'' - |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add NONE]), simps'') + |> note (("simps", [Simplifier.simp_add, RecfunCodegen.add_default]), simps'') |> snd |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns]) |> snd diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/recdef_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -211,7 +211,7 @@ tfl_fn not_permissive thy cs (ss delcongs [imp_cong]) 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, RecfunCodegen.add NONE] else []; + val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add_default] else []; val ((simps' :: rules', [induct']), thy) = thy diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Sep 18 07:36:15 2007 +0200 @@ -8,6 +8,7 @@ signature RECFUN_CODEGEN = sig val add: string option -> attribute + val add_default: attribute val del: attribute val setup: theory -> theory end; @@ -26,7 +27,6 @@ fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst); ); - val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; val lhs_of = fst o dest_eqn o prop_of; val const_of = dest_Const o head_of o fst o dest_eqn; @@ -34,28 +34,23 @@ fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^ string_of_thm thm); -fun add optmod = - let - fun add thm = - if Pattern.pattern (lhs_of thm) then - RecCodegenData.map - (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, optmod))) - else tap (fn _ => warn thm) - handle TERM _ => tap (fn _ => warn thm); - in - Thm.declaration_attribute (fn thm => Context.mapping - (add thm #> Code.add_func false thm) I) - end; +fun add_thm opt_module thm = + if Pattern.pattern (lhs_of thm) then + RecCodegenData.map + (Symtab.update_list ((fst o const_of o prop_of) thm, (thm, opt_module))) + else tap (fn _ => warn thm) + handle TERM _ => tap (fn _ => warn thm); -fun del_thm thm thy = - let - val tab = RecCodegenData.get thy; - val (s, _) = const_of (prop_of thm); - in case Symtab.lookup tab s of - NONE => thy - | SOME thms => - RecCodegenData.put (Symtab.update (s, remove (Thm.eq_thm o apsnd fst) thm thms) tab) thy - end handle TERM _ => (warn thm; thy); +fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping + (add_thm opt_module thm #> Code.add_liberal_func thm) I); + +val add_default = Thm.declaration_attribute (fn thm => Context.mapping + (add_thm NONE thm #> Code.add_default_func thm) I); + +fun del_thm thm = case try const_of (prop_of thm) + of SOME (s, _) => RecCodegenData.map + (Symtab.map_entry s (remove (Thm.eq_thm o apsnd fst) thm)) + | NONE => tap (fn _ => warn thm); val del = Thm.declaration_attribute (fn thm => Context.mapping (del_thm thm #> Code.del_func thm) I) diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -1512,8 +1512,8 @@ ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs)) ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs) |-> (fn args as ((_, dest_defs), upd_defs) => - fold (Code.add_func false) dest_defs - #> fold (Code.add_func false) upd_defs + fold Code.add_default_func dest_defs + #> fold Code.add_default_func upd_defs #> pair args); val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) = timeit_msg "record extension type/selector/update defs:" mk_defs; @@ -1916,9 +1916,9 @@ ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) [make_spec, fields_spec, extend_spec, truncate_spec]) |-> (fn defs as ((sel_defs, upd_defs), derived_defs) => - fold (Code.add_func false) sel_defs - #> fold (Code.add_func false) upd_defs - #> fold (Code.add_func false) derived_defs + fold Code.add_default_func sel_defs + #> fold Code.add_default_func upd_defs + #> fold Code.add_default_func derived_defs #> pair defs) val (((sel_defs, upd_defs), derived_defs), defs_thy) = timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:" diff -r 7b2bc73405b8 -r b8383b1bbae3 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/HOL/Tools/typecopy_package.ML Tue Sep 18 07:36:15 2007 +0200 @@ -141,7 +141,7 @@ (* hook for projection function code *) -fun add_project (_ , {proj_def, ...} : info) = Code.add_func true proj_def; +fun add_project (_ , {proj_def, ...} : info) = Code.add_default_func proj_def; val setup = add_hook add_project; diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Isar/code.ML Tue Sep 18 07:36:15 2007 +0200 @@ -8,10 +8,12 @@ signature CODE = sig - val add_func: bool -> thm -> theory -> theory + val add_func: thm -> theory -> theory + val add_liberal_func: thm -> theory -> theory + val add_default_func: thm -> theory -> theory + val add_default_func_attr: Attrib.src val del_func: thm -> theory -> theory val add_funcl: string * thm list Susp.T -> theory -> theory - val add_func_attr: bool -> Attrib.src val add_inline: thm -> theory -> theory val del_inline: thm -> theory -> theory val add_inline_proc: string * (theory -> cterm list -> thm list) -> theory -> theory @@ -635,7 +637,8 @@ in check_typ (const_of_func thy thm, thm) end; val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func); -val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func); +val mk_liberal_func = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func); +val mk_default_func = CodeUnit.try_thm (assert_func_typ o CodeUnit.mk_func); end; @@ -643,6 +646,10 @@ (** interfaces and attributes **) +fun delete_force msg key xs = + if AList.defined (op =) xs key then AList.delete (op =) key xs + else error ("No such " ^ msg ^ ": " ^ quote key); + fun get_datatype thy tyco = case Symtab.lookup ((the_dtyps o get_exec) thy) tyco of SOME spec => spec @@ -667,38 +674,48 @@ in SOME (Logic.varifyT ty) end | NONE => NONE; -fun add_func true thm thy = - let - val func = mk_func thm; - val c = const_of_func thy func; - val _ = if (is_some o AxClass.class_of_param thy) c - then error ("Rejected polymorphic equation for overloaded constant:\n" - ^ string_of_thm thm) - else (); - val _ = if (is_some o get_datatype_of_constr thy) c - then error ("Rejected equation for datatype constructor:\n" - ^ string_of_thm func) - else (); - in - (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default - (c, (Susp.value [], [])) (add_thm func)) thy - end - | add_func false thm thy = - case mk_func_liberal thm - of SOME func => let - val c = const_of_func thy func - in if (is_some o AxClass.class_of_param thy) c - orelse (is_some o get_datatype_of_constr thy) c - then thy - else map_exec_purge (SOME [c]) (map_funcs - (Symtab.map_default - (c, (Susp.value [], [])) (add_thm func))) thy - end - | NONE => thy; +fun add_func thm thy = + let + val func = mk_func thm; + val c = const_of_func thy func; + val _ = if (is_some o AxClass.class_of_param thy) c + then error ("Rejected polymorphic equation for overloaded constant:\n" + ^ string_of_thm thm) + else (); + val _ = if (is_some o get_datatype_of_constr thy) c + then error ("Rejected equation for datatype constructor:\n" + ^ string_of_thm func) + else (); + in + (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default + (c, (Susp.value [], [])) (add_thm func)) thy + end; -fun delete_force msg key xs = - if AList.defined (op =) xs key then AList.delete (op =) key xs - else error ("No such " ^ msg ^ ": " ^ quote key); +fun add_liberal_func thm thy = + case mk_liberal_func thm + of SOME func => let + val c = const_of_func thy func + in if (is_some o AxClass.class_of_param thy) c + orelse (is_some o get_datatype_of_constr thy) c + then thy + else map_exec_purge (SOME [c]) (map_funcs + (Symtab.map_default + (c, (Susp.value [], [])) (add_thm func))) thy + end + | NONE => thy; + +fun add_default_func thm thy = + case mk_default_func thm + of SOME func => let + val c = const_of_func thy func + in if (is_some o AxClass.class_of_param thy) c + orelse (is_some o get_datatype_of_constr thy) c + then thy + else map_exec_purge (SOME [c]) (map_funcs + (Symtab.map_default + (c, (Susp.value [], [])) (add_thm func))) thy + end + | NONE => thy; fun del_func thm thy = let @@ -719,8 +736,8 @@ (add_lthms lthms'))) thy end; -fun add_func_attr strict = Attrib.internal (fn _ => Thm.declaration_attribute - (fn thm => Context.mapping (add_func strict thm) I)); +val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute + (fn thm => Context.mapping (add_default_func thm) I)); fun add_datatype raw_cs thy = let @@ -786,7 +803,7 @@ add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) || Scan.succeed (mk_attribute add)) in - add_del_attribute ("func", (add_func true, del_func)) + add_del_attribute ("func", (add_func, del_func)) #> add_del_attribute ("inline", (add_inline, del_inline)) #> add_del_attribute ("post", (add_post, del_post)) end); diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Isar/code_unit.ML Tue Sep 18 07:36:15 2007 +0200 @@ -27,6 +27,7 @@ val bad_thm: string -> 'a val error_thm: (thm -> thm) -> thm -> thm val warning_thm: (thm -> thm) -> thm -> thm option + val try_thm: (thm -> thm) -> thm -> thm option val inst_thm: sort Vartab.table -> thm -> thm val expand_eta: int -> thm -> thm @@ -46,6 +47,7 @@ fun error_thm f thm = f thm handle BAD_THM msg => error msg; fun warning_thm f thm = SOME (f thm) handle BAD_THM msg => (warning ("code generator: " ^ msg); NONE); +fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); fun string_of_const thy c = case Class.param_const thy c diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Isar/constdefs.ML Tue Sep 18 07:36:15 2007 +0200 @@ -51,7 +51,7 @@ thy |> Sign.add_consts_i [(c, T, mx)] |> PureThy.add_defs_i false [((name, def), atts)] - |-> (fn [thm] => Code.add_func false thm); + |-> (fn [thm] => Code.add_default_func thm); in ((c, T), thy') end; fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Sep 18 07:36:15 2007 +0200 @@ -431,7 +431,7 @@ || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> Class.interpretation_in_class_cmd || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) - >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false))) + >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); val instantiationP = diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Isar/specification.ML Tue Sep 18 07:36:15 2007 +0200 @@ -131,7 +131,7 @@ |> LocalTheory.def Thm.definitionK ((x, mx), ((name ^ "_raw", []), rhs)); val ((b, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK - ((name, Code.add_func_attr false :: atts), [prove lthy2 th]); + ((name, Code.add_default_func_attr :: atts), [prove lthy2 th]); val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs; val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)]; diff -r 7b2bc73405b8 -r b8383b1bbae3 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Tue Sep 18 07:36:14 2007 +0200 +++ b/src/Pure/Proof/extraction.ML Tue Sep 18 07:36:15 2007 +0200 @@ -741,7 +741,7 @@ (ProofChecker.thm_of_proof thy' (fst (Proofterm.freeze_thaw_prf prf)))))), []) |> snd - |> fold (Code.add_func false) def_thms + |> fold Code.add_default_func def_thms end | SOME _ => thy);