# HG changeset patch
# User haftmann
# Date 1167242993 -3600
# Node ID 59fcfa2a77eabbb52bc12355895f79103bc6bc1c
# Parent  bb5b9c267c1dc06c83ebf9d81a46328100914ee2
moved code generator bool setup here

diff -r bb5b9c267c1d -r 59fcfa2a77ea src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Wed Dec 27 16:24:31 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Wed Dec 27 19:09:53 2006 +0100
@@ -80,6 +80,86 @@
 
 subsection {* Generic code generator setup *}
 
+text {* operational equality for code generation *}
+
+axclass eq \<subseteq> type
+  attach "op ="
+
+
+text {* equality for Haskell *}
+
+code_class eq
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
+
+code_const "op ="
+  (Haskell infixl 4 "==")
+
+
+text {* boolean expressions *}
+
+lemma [code func]:
+  shows "(False \<and> x) = False"
+    and "(True \<and> x) = x"
+    and "(x \<and> False) = False"
+    and "(x \<and> True) = x" by simp_all
+
+lemma [code func]:
+  shows "(False \<or> x) = x"
+    and "(True \<or> x) = True"
+    and "(x \<or> False) = x"
+    and "(x \<or> True) = True" by simp_all
+
+lemma [code func]:
+  shows "(\<not> True) = False"
+    and "(\<not> False) = True" by (rule HOL.simp_thms)+
+
+lemmas [code func] = imp_conv_disj
+
+lemmas [code func] = if_True if_False
+
+instance bool :: eq ..
+
+lemma [code func]:
+  "True = P \<longleftrightarrow> P" by simp
+
+lemma [code func]:
+  "False = P \<longleftrightarrow> \<not> P" by simp
+
+lemma [code func]:
+  "P = True \<longleftrightarrow> P" by simp
+
+lemma [code func]:
+  "P = False \<longleftrightarrow> \<not> P" by simp
+
+code_type bool
+  (SML "bool")
+  (OCaml "bool")
+  (Haskell "Bool")
+
+code_instance bool :: eq
+  (Haskell -)
+
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const True and False and Not and "op &" and "op |" and If
+  (SML "true" and "false" and "not"
+    and infixl 1 "andalso" and infixl 0 "orelse"
+    and "!(if (_)/ then (_)/ else (_))")
+  (OCaml "true" and "false" and "not"
+    and infixl 4 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+  (Haskell "True" and "False" and "not"
+    and infixl 3 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+
+code_reserved SML
+  bool true false not
+
+code_reserved OCaml
+  bool true false not
+
+
 text {* itself as a code generator datatype *}
 
 setup {*
@@ -101,13 +181,14 @@
 
 setup {*
   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
+  #> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")"
 *}
 
 code_const arbitrary
   (Haskell "error/ \"arbitrary\"")
 
 code_reserved SML Fail
-code_reserved Haskell error
+code_reserved OCaml failwith
 
 
 subsection {* Evaluation oracle *}
@@ -194,49 +275,6 @@
   unfolding if_delayed_def ..
 
 
-subsection {* Operational equality for code generation *}
-
-subsubsection {* eq class *}
-
-axclass eq \<subseteq> type
-  attach "op ="
-
-
-subsubsection {* bool type *}
-
-instance bool :: eq ..
-
-lemma [code func]:
-  "True = P \<longleftrightarrow> P" by simp
-
-lemma [code func]:
-  "False = P \<longleftrightarrow> \<not> P" by simp
-
-lemma [code func]:
-  "P = True \<longleftrightarrow> P" by simp
-
-lemma [code func]:
-  "P = False \<longleftrightarrow> \<not> P" by simp
-
-
-subsubsection {* Haskell *}
-
-code_class eq
-  (Haskell "Eq" where "op =" \<equiv> "(==)")
-
-code_const "op ="
-  (Haskell infixl 4 "==")
-
-code_instance bool :: eq
-  (Haskell -)
-
-code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
-
-code_reserved Haskell
-  Eq eq
-
-
 hide (open) const if_delayed
 
 end
\ No newline at end of file