src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 00:34:54 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 17:00:22 2006 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/datatype_codegen.ML
     ID:         $Id$
-    Author:     Stefan Berghofer, TU Muenchen
+    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
 
 Code generator for inductive datatypes.
 *)
@@ -10,6 +10,8 @@
   val get_datatype_spec_thms: theory -> string
     -> (((string * sort) list * (string * typ list) list) * tactic) option
   val get_all_datatype_cons: theory -> (string * string) list
+  val dest_case_expr: theory -> term
+    -> ((string * typ) list * ((term * typ) * (term * term) list)) option;
   val add_datatype_case_const: string -> theory -> theory
   val add_datatype_case_defs: string -> theory -> theory
   val setup: theory -> theory
@@ -304,6 +306,34 @@
 
 (** code 2nd generation **)
 
+fun dtyp_of_case_const thy c =
+  get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
+    ((Symtab.dest o DatatypePackage.get_datatypes) thy);
+
+fun dest_case_app cs ts tys =
+  let
+    val abs = CodegenThingol.give_names [] (Library.drop (length ts, tys));
+    val (ts', t) = split_last (ts @ map Free abs);
+    val (tys', sty) = split_last tys;
+    fun freenames_of t = fold_aterms
+      (fn Free (v, _) => insert (op =) v | _ => I) t [];
+    fun dest_case ((c, tys_decl), ty) t =
+      let
+        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
+        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
+      in (c', t') end;
+  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
+
+fun dest_case_expr thy t =
+  case strip_comb t
+   of (Const (c, ty), ts) =>
+        (case dtyp_of_case_const thy c
+         of SOME dtco =>
+              let val (vs, cs) = (the o DatatypePackage.get_datatype_spec thy) dtco;
+              in SOME (dest_case_app cs ts (Library.take (length cs + 1, (fst o strip_type) ty))) end
+          | _ => NONE)
+    | _ => NONE;
+
 fun datatype_tac thy dtco =
   let
     val ctxt = Context.init_proof thy;
@@ -333,10 +363,9 @@
 
 fun add_datatype_case_const dtco thy =
   let
-    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
+    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
+    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
   end;
 
 fun add_datatype_case_defs dtco thy =
@@ -351,8 +380,6 @@
   add_tycodegen "datatype" datatype_tycodegen #>
   CodegenTheorems.add_datatype_extr
     get_datatype_spec_thms #>
-  CodegenPackage.set_get_datatype
-    DatatypePackage.get_datatype_spec #>
   CodegenPackage.set_get_all_datatype_cons
     get_all_datatype_cons #>
   DatatypeHooks.add add_datatype_case_const #>