--- a/src/HOL/Inductive.thy Tue May 09 10:09:17 2006 +0200
+++ b/src/HOL/Inductive.thy Tue May 09 10:09:37 2006 +0200
@@ -16,6 +16,7 @@
("Tools/datatype_rep_proofs.ML")
("Tools/datatype_abs_proofs.ML")
("Tools/datatype_realizer.ML")
+ ("Tools/datatype_hooks.ML")
("Tools/datatype_package.ML")
("Tools/datatype_codegen.ML")
("Tools/recfun_codegen.ML")
@@ -82,6 +83,10 @@
use "Tools/datatype_rep_proofs.ML"
use "Tools/datatype_abs_proofs.ML"
use "Tools/datatype_realizer.ML"
+
+use "Tools/datatype_hooks.ML"
+setup DatatypeHooks.setup
+
use "Tools/datatype_package.ML"
setup DatatypePackage.setup
--- a/src/HOL/Tools/datatype_codegen.ML Tue May 09 10:09:17 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Tue May 09 10:09:37 2006 +0200
@@ -9,9 +9,7 @@
sig
val get_datatype_spec_thms: theory -> string
-> (((string * sort) list * (string * typ list) list) * tactic) option
- val get_case_const_data: theory -> string -> (string * int) list option
val get_all_datatype_cons: theory -> (string * string) list
- val get_datatype_case_consts: theory -> string list
val setup: theory -> theory
end;
@@ -331,17 +329,13 @@
((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
(DatatypePackage.get_datatypes thy) [];
-fun get_case_const_data thy c =
- case find_first (fn (_, {index, descr, case_name, ...}) =>
- case_name = c
- ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
- of NONE => NONE
- | SOME (_, {index, descr, ...}) =>
- (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
-
-fun get_datatype_case_consts thy =
- Symtab.fold (fn (_, {case_name, ...}) => cons case_name)
- (DatatypePackage.get_datatypes thy) [];
+fun add_datatype_case_const dtco thy =
+ let
+ val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
+ in
+ CodegenPackage.add_case_const case_name
+ ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
+ end;
val setup =
add_codegen "datatype" datatype_codegen #>
@@ -352,8 +346,6 @@
DatatypePackage.get_datatype_spec #>
CodegenPackage.set_get_all_datatype_cons
get_all_datatype_cons #>
- CodegenPackage.ensure_datatype_case_consts
- get_datatype_case_consts
- get_case_const_data;
+ DatatypeHooks.add add_datatype_case_const
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/datatype_hooks.ML Tue May 09 10:09:37 2006 +0200
@@ -0,0 +1,55 @@
+(* Title: HOL/Tools/datatype_hooks.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Hooks for datatype introduction.
+*)
+
+signature DATATYPE_HOOKS =
+sig
+ type hook = string -> theory -> theory;
+ val add: hook -> theory -> theory;
+ val invoke: hook;
+ val setup: theory -> theory;
+end;
+
+structure DatatypeHooks : DATATYPE_HOOKS =
+struct
+
+
+(* theory data *)
+
+type hook = string -> theory -> theory;
+datatype T = T of (serial * hook) list;
+
+fun map_T f (T hooks) = T (f hooks);
+fun merge_T pp (T hooks1, T hooks2) =
+ T (AList.merge (op =) (K true) (hooks1, hooks2));
+
+structure DatatypeHooksData = TheoryDataFun
+(struct
+ val name = "HOL/DatatypeHooks";
+ type T = T;
+ val empty = T [];
+ val copy = I;
+ val extend = I;
+ val merge = merge_T;
+ fun print _ _ = ();
+end);
+
+
+(* interface *)
+
+fun add hook =
+ DatatypeHooksData.map (map_T (cons (serial (), hook)));
+
+fun invoke dtco thy =
+ fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
+
+
+(* theory setup *)
+
+val setup = DatatypeHooksData.init;
+
+end;
+
--- a/src/HOL/Tools/datatype_package.ML Tue May 09 10:09:17 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue May 09 10:09:37 2006 +0200
@@ -139,14 +139,6 @@
in SOME (map mk_co cos) end
| NONE => NONE;
-fun get_case_const_data thy c =
- case find_first (fn (_, {index, descr, case_name, ...}) =>
- case_name = c
- ) ((Symtab.dest o get_datatypes) thy)
- of NONE => NONE
- | SOME (_, {index, descr, ...}) =>
- (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
-
fun find_tname var Bi =
let val frees = map dest_Free (term_frees Bi)
val params = rename_wrt_term Bi (Logic.strip_params Bi);
@@ -717,9 +709,10 @@
|> put_datatypes (fold Symtab.update dt_infos dt_info)
|> add_cases_induct dt_infos induct
|> Theory.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
+ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
+ |> snd
|> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
- |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names';
+ |> fold (DatatypeHooks.invoke o fst) dt_infos;
in
({distinct = distinct,
inject = inject,
@@ -778,7 +771,7 @@
|> Theory.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
|> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
- |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names;
+ |> fold (DatatypeHooks.invoke o fst) dt_infos;
in
({distinct = distinct,
inject = inject,
@@ -876,15 +869,18 @@
val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
- val thy11 = thy10 |>
- Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
- add_rules simps case_thms size_thms rec_thms inject distinct
- weak_case_congs (Simplifier.attrib (op addcongs)) |>
- put_datatypes (fold Symtab.update dt_infos dt_info) |>
- add_cases_induct dt_infos induction' |>
- Theory.parent_path |>
- (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
- DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
+ val thy11 =
+ thy10
+ |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, [])
+ |> add_rules simps case_thms size_thms rec_thms inject distinct
+ weak_case_congs (Simplifier.attrib (op addcongs))
+ |> put_datatypes (fold Symtab.update dt_infos dt_info)
+ |> add_cases_induct dt_infos induction'
+ |> Theory.parent_path
+ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
+ |> snd
+ |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
+ |> fold (DatatypeHooks.invoke o fst) dt_infos;
in
({distinct = distinct,
inject = inject,