# HG changeset patch
# User berghofe
# Date 1164625795 -3600
# Node ID f3faed8276e62e778697feb4cb09aa246eb9c81f
# Parent  c5cf9243ad625ecc4179477471866cc192134388
Additional information about nominal datatypes (descriptor,
recursion equations etc.) is now stored in theory.

diff -r c5cf9243ad62 -r f3faed8276e6 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sun Nov 26 23:43:53 2006 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Nov 27 12:09:55 2006 +0100
@@ -9,6 +9,10 @@
 sig
   val add_nominal_datatype : bool -> string list -> (string list * bstring * mixfix *
     (bstring * string list * mixfix) list) list -> theory -> theory
+  type nominal_datatype_info
+  val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
+  val get_nominal_datatype : theory -> string -> nominal_datatype_info option
+  val setup: theory -> theory
 end
 
 structure NominalPackage : NOMINAL_PACKAGE =
@@ -47,6 +51,53 @@
 
 end;
 
+(* data kind 'HOL/nominal_datatypes' *)
+
+type nominal_datatype_info =
+  {index : int,
+   descr : descr,
+   sorts : (string * sort) list,
+   rec_names : string list,
+   rec_rewrites : thm list,
+   induction : thm,
+   distinct : thm list,
+   inject : thm list};
+
+structure NominalDatatypesData = TheoryDataFun
+(struct
+  val name = "HOL/nominal_datatypes";
+  type T = nominal_datatype_info Symtab.table;
+
+  val empty = Symtab.empty;
+  val copy = I;
+  val extend = I;
+  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+
+  fun print sg tab =
+    Pretty.writeln (Pretty.strs ("nominal datatypes:" ::
+      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
+end);
+
+val get_nominal_datatypes = NominalDatatypesData.get;
+val put_nominal_datatypes = NominalDatatypesData.put;
+val map_nominal_datatypes = NominalDatatypesData.map;
+val get_nominal_datatype = Symtab.lookup o get_nominal_datatypes;
+val setup = NominalDatatypesData.init;
+
+(**** make datatype info ****)
+
+fun make_dt_info descr sorts induct reccomb_names rec_thms
+    (((i, (_, (tname, _, _))), distinct), inject) =
+  (tname,
+   {index = i,
+    descr = descr,
+    sorts = sorts,
+    rec_names = reccomb_names,
+    rec_rewrites = rec_thms,
+    induction = induct,
+    distinct = distinct,
+    inject = inject});
+
 (*******************************)
 
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
@@ -1990,6 +2041,9 @@
       end) (rec_eq_prems ~~
         DatatypeProp.make_primrecs new_type_names descr' sorts' thy12);
 
+    val dt_infos = map (make_dt_info descr'' sorts induct reccomb_names rec_thms)
+      ((0 upto length descr1 - 1) ~~ descr1 ~~ distinct_thms ~~ inject_thms);
+
     (* FIXME: theorems are stored in database for testing only *)
     val (_, thy13) = thy12 |>
       PureThy.add_thmss
@@ -1999,7 +2053,8 @@
          (("rec_fresh", List.concat rec_fresh_thms), []),
          (("rec_unique", map standard rec_unique_thms), []),
          (("recs", rec_thms), [])] ||>
-      Theory.parent_path;
+      Theory.parent_path ||>
+      map_nominal_datatypes (fold Symtab.update dt_infos);
 
   in
     thy13