added codegenerator

--- a/src/HOL/Integ/IntDef.thy	Tue Nov 22 12:42:59 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Nov 22 12:59:25 2005 +0100
@@ -897,6 +897,10 @@
   "neg"                         ("(_ < 0)")
 
 ML {*
+fun mk_int_to_nat bin =
+  Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
+  $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
+
 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
       Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
         (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
@@ -909,7 +913,11 @@
   | number_of_codegen _ _ _ _ _ _ _ = NONE;
 *}
 
-setup {* [Codegen.add_codegen "number_of_codegen" number_of_codegen] *}
+setup {*[
+  Codegen.add_codegen "number_of_codegen" number_of_codegen,
+  CodegenPackage.add_codegen_expr
+    ("number", CodegenPackage.codegen_number_of HOLogic.dest_binum mk_int_to_nat)
+]*}
 
 quickcheck_params [default_type = int]
 

--- a/src/HOL/Product_Type.thy	Tue Nov 22 12:42:59 2005 +0100
+++ b/src/HOL/Product_Type.thy	Tue Nov 22 12:59:25 2005 +0100
@@ -865,9 +865,14 @@
 
 in
 
-val prod_codegen_setup =
-  [Codegen.add_codegen "let_codegen" let_codegen,
-   Codegen.add_codegen "split_codegen" split_codegen];
+val prod_codegen_setup = [
+  Codegen.add_codegen "let_codegen" let_codegen,
+  Codegen.add_codegen "split_codegen" split_codegen,
+  CodegenPackage.add_codegen_expr
+    ("let", CodegenPackage.codegen_let strip_abs),
+  CodegenPackage.add_codegen_expr
+    ("split", CodegenPackage.codegen_split strip_abs)
+];
 
 end;
 *}

--- a/src/HOL/Tools/datatype_codegen.ML	Tue Nov 22 12:42:59 2005 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Nov 22 12:59:25 2005 +0100
@@ -7,6 +7,9 @@
 
 signature DATATYPE_CODEGEN =
 sig
+  val is_datatype: theory -> string -> bool
+  val get_datatype: theory -> string -> (string list * string list) option
+  val get_datacons: theory -> string * string -> typ list option
   val setup: (theory -> theory) list
 end;
 
@@ -296,9 +299,58 @@
            end)
   | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
 
+fun is_datatype thy dtyco =
+  Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
+  |> is_some;
 
-val setup =
-  [add_codegen "datatype" datatype_codegen,
-   add_tycodegen "datatype" datatype_tycodegen];
+fun get_datatype thy dtname =
+  case CodegenPackage.tname_of_idf thy dtname
+   of SOME dtname =>
+        dtname
+        |> Symtab.lookup (DatatypePackage.get_datatypes thy)
+        |> Option.map #descr
+        |> these
+        |> get_first (fn (_, (dtname', vs, cs)) =>
+             if dtname = dtname'
+             then SOME (vs, map fst cs)
+             else NONE)
+        |> Option.mapPartial (try (apfst (map DatatypeAux.dest_DtTFree)))
+    | _ => NONE;
+
+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;
+
+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),
+  CodegenPackage.add_defgen
+    ("datacons", CodegenPackage.defgen_datacons get_datacons)
+];
 
 end;

--- a/src/HOL/Tools/recfun_codegen.ML	Tue Nov 22 12:42:59 2005 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Nov 22 12:59:25 2005 +0100
@@ -9,6 +9,7 @@
 sig
   val add: string option -> theory attribute
   val del: theory attribute
+  val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
   val setup: (theory -> theory) list
 end;
 
@@ -79,6 +80,19 @@
              | SOME thyname => thyname)
        end);
 
+fun get_rec_equations thy (s, T) =
+  Symtab.lookup (CodegenData.get thy) s
+  |> Option.map (fn thms => 
+       List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms
+       |> del_redundant thy [])
+  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
+  |> Option.map (fn thms =>
+       (preprocess thy (map fst thms),
+          (snd o const_of o prop_of o fst o hd) thms))
+  |> the_default ([], dummyT)
+  |> apfst (map prop_of)
+  |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
+
 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
   SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
 
@@ -165,11 +179,14 @@
   | _ => NONE);
 
 
-val setup =
-  [CodegenData.init,
-   add_codegen "recfun" recfun_codegen,
-   add_attribute ""
-     (   Args.del |-- Scan.succeed del
-      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
+val setup = [
+  CodegenData.init,
+  add_codegen "recfun" recfun_codegen,
+  add_attribute ""
+    (   Args.del |-- Scan.succeed del
+     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
+  CodegenPackage.add_defgen
+    ("rec", CodegenPackage.defgen_recfun get_rec_equations)
+];
 
 end;