Recursive equations to be used for code generation are now registered
via RecfunCodegen.add
--- a/src/HOL/Tools/datatype_package.ML Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML Mon Dec 10 15:34:15 2001 +0100
@@ -290,6 +290,7 @@
(#1 o PureThy.add_thmss [(("simps", simps), []),
(("", flat case_thms @ size_thms @
flat distinct @ rec_thms), [Simplifier.simp_add_global]),
+ (("", size_thms @ rec_thms), [RecfunCodegen.add]),
(("", flat inject), [iff_add_global]),
(("", flat distinct RL [notE]), [Classical.safe_elim_global]),
(("", weak_case_congs), [cong_att])]);
--- a/src/HOL/Tools/primrec_package.ML Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/primrec_package.ML Mon Dec 10 15:34:15 2001 +0100
@@ -9,13 +9,10 @@
signature PRIMREC_PACKAGE =
sig
val quiet_mode: bool ref
- val print_primrecs: theory -> unit
- val get_primrec: theory -> string -> (string * thm list) list option
val add_primrec: string -> ((bstring * string) * Args.src list) list
-> theory -> theory * thm list
val add_primrec_i: string -> ((bstring * term) * theory attribute list) list
-> theory -> theory * thm list
- val setup: (theory -> theory) list
end;
structure PrimrecPackage : PRIMREC_PACKAGE =
@@ -36,41 +33,6 @@
fun message s = if ! quiet_mode then () else writeln s;
-(** theory data **)
-
-(* data kind 'HOL/primrec' *)
-
-structure PrimrecArgs =
-struct
- val name = "HOL/primrec";
- type T = (string * thm list) list Symtab.table;
-
- val empty = Symtab.empty;
- val copy = I;
- val prep_ext = I;
- val merge: T * T -> T = Symtab.merge (K true);
-
- fun print sg tab =
- Pretty.writeln (Pretty.strs ("primrecs:" ::
- map #1 (Sign.cond_extern_table sg Sign.constK tab)));
-end;
-
-structure PrimrecData = TheoryDataFun(PrimrecArgs);
-val print_primrecs = PrimrecData.print;
-
-
-(* get and put data *)
-
-fun get_primrec thy name = Symtab.lookup (PrimrecData.get thy, name);
-
-fun put_primrec name info thy =
- let val tab = PrimrecData.get thy
- in
- PrimrecData.put (case Symtab.lookup (tab, name) of
- None => Symtab.update_new ((name, [info]), tab)
- | Some infos => Symtab.update ((name, info::infos), tab)) thy end;
-
-
(* preprocessing of equations *)
fun process_eqn sign (eq, rec_fns) =
@@ -305,12 +267,11 @@
(fn _ => [rtac refl 1])) eqns;
val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy';
val thy''' = thy''
- |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global])])
+ |> (#1 o PureThy.add_thmss [(("simps", simps'), [Simplifier.simp_add_global, RecfunCodegen.add])])
|> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])])
|> Theory.parent_path
in
- (foldl (fn (thy, (fname, _, _, tname)) =>
- put_primrec fname (tname, simps) thy) (thy''', defs), simps')
+ (thy''', simps')
end;
@@ -328,10 +289,6 @@
end;
-(** package setup **)
-
-val setup = [PrimrecData.init];
-
(* outer syntax *)
local structure P = OuterParse and K = OuterSyntax.Keyword in
--- a/src/HOL/Tools/recdef_package.ML Mon Dec 10 15:32:10 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML Mon Dec 10 15:34:15 2001 +0100
@@ -242,7 +242,8 @@
val (cs, ss, congs, wfs) = prep_hints thy hints;
val (thy, {rules = rules_idx, induct, tcs}) = tfl_fn strict thy cs ss congs wfs name R eqs;
val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
- val simp_att = if null tcs then [Simplifier.simp_add_global] else [];
+ val simp_att = if null tcs then
+ [Simplifier.simp_add_global, RecfunCodegen.add] else [];
val case_numbers = map Library.string_of_int (1 upto Thm.nprems_of induct);
val (thy, (simps' :: rules', [induct'])) =