# HG changeset patch
# User haftmann
# Date 1150279957 -7200
# Node ID e3a03f1f54eb12e8f4d21d9df95345bac0aa5e43
# Parent  6bec6daac280d0e33599037af1c7c8a5767da624
slight refinements for code generator

diff -r 6bec6daac280 -r e3a03f1f54eb src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Jun 14 12:12:01 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Wed Jun 14 12:12:37 2006 +0200
@@ -902,14 +902,11 @@
   "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                              ("(_ < 0)")
 
-code_syntax_tyco int
+code_typapp int
   ml (target_atom "IntInf.int")
   haskell (target_atom "Integer")
 
-code_syntax_const
-  "0 :: int"
-    ml (target_atom "(0:IntInf.int)")
-    haskell (target_atom "0")
+code_constapp
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
     ml (infixl 8 "+")
     haskell (infixl 6 "+")
@@ -938,6 +935,15 @@
   handle TERM _
     => error ("not a number: " ^ Sign.string_of_term thy bin);
 
+fun appgen_number thy tabs (app as ((_, ty), _)) =
+  let
+    val _ = case strip_type ty
+     of (_, Type (ty', [])) => if ty' = "IntDef.int" then ()
+       else error ("not integer type: " ^ quote ty');
+  in
+    CodegenPackage.appgen_number_of bin_to_int thy tabs app
+  end;
+
 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)),
@@ -955,7 +961,7 @@
   Codegen.add_codegen "number_of_codegen" number_of_codegen
   #> CodegenPackage.add_appconst
        ("Numeral.number_of", ((1, 1),
-          CodegenPackage.appgen_number_of bin_to_int))
+          appgen_number))
   #> CodegenPackage.set_int_tyco "IntDef.int"
 *}
 
diff -r 6bec6daac280 -r e3a03f1f54eb src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jun 14 12:12:01 2006 +0200
+++ b/src/HOL/Integ/NatBin.thy	Wed Jun 14 12:12:37 2006 +0200
@@ -781,13 +781,6 @@
 
 subsection {* code generator setup *}
 
-lemma number_of_eval [code fun]:
-  "number_of Numeral.Pls = (0::int)"
-  and "number_of Numeral.Min = uminus (1::int)"
-  and "number_of (n BIT bit.B0) = (2::int) * number_of n"
-  and "number_of (n BIT bit.B1) = (2::int) * number_of n + 1"
-  by simp_all
-
 lemma elim_nat [code unfolt]:
   "(number_of n :: nat) = nat (number_of n)"
   by simp
@@ -800,6 +793,10 @@
   "(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
   by simp
 
+lemma elim_one_nat [code unfolt]:
+  "1 = Suc 0"
+  by simp
+
 lemmas [code unfolt] =
   bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
   bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0