# HG changeset patch
# User haftmann
# Date 1162283333 -3600
# Node ID fc98cb66c5c332d439da925fc68e4aed8f7f4139
# Parent  f8f89be75e81696baa23048df923c08cc1a8a176
adaptions to changes in preprocessor

diff -r f8f89be75e81 -r fc98cb66c5c3 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Tue Oct 31 09:28:52 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Tue Oct 31 09:28:53 2006 +0100
@@ -104,88 +104,21 @@
 *}
 
 code_const arbitrary
-  (Haskell target_atom "(error \"arbitrary\")")
+  (Haskell "error/ \"arbitrary\"")
 
 code_reserved SML Fail
 code_reserved Haskell error
 
-subsection {* Operational equality for code generation *}
 
-subsubsection {* eq class *}
-
-class eq =
-  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
-  eq_def [normal post]: "eq \<equiv> (op =)"
-
-lemmas [symmetric, code inline] = eq_def
-
-
-subsubsection {* bool type *}
-
-instance bool :: eq ..
-
-lemma [code func]:
-  "eq True p = p" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq False p = (\<not> p)" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq p True = p" unfolding eq_def by auto
-
-lemma [code func]:
-  "eq p False = (\<not> p)" unfolding eq_def by auto
-
-
-subsubsection {* preprocessors *}
+subsection {* normalization by evaluation *}
 
 setup {*
 let
-  fun constrain_op_eq thy ts =
-    let
-      fun add_eq (Const ("op =", ty)) =
-            fold (insert (eq_fst (op = : indexname * indexname -> bool)))
-              (Term.add_tvarsT ty [])
-        | add_eq _ =
-            I
-      val eqs = (fold o fold_aterms) add_eq ts [];
-      val inst = map (fn (v_i, _) => (v_i, [HOLogic.class_eq])) eqs;
-    in inst end;
-in CodegenData.add_constrains constrain_op_eq end
-*}
-
-
-subsubsection {* Haskell *}
-
-code_class eq
-  (Haskell "Eq" where eq \<equiv> "(==)")
-
-code_const eq
-  (Haskell infixl 4 "==")
-
-code_instance bool :: eq
-  (Haskell -)
-
-code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-  (Haskell infixl 4 "==")
-
-code_reserved Haskell
-  Eq eq
-
-subsection {* normalization by evaluation *}
-
-lemma eq_refl: "eq x x"
-  unfolding eq_def ..
-
-setup {*
-let
-  val eq_refl = thm "eq_refl";
   fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
-    (Drule.goals_conv (equal i) (HOL.Trueprop_conv NBE.normalization_conv)));
+    (Drule.goals_conv (equal i) (HOL.Trueprop_conv
+      (HOL.Equals_conv NBE.normalization_conv))));
   val normalization_meth =
-    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl, eq_refl] 1));
+    Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
 in
   Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
 end;
@@ -207,6 +140,54 @@
   unfolding if_delayed_def ..
 
 
+subsection {* Operational equality for code generation *}
+
+subsubsection {* eq class *}
+
+class eq =
+  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+
+defs
+  eq_def [normal post]: "eq \<equiv> (op =)"
+
+lemmas [symmetric, code inline, code func] = eq_def
+
+
+subsubsection {* bool type *}
+
+instance bool :: eq ..
+
+lemma [code func]:
+  "eq True p = p" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq False p = (\<not> p)" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq p True = p" unfolding eq_def by auto
+
+lemma [code func]:
+  "eq p False = (\<not> p)" unfolding eq_def by auto
+
+
+subsubsection {* Haskell *}
+
+code_class eq
+  (Haskell "Eq" where eq \<equiv> "(==)")
+
+code_const eq
+  (Haskell infixl 4 "==")
+
+code_instance bool :: eq
+  (Haskell -)
+
+code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_reserved Haskell
+  Eq eq
+
+
 hide (open) const eq if_delayed
 
 end
\ No newline at end of file