# HG changeset patch
# User haftmann
# Date 1147162177 -7200
# Node ID a5c7eb37d14f18a094b5d0b9a381eb2b5f9341db
# Parent  d68dd20af31fe7726ecb2532900e4ca0b87f7cfa
added DatatypeHooks

diff -r d68dd20af31f -r a5c7eb37d14f src/HOL/Inductive.thy
--- 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
 
diff -r d68dd20af31f -r a5c7eb37d14f src/HOL/Tools/datatype_codegen.ML
--- 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;
diff -r d68dd20af31f -r a5c7eb37d14f src/HOL/Tools/datatype_hooks.ML
--- /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;
+
diff -r d68dd20af31f -r a5c7eb37d14f src/HOL/Tools/datatype_package.ML
--- 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,