src/HOL/Tools/Datatype/datatype_codegen.ML

--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Nov 27 08:41:10 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Nov 27 08:42:34 2009 +0100
@@ -6,16 +6,19 @@
 
 signature DATATYPE_CODEGEN =
 sig
-  val find_shortest_path: Datatype.descr -> int -> (string * int) option
+  include DATATYPE_COMMON
+  val find_shortest_path: descr -> int -> (string * int) option
   val setup: theory -> theory
 end;
 
 structure DatatypeCodegen : DATATYPE_CODEGEN =
 struct
 
+open DatatypeAux
+
 (** find shortest path to constructor with no recursive arguments **)
 
-fun find_nonempty (descr: Datatype.descr) is i =
+fun find_nonempty (descr: descr) is i =
   let
     val (_, _, constrs) = the (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
@@ -40,7 +43,7 @@
 
 (* datatype definition *)
 
-fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
+fun add_dt_defs thy defs dep module (descr: descr) sorts gr =
   let
     val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
     val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
@@ -274,12 +277,12 @@
 
 fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
    (c as Const (s, T), ts) =>
-     (case Datatype.info_of_case thy s of
+     (case Datatype_Data.info_of_case thy s of
         SOME {index, descr, ...} =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           SOME (pretty_case thy defs dep module brack
             (#3 (the (AList.lookup op = descr index))) c ts gr )
-      | NONE => case (Datatype.info_of_constr thy (s, T), strip_type T) of
+      | NONE => case (Datatype_Data.info_of_constr thy (s, T), strip_type T) of
         (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
           if is_some (get_assoc_code thy (s, T)) then NONE else
           let
@@ -294,7 +297,7 @@
  | _ => NONE);
 
 fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
-      (case Datatype.get_info thy s of
+      (case Datatype_Data.get_info thy s of
          NONE => NONE
        | SOME {descr, sorts, ...} =>
            if is_some (get_assoc_type thy s) then NONE else
@@ -329,7 +332,7 @@
 fun mk_case_cert thy tyco =
   let
     val raw_thms =
-      (#case_rewrites o Datatype.the_info thy) tyco;
+      (#case_rewrites o Datatype_Data.the_info thy) tyco;
     val thms as hd_thm :: _ = raw_thms
       |> Conjunction.intr_balanced
       |> Thm.unvarify
@@ -362,9 +365,9 @@
 
 fun mk_eq_eqns thy dtco =
   let
-    val (vs, cos) = Datatype.the_spec thy dtco;
+    val (vs, cos) = Datatype_Data.the_spec thy dtco;
     val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
-      Datatype.the_info thy dtco;
+      Datatype_Data.the_info thy dtco;
     val ty = Type (dtco, map TFree vs);
     fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
       $ t1 $ t2;
@@ -424,11 +427,11 @@
 
 fun add_all_code config dtcos thy =
   let
-    val (vs :: _, coss) = (split_list o map (Datatype.the_spec thy)) dtcos;
+    val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
     val css = if exists is_none any_css then []
       else map_filter I any_css;
-    val case_rewrites = maps (#case_rewrites o Datatype.the_info thy) dtcos;
+    val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
     val certs = map (mk_case_cert thy) dtcos;
   in
     if null css then thy
@@ -446,6 +449,6 @@
 val setup = 
   add_codegen "datatype" datatype_codegen
   #> add_tycodegen "datatype" datatype_tycodegen
-  #> Datatype.interpretation add_all_code
+  #> Datatype_Data.interpretation add_all_code
 
 end;