# HG changeset patch
# User haftmann
# Date 1135174697 -3600
# Node ID 5ff0244e25e81f6caff4dca40b8ec4605b4ae769
# Parent  e57731ba01dd75c6b246717da9b71fd334ce007d
slight clean ups

diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 21 13:25:20 2005 +0100
+++ b/src/HOL/List.thy	Wed Dec 21 15:18:17 2005 +0100
@@ -2692,4 +2692,6 @@
 
 setup list_codegen_setup
 
+setup "[CodegenPackage.rename_inconsistent]"
+
 end
diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 13:25:20 2005 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 15:18:17 2005 +0100
@@ -7,10 +7,6 @@
 
 signature DATATYPE_CODEGEN =
 sig
-  val is_datatype: theory -> string -> bool
-  val get_datatype: theory -> string -> ((string * sort) list * string list) option
-  val get_datacons: theory -> string * string -> typ list option
-  val get_case_const_data: theory -> string -> (string * int) list option;
   val setup: (theory -> theory) list
 end;
 
@@ -300,64 +296,20 @@
            end)
   | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
 
-fun is_datatype thy dtyco =
-  Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
-  |> is_some;
-
-fun get_datatype thy dtname =
-  dtname
-  |> Symtab.lookup (DatatypePackage.get_datatypes thy)
-  |> Option.map (fn info => (#sorts info,
-      (get_first (fn (_, (dtname', _, cs)) =>
-        if dtname = dtname'
-        then SOME (map fst cs)
-        else NONE) (#descr info) |> the)));
-  
-fun get_datacons thy (c, dtname) =
-  let
-    val descr =
-      dtname
-      |> Symtab.lookup (DatatypePackage.get_datatypes thy)
-      |> Option.map #descr
-      |> these
-    val one_descr =
-      descr
-      |> get_first (fn (_, (dtname', vs, cs)) =>
-          if dtname = dtname'
-          then SOME (vs, cs)
-          else NONE);
-  in
-    if is_some one_descr
-    then
-      the one_descr
-      |> (fn (vs, cs) =>
-          c
-          |> AList.lookup (op =) cs
-          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
-               (map DatatypeAux.dest_DtTFree vs)))))
-    else NONE
-  end;
-
-fun get_case_const_data thy f =
-  case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
-      case_name = f
-    ) ((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;
-
 
 val setup = [
   add_codegen "datatype" datatype_codegen,
   add_tycodegen "datatype" datatype_tycodegen,
   CodegenPackage.set_is_datatype
-    is_datatype,
-  CodegenPackage.add_defgen
-    ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
+    DatatypePackage.is_datatype,
+  CodegenPackage.set_get_all_datatype_cons
+    DatatypePackage.get_all_datatype_cons,
   CodegenPackage.add_defgen
-    ("datacons", CodegenPackage.defgen_datacons get_datacons),
+    ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
+  CodegenPackage.add_defgen
+    ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons),
   CodegenPackage.add_appgen
-    ("case", CodegenPackage.appgen_case get_case_const_data)
+    ("case", CodegenPackage.appgen_case DatatypePackage.get_case_const_data)
 ];
 
 end;
diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Dec 21 13:25:20 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 21 15:18:17 2005 +0100
@@ -66,6 +66,11 @@
   val print_datatypes : theory -> unit
   val datatype_info : theory -> string -> DatatypeAux.datatype_info option
   val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
+  val is_datatype : theory -> string -> bool
+  val get_datatype : theory -> string -> ((string * sort) list * string list) option
+  val get_datatype_cons : theory -> string * string -> typ list option
+  val get_case_const_data : theory -> string -> (string * int) list option
+  val get_all_datatype_cons : theory -> (string * string list) list
   val constrs_of : theory -> string -> term list option
   val case_const_of : theory -> string -> term option
   val weak_case_congs_of : theory -> thm list
@@ -948,6 +953,61 @@
 val add_datatype = gen_add_datatype read_typ true;
 
 
+(** queries **)
+
+fun is_datatype thy dtco =
+  Symtab.lookup (get_datatypes thy) dtco
+  |> is_some;
+
+fun get_datatype thy dtco =
+  dtco
+  |> Symtab.lookup (get_datatypes thy)
+  |> Option.map (fn info => (#sorts info,
+      (get_first (fn (_, (dtco', _, cs)) =>
+        if dtco = dtco'
+        then SOME (map fst cs)
+        else NONE) (#descr info) |> the)));
+  
+fun get_datatype_cons thy (co, dtco) =
+  let
+    val descr =
+      dtco
+      |> Symtab.lookup (get_datatypes thy)
+      |> Option.map #descr
+      |> these
+    val one_descr =
+      descr
+      |> get_first (fn (_, (dtco', vs, cs)) =>
+          if dtco = dtco'
+          then SOME (vs, cs)
+          else NONE);
+  in
+    if is_some one_descr
+    then
+      the one_descr
+      |> (fn (vs, cs) =>
+          co
+          |> AList.lookup (op =) cs
+          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
+               (map DatatypeAux.dest_DtTFree vs)))))
+    else NONE
+  end;
+
+fun get_case_const_data thy c =
+  case Library.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 get_all_datatype_cons thy =
+  Symtab.fold (fn (dtco, _) => fold
+    (fn co =>
+      AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco))
+    ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
+
+
 (** package setup **)
 
 (* setup theory *)