--- 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 =
--- 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])]
--- 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
--- 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
--- 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
--- 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)
--- 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:"
--- 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;
--- 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);
--- 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
--- 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 =
--- 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.$$$ "\\<subseteq>" || 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 =
--- 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)];
--- 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);