# HG changeset patch
# User haftmann
# Date 1149692114 -7200
# Node ID bb16bf9ae3fd06979f8bc3ed58f2da753f43da89
# Parent  a8c8ed1c85e0556891dbf20c89761f13fd35df5e
slight code generator cleanup

diff -r a8c8ed1c85e0 -r bb16bf9ae3fd src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Jun 07 16:54:30 2006 +0200
+++ b/src/HOL/Datatype.thy	Wed Jun 07 16:55:14 2006 +0200
@@ -219,20 +219,20 @@
   done
 
 
+subsubsection {* Codegenerator setup *}
+
 consts
   is_none :: "'a option \<Rightarrow> bool"
 primrec
   "is_none None = True"
   "is_none (Some x) = False"
 
-(* lemma is_none_none [code unfolt]:
+lemma is_none_none [code unfolt]:
   "(x = None) = (is_none x)" 
-by (cases "x") simp_all *)
+by (cases "x") simp_all
 
 lemmas [code] = imp_conv_disj
 
-subsubsection {* Codegenerator setup *}
-
 lemma [code fun]:
   "(\<not> True) = False" by (rule HOL.simp_thms)
 
@@ -260,8 +260,6 @@
 lemma [code unfolt]:
   "1 == Suc 0" by simp
 
-code_generate True False Not "op &" "op |" If
-
 code_syntax_tyco bool
   ml (target_atom "bool")
   haskell (target_atom "Bool")
@@ -286,8 +284,6 @@
     ml (target_atom "(if __/ then __/ else __)")
     haskell (target_atom "(if __/ then __/ else __)")
 
-code_generate Pair
-
 code_syntax_tyco
   *
     ml (infix 2 "*")
@@ -298,8 +294,6 @@
     ml (target_atom "(__,/ __)")
     haskell (target_atom "(__,/ __)")
 
-code_generate Unity
-
 code_syntax_tyco
   unit
     ml (target_atom "unit")
@@ -310,8 +304,6 @@
     ml (target_atom "()")
     haskell (target_atom "()")
 
-code_generate None Some
-
 code_syntax_tyco
   option
     ml ("_ option")
@@ -325,7 +317,4 @@
     ml (target_atom "SOME")
     haskell (target_atom "Just")
 
-
-
-
 end
diff -r a8c8ed1c85e0 -r bb16bf9ae3fd src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Jun 07 16:54:30 2006 +0200
+++ b/src/HOL/List.thy	Wed Jun 07 16:55:14 2006 +0200
@@ -270,9 +270,9 @@
 lemma null_empty: "null xs = (xs = [])"
   by (cases xs) simp_all
 
-(*lemma empty_null [code unfolt]:
+lemma empty_null [code unfolt]:
   "(xs = []) = null xs"
-using null_empty [symmetric] .*)
+using null_empty [symmetric] .
 
 subsubsection {* @{text length} *}
 
@@ -2240,7 +2240,8 @@
 use @{prop"x : set xs"} instead --- it is much easier to reason about.
 The same is true for @{const list_all} and @{const list_ex}: write
 @{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL
-quantifiers are aleady known to the automatic provers. In fact, the declarations in the Code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"}
+quantifiers are aleady known to the automatic provers. In fact,
+the declarations in the code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"}
 and @{text"\<exists>x\<in>set xs"} are implemented efficiently.
 
 The functions @{const itrev}, @{const filtermap} and @{const
@@ -2736,8 +2737,6 @@
   "List.op @" "List.append"
   "List.op mem" "List.mem"
 
-code_generate Nil Cons
-
 code_syntax_tyco
   list
     ml ("_ list")
diff -r a8c8ed1c85e0 -r bb16bf9ae3fd src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Wed Jun 07 16:54:30 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 07 16:55:14 2006 +0200
@@ -14,7 +14,7 @@
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   "xor p q = ((p | q) & \<not> (p & q))"
 
-code_generate xor
+code_generate (ml) xor
 
 subsection {* natural numbers *}
 
@@ -24,7 +24,9 @@
   n :: nat
   "n = 42"
 
-code_generate
+code_generate (ml) n
+
+code_generate (ml)
   "0::nat" "one" n
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -42,7 +44,7 @@
   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
   "appl p = (let (f, x) = p in f x)"
 
-code_generate Pair fst snd Let split swap swapp appl
+code_generate (ml) Pair fst snd Let split swap swapp appl
 
 definition
   k :: "int"
@@ -54,7 +56,7 @@
 recdef fac "measure nat"
   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
 
-code_generate
+code_generate (ml)
   "0::int" k
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   "op - :: int \<Rightarrow> int \<Rightarrow> int"
@@ -65,11 +67,11 @@
 
 subsection {* sums *}
 
-code_generate Inl Inr
+code_generate (ml) Inl Inr
 
 subsection {* options *}
 
-code_generate None Some
+code_generate (ml) None Some
 
 subsection {* lists *}
 
@@ -79,7 +81,7 @@
   qs :: "nat list"
   "qs == rev ps"
 
-code_generate hd tl "op @" ps qs
+code_generate (ml) hd tl "op @" ps qs
 
 subsection {* mutual datatypes *}
 
@@ -96,11 +98,11 @@
   "mut2 mut2.Tip = mut2.Tip"
   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
 
-code_generate mut1 mut2
+code_generate (ml) mut1 mut2
 
 subsection {* equalities *}
 
-code_generate
+code_generate (ml)
   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
@@ -111,6 +113,7 @@
   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
 
+
 subsection {* heavy usage of names *}
 
 definition
@@ -126,7 +129,7 @@
   "Codegenerator.g" "Mymod.A.f"
   "Codegenerator.h" "Mymod.A.B.f"
 
-code_generate f g h
+code_generate (ml) f g h
 
 code_serialize ml (-)