simplified interpretations

--- a/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 15:09:19 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Nov 28 15:09:20 2007 +0100
@@ -15,11 +15,7 @@
 
   type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
     -> theory -> theory
-  val codetype_hook: hook
-  val eq_hook: hook
   val add_codetypes_hook: hook -> theory -> theory
-  val the_codetypes_mut_specs: theory -> (string * bool) list
-    -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
   val get_codetypes_arities: theory -> (string * bool) list -> sort
     -> (string * (arity * term list)) list
   val prove_codetypes_arities: tactic -> (string * bool) list -> sort
@@ -482,7 +478,7 @@
       (tyco, (is_dt, get_spec thy (tyco, is_dt)));
     fun datatype_hook dtcos thy =
       hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
-    fun typecopy_hook ((tyco, _)) thy =
+    fun typecopy_hook tyco thy =
       hook ([(tyco, (false, TypecopyPackage.get_spec thy tyco))]) thy;
   in
     thy
@@ -504,17 +500,6 @@
       in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
 
 
-(* registering code types in code generator *)
-
-fun add_datatype_spec (tyco, (vs, cos)) thy =
-  let
-    val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
-  in try (Code.add_datatype cs) thy |> the_default thy end;
-
-val codetype_hook =
-  fold (fn (dtco, (_ : bool, spec)) => add_datatype_spec (dtco, spec));
-
-
 (* instrumentalizing the sort algebra *)
 
 fun get_codetypes_arities thy tycos sort =
@@ -587,22 +572,28 @@
 
 (** theory setup **)
 
-fun add_datatype_case_defs dtco thy =
+fun add_datatype_spec dtco thy =
   let
-    val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco
-  in
-    fold_rev Code.add_default_func case_rewrites thy
-  end;
+    val SOME (vs, cos) = DatatypePackage.get_datatype_spec thy dtco;
+    val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+  in try (Code.add_datatype cs) thy |> the_default thy end;
 
 fun add_datatype_case_certs dtco thy =
   Code.add_case (get_case_cert thy dtco) thy;
 
+fun add_datatype_case_defs dtco thy =
+  let
+    val {case_rewrites, ...} = DatatypePackage.the_datatype thy dtco;
+  in
+    fold_rev Code.add_default_func case_rewrites thy
+  end;
+
 val setup = 
   add_codegen "datatype" datatype_codegen
   #> add_tycodegen "datatype" datatype_tycodegen
+  #> DatatypePackage.interpretation (fold add_datatype_spec)
   #> DatatypePackage.interpretation (fold add_datatype_case_certs)
   #> DatatypePackage.interpretation (fold add_datatype_case_defs)
-  #> add_codetypes_hook codetype_hook
   #> add_codetypes_hook eq_hook
 
 end;

--- a/src/HOL/Tools/typecopy_package.ML	Wed Nov 28 15:09:19 2007 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Wed Nov 28 15:09:20 2007 +0100
@@ -19,7 +19,7 @@
     -> theory -> (string * info) * theory
   val get_typecopies: theory -> string list
   val get_typecopy_info: theory -> string -> info option
-  val interpretation: (string * info -> theory -> theory) -> theory -> theory
+  val interpretation: (string -> theory -> theory) -> theory -> theory
   val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
   val get_eq: theory -> string -> thm
   val print_typecopies: theory -> unit
@@ -68,12 +68,10 @@
 val get_typecopy_info = Symtab.lookup o TypecopyData.get;
 
 
-(* interpretation *)
+(* interpretation of type copies *)
 
 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);
-
-fun interpretation interp = TypecopyInterpretation.interpretation
-  (fn tyco => fn thy => interp (tyco, (the o get_typecopy_info thy) tyco) thy);
+val interpretation = TypecopyInterpretation.interpretation;
 
 
 (* add a type copy *)
@@ -123,21 +121,30 @@
 end;
 
 
-(* equality function equation and datatype specification *)
-
-fun get_eq thy tyco =
-  (#inject o the o get_typecopy_info thy) tyco;
+(* code generator setup *)
 
 fun get_spec thy tyco =
   let
     val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
   in (vs, [(constr, [typ])]) end;
 
-
-(* interpretation for projection function code *)
+fun get_eq thy tyco =
+  (#inject o the o get_typecopy_info thy) tyco;
 
-fun add_project (_, {proj_def, ...} : info) = Code.add_default_func proj_def;
+fun add_typecopy_spec tyco thy =
+  let
+    val c = (#constr o the o get_typecopy_info thy) tyco;
+    val ty = Logic.unvarifyT (Sign.the_const_type thy c);
+  in
+    thy |> Code.add_datatype [(c, ty)]
+  end;
 
-val setup = TypecopyInterpretation.init #> interpretation add_project;
+fun add_project tyco thy = thy |> Code.add_default_func
+  ((#proj_def o the o get_typecopy_info thy) tyco);
+
+val setup =
+  TypecopyInterpretation.init
+  #> interpretation add_typecopy_spec
+  #> interpretation add_project
 
 end;