# HG changeset patch
# User haftmann
# Date 1157092611 -7200
# Node ID 855f07fabd76e7087ddebf5f6abfee19954ae73a
# Parent  6d8b29c7a960fcb2cce220d93214d55204a0b451
final syntax for some Isar code generator keywords

diff -r 6d8b29c7a960 -r 855f07fabd76 NEWS
--- a/NEWS	Thu Aug 31 23:01:16 2006 +0200
+++ b/NEWS	Fri Sep 01 08:36:51 2006 +0200
@@ -48,16 +48,45 @@
 Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples.
 
 * Yet another code generator framework allows to generate executable code
-for ML and Haskell (including "class"es). Most basic use cases:
+for ML and Haskell (including "class"es). A short usage sketch:
 
     internal compilation:
-        code_serialize ml <list of constants (term syntax)> (-)
-    writing ML code to a file:
-        code_serialize ml <list of constants (term syntax)> (<filename>)
+        code_gen <list of constants (term syntax)> (SML -)
+    writing SML code to a file:
+        code_gen <list of constants (term syntax)> (SML <filename>)
     writing Haskell code to a bunch of files:
-        code_serialize haskell <list of constants (term syntax)> (<filename>)
-
-See HOL/ex/Codegenerator.thy for examples.
+        code_gen <list of constants (term syntax)> (Haskell <filename>)
+
+Reasonable default setup of framework in HOL/Main.
+
+See HOL/ex/Code*.thy for examples.
+
+Theorem attributs for selecting and transforming function equations theorems:
+
+    [code fun]:       select a theorem as function equation for a specific constant
+    [code nofun]:     deselect a theorem as function equation for a specific constant
+    [code inline]:    select an equation theorem for unfolding (inlining) in place
+    [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
+
+User-defined serializations (target in {SML, Haskell}):
+
+    code_const <and-list of constants (term syntax)>
+      {(target) <and-list of const target syntax>}+
+
+    code_type <and-list of type constructors>
+      {(target) <and-list of type target syntax>}+
+
+    code_instance <and-list of instances>
+      {(target)}+
+        where instance ::= <type constructor> :: <class>
+
+    code_class <and_list of classes>
+      {(target) <and-list of class target syntax>}+
+        where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
+
+For code_instance and code_class, target SML is silently ignored.
+
+See HOL theories and HOL/ex/Code*.thy for usage examples.
 
 * Command 'no_translations' removes translation rules from theory
 syntax.
diff -r 6d8b29c7a960 -r 855f07fabd76 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Fri Sep 01 08:36:51 2006 +0200
@@ -43,8 +43,9 @@
     "classrel"
     "clear_undos"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
@@ -52,7 +53,7 @@
     "code_purge"
     "code_serialize"
     "code_simtype"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "commit"
@@ -368,15 +369,16 @@
     "classes"
     "classrel"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "const_syntax"
diff -r 6d8b29c7a960 -r 855f07fabd76 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords-ZF.el	Fri Sep 01 08:36:51 2006 +0200
@@ -41,8 +41,9 @@
     "clear_undos"
     "codatatype"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
@@ -50,7 +51,7 @@
     "code_purge"
     "code_serialize"
     "code_simtype"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "commit"
@@ -354,15 +355,16 @@
     "classrel"
     "codatatype"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "const_syntax"
diff -r 6d8b29c7a960 -r 855f07fabd76 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords.el	Fri Sep 01 08:36:51 2006 +0200
@@ -43,8 +43,9 @@
     "classrel"
     "clear_undos"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
@@ -52,7 +53,7 @@
     "code_purge"
     "code_serialize"
     "code_simtype"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "commit"
@@ -389,15 +390,16 @@
     "classes"
     "classrel"
     "code_class"
-    "code_constapp"
+    "code_const"
     "code_constname"
+    "code_gen"
     "code_generate"
     "code_instance"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_typapp"
+    "code_type"
     "code_typename"
     "coinductive"
     "const_syntax"
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Datatype.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -261,61 +261,40 @@
   "split = prod_case"
 by (simp add: expand_fun_eq split_def prod.cases)
 
-code_typapp bool
-  ml (target_atom "bool")
-  haskell (target_atom "Bool")
+code_type bool
+  (SML target_atom "bool")
+  (Haskell target_atom "Bool")
 
-code_constapp
-  True
-    ml (target_atom "true")
-    haskell (target_atom "True")
-  False
-    ml (target_atom "false")
-    haskell (target_atom "False")
-  Not
-    ml (target_atom "not")
-    haskell (target_atom "not")
-  "op &"
-    ml (infixl 1 "andalso")
-    haskell (infixl 3 "&&")
-  "op |"
-    ml (infixl 0 "orelse")
-    haskell (infixl 2 "||")
-  If
-    ml (target_atom "(if __/ then __/ else __)")
-    haskell (target_atom "(if __/ then __/ else __)")
+code_const True and False and Not and "op &" and "op |" and If
+  (SML target_atom "true" and target_atom "false" and target_atom "not"
+    and infixl 1 "andalso" and infixl 0 "orelse"
+    and target_atom "(if __/ then __/ else __)")
+  (Haskell target_atom "True" and target_atom "False" and target_atom "not"
+    and infixl 3 "&&" and infixl 2 "||"
+    and target_atom "(if __/ then __/ else __)")
+
+code_type *
+  (SML infix 2 "*")
+  (Haskell target_atom "(__,/ __)")
 
-code_typapp
-  *
-    ml (infix 2 "*")
-    haskell (target_atom "(__,/ __)")
+code_const Pair
+  (SML target_atom "(__,/ __)")
+  (Haskell target_atom "(__,/ __)")
 
-code_constapp
-  Pair
-    ml (target_atom "(__,/ __)")
-    haskell (target_atom "(__,/ __)")
-
-code_typapp
-  unit
-    ml (target_atom "unit")
-    haskell (target_atom "()")
+code_type unit
+  (SML target_atom "unit")
+  (Haskell target_atom "()")
 
-code_constapp
-  Unity
-    ml (target_atom "()")
-    haskell (target_atom "()")
+code_const Unity
+  (SML target_atom "()")
+  (Haskell target_atom "()")
 
-code_typapp
-  option
-    ml ("_ option")
-    haskell ("Maybe _")
+code_type option
+  (SML "_ option")
+  (Haskell "Maybe _")
 
-code_constapp
-  None
-    ml (target_atom "NONE")
-    haskell (target_atom "Nothing")
-  Some
-    ml (target_atom "SOME")
-    haskell (target_atom "Just")
+code_const None and Some
+  (SML target_atom "NONE" and target_atom "SOME")
+  (Haskell target_atom "Nothing" and target_atom "Just")
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/HOL.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -1420,9 +1420,8 @@
   CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
 *}
 
-code_constapp
-  "op =" (* an intermediate solution for polymorphic equality *)
-    ml (infixl 6 "=")
-    haskell (infixl 4 "==")
+code_const "op =" (* an intermediate solution for polymorphic equality *)
+  (SML infixl 6 "=")
+  (Haskell infixl 4 "==")
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -902,26 +902,29 @@
   "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                              ("(_ < 0)")
 
-code_typapp int
-  ml (target_atom "IntInf.int")
-  haskell (target_atom "Integer")
+code_type int
+  (SML target_atom "IntInf.int")
+  (Haskell target_atom "Integer")
+
+code_const "op + :: int \<Rightarrow> int \<Rightarrow> int"
+  (SML "IntInf.+ (_, _)")
+  (Haskell infixl 6 "+")
+
+code_const "op * :: int \<Rightarrow> int \<Rightarrow> int"
+  (SML "IntInf.* (_, _)")
+  (Haskell infixl 7 "*")
 
-code_constapp
-  "op + :: int \<Rightarrow> int \<Rightarrow> int"
-    ml ("IntInf.+ (_, _)")
-    haskell (infixl 6 "+")
-  "op * :: int \<Rightarrow> int \<Rightarrow> int"
-    ml ("IntInf.* (_, _)")
-    haskell (infixl 7 "*")
-  "uminus :: int \<Rightarrow> int"
-    ml (target_atom "IntInf.~")
-    haskell (target_atom "negate")
-  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
-    ml ("(op =) (_ : IntInf.int, _)")
-    haskell (infixl 4 "==")
-  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
-    ml ("IntInf.<= (_, _)")
-    haskell (infix 4 "<=")
+code_const "uminus :: int \<Rightarrow> int"
+  (SML target_atom "IntInf.~")
+  (Haskell target_atom "negate")
+
+code_const "op = :: int \<Rightarrow> int \<Rightarrow> bool"
+  (SML "(op =) (_ : IntInf.int, _)")
+  (Haskell infixl 4 "==")
+
+code_const "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
+  (SML "IntInf.<= (_, _)")
+  (Haskell infix 4 "<=")
 
 ML {*
 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -501,9 +501,9 @@
   arbitrary :: "'a"       ("(error \"arbitrary\")")
   arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
 
-code_constapp
-  "arbitrary :: 'a"       ml (target_atom "(error \"arbitrary\")")
-  "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
+code_const "arbitrary :: 'a" and "arbitrary :: 'a \<Rightarrow> 'b"
+  (SML target_atom "(error \"arbitrary\")"
+    and target_atom "(fn '_ => error \"arbitrary\")")
 
 code_module Norm
 contains
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -61,23 +61,17 @@
   "nat_less_equal m n = (int m <= int n)"
   "nat_eq m n = (int m = int n)"
 
-code_typapp nat
-  ml (target_atom "IntInf.int")
-  haskell (target_atom "Integer")
+code_type nat
+  (SML target_atom "IntInf.int")
+  (Haskell target_atom "Integer")
 
-code_constapp
-  "0::nat" (* all constructors of nat must be hidden *)
-    ml (target_atom "(0 :: IntInf.int)")
-    haskell (target_atom "0")
-  Suc (* all constructors of nat must be hidden *)
-    ml ("IntInf.+ (_, 1)")
-    haskell ("(+) 1 _")
-  nat
-    ml (target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)")
-    haskell (target_atom "(\\n :: Int -> if n < 0 then 0 else n)")
-  int
-    ml ("_")
-    haskell ("_")
+code_const "0::nat" and Suc (*all constructors of nat must be hidden*)
+  (SML target_atom "(0 :: IntInf.int)" and "IntInf.+ (_, 1)")
+  (Haskell target_atom "0" and "(+) 1 _")
+
+code_const nat and int
+  (SML target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)" and "_")
+  (Haskell target_atom "(\\n :: Int -> if n < 0 then 0 else n)" and "_")
 
 text {*
   Eliminate @{const "0::nat"} and @{const "1::nat"}
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -81,11 +81,12 @@
 types_code
   rat ("{*erat*}")
 
-code_generate (ml, haskell) Rat
+code_gen Rat
+  (SML) (Haskell)
 
-code_typapp rat
-  ml ("{*erat*}")
-  haskell ("{*erat*}")
+code_type rat
+  (SML "{*erat*}")
+  (Haskell "{*erat*}")
 
 
 section {* const serializations *}
@@ -103,12 +104,11 @@
   Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}")
 
-code_constapp
-  "arbitrary :: erat"
-    ml ("raise/ (Fail/ \"non-defined rational number\")")
-    haskell ("error/ \"non-defined rational number\"")
+code_const "arbitrary :: erat"
+  (SML "raise/ (Fail/ \"non-defined rational number\")")
+  (Haskell "error/ \"non-defined rational number\"")
 
-code_generate (ml, haskell)
+code_gen
   of_quotient
   "0::erat"
   "1::erat"
@@ -118,37 +118,46 @@
   "inverse :: erat \<Rightarrow> erat"
   "op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
   eq_rat
+  (SML) (Haskell)
 
-code_constapp
-  Fract
-    ml ("{*of_quotient*}")
-    haskell ("{*of_quotient*}")
-  "0 :: rat"
-    ml ("{*0::erat*}")
-    haskell ("{*1::erat*}")
-  "1 :: rat"
-    ml ("{*1::erat*}")
-    haskell ("{*1::erat*}")
-  "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
-    ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-    haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  "uminus :: rat \<Rightarrow> rat"
-    ml ("{*uminus :: erat \<Rightarrow> erat*}")
-    haskell ("{*uminus :: erat \<Rightarrow> erat*}")
-  "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
-    ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-    haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
-  "inverse :: rat \<Rightarrow> rat"
-    ml ("{*inverse :: erat \<Rightarrow> erat*}")
-    haskell ("{*inverse :: erat \<Rightarrow> erat*}")
-  "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
-    ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
-    haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
-  "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
-    ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
-    haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
-  "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
-    ml ("{*eq_rat*}")
-    haskell ("{*eq_rat*}")
+code_const Fract
+  (SML "{*of_quotient*}")
+  (Haskell "{*of_quotient*}")
+
+code_const "0 :: rat"
+  (SML "{*0::erat*}")
+  (Haskell "{*1::erat*}")
+
+code_const "1 :: rat"
+  (SML "{*1::erat*}")
+  (Haskell "{*1::erat*}")
+
+code_const "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
+  (SML "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+  (Haskell "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+
+code_const "uminus :: rat \<Rightarrow> rat"
+  (SML "{*uminus :: erat \<Rightarrow> erat*}")
+  (Haskell "{*uminus :: erat \<Rightarrow> erat*}")
+
+code_const "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
+  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+
+code_const "inverse :: rat \<Rightarrow> rat"
+  (SML "{*inverse :: erat \<Rightarrow> erat*}")
+  (Haskell "{*inverse :: erat \<Rightarrow> erat*}")
+
+code_const "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
+  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
+  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
+
+code_const "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
+  (SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+  (Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+
+code_const "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
+  (SML "{*eq_rat*}")
+  (Haskell "{*eq_rat*}")
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -234,9 +234,9 @@
 and gen_set aG i = gen_set' aG i i;
 *}
 
-code_typapp set
-  ml ("_ list")
-  haskell (target_atom "[_]")
+code_type set
+  (SML "_ list")
+  (Haskell target_atom "[_]")
 
 
 subsection {* const serializations *}
@@ -261,46 +261,57 @@
   "ExecutableSet.insertl" "List.insertl"
   "ExecutableSet.drop_first" "List.drop_first"
 
-code_generate (ml, haskell) 
+code_gen
   insertl unionl intersect flip subtract map_distinct
   unions intersects map_union map_inter Blall Blex
+  (SML) (Haskell) 
 
-code_constapp
-  "{}"
-    ml (target_atom "[]")
-    haskell (target_atom "[]")
-  insert
-    ml ("{*insertl*}")
-    haskell ("{*insertl*}")
-  "op \<union>"
-    ml ("{*unionl*}")
-    haskell ("{*unionl*}")
-  "op \<inter>"
-    ml ("{*intersect*}")
-    haskell ("{*intersect*}")
-  "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-    ml ("{*flip subtract*}")
-    haskell ("{*flip subtract*}")
-  image
-    ml ("{*map_distinct*}")
-    haskell ("{*map_distinct*}")
-  "Union"
-    ml ("{*unions*}")
-    haskell ("{*unions*}")
-  "Inter"
-    ml ("{*intersects*}")
-    haskell ("{*intersects*}")
-  UNION
-    ml ("{*map_union*}")
-    haskell ("{*map_union*}")
-  INTER
-    ml ("{*map_inter*}")
-    haskell ("{*map_inter*}")
-  Ball
-    ml ("{*Blall*}")
-    haskell ("{*Blall*}")
-  Bex
-    ml ("{*Blex*}")
-    haskell ("{*Blex*}")
+code_const "{}"
+  (SML target_atom "[]")
+  (Haskell target_atom "[]")
+
+code_const insert
+  (SML "{*insertl*}")
+  (Haskell "{*insertl*}")
+
+code_const "op \<union>"
+  (SML "{*unionl*}")
+  (Haskell "{*unionl*}")
+
+code_const "op \<inter>"
+  (SML "{*intersect*}")
+  (Haskell "{*intersect*}")
+
+code_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+  (SML "{*flip subtract*}")
+  (Haskell "{*flip subtract*}")
+
+code_const image
+  (SML "{*map_distinct*}")
+  (Haskell "{*map_distinct*}")
+
+code_const "Union"
+  (SML "{*unions*}")
+  (Haskell "{*unions*}")
+
+code_const "Inter"
+  (SML "{*intersects*}")
+  (Haskell "{*intersects*}")
+
+code_const UNION
+  (SML "{*map_union*}")
+  (Haskell "{*map_union*}")
+
+code_const INTER
+  (SML "{*map_inter*}")
+  (Haskell "{*map_inter*}")
+
+code_const Ball
+  (SML "{*Blall*}")
+  (Haskell "{*Blall*}")
+
+code_const Bex
+  (SML "{*Blex*}")
+  (Haskell "{*Blex*}")
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/MLString.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -5,7 +5,7 @@
 header {* Monolithic strings for ML  *}
 
 theory MLString
-imports Main
+imports List
 begin
 
 section {* Monolithic strings for ML *}
@@ -58,31 +58,20 @@
 
 subsection {* Code serialization *}
 
-code_typapp ml_string
-  ml (target_atom "string")
-  haskell (target_atom "String")
+code_type ml_string
+  (SML target_atom "string")
+  (Haskell target_atom "String")
 
-code_constapp STR
-  haskell ("_")
+code_const STR
+  (Haskell "_")
 
 setup {*
-let
-  fun print_char c =
-    let
-      val i = ord c
-    in if i < 32
-      then prefix "\\" (string_of_int i)
-      else c
-    end;
-  val print_string = quote;
-in 
-  CodegenPackage.add_pretty_ml_string "ml" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
-    print_char print_string "String.implode"
-end
+  CodegenPackage.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
+    HOList.print_char HOList.print_string "String.implode"
 *}
 
-code_constapp explode
-  ml (target_atom "String.explode")
-  haskell ("_")
+code_const explode
+  (SML target_atom "String.explode")
+  (Haskell "_")
 
-end
\ No newline at end of file
+end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/List.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -2650,6 +2650,28 @@
 fun nibble_of_int i =
   if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
 
+fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
+      let
+        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
+          | dest_nibble _ = raise Match;
+      in
+        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
+        handle Fail _ => NONE | Match => NONE)
+      end
+  | dest_char _ = NONE;
+
+val print_list = Pretty.enum "," "[" "]";
+
+fun print_char c =
+  let
+    val i = ord c
+  in if i < 32
+    then prefix "\\" (string_of_int i)
+    else c
+  end;
+
+val print_string = quote;
+
 fun term_string s =
   let
     val ty_n = Type ("List.nibble", []);
@@ -2693,61 +2715,9 @@
   in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
 *}
 
+
 subsubsection {* Code generator setup *}
 
-ML {*
-local
-
-fun list_codegen thy defs gr dep thyname b t =
-  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
-    (gr, HOLogic.dest_list t)
-  in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
-
-fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
-      let
-        fun dest_nibble (Const (s, _)) = (HOList.int_of_nibble o unprefix "List.nibble.Nibble") s
-          | dest_nibble _ = raise Match;
-      in
-        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
-        handle Fail _ => NONE | Match => NONE)
-      end
-  | dest_char _ = NONE;
-
-fun char_codegen thy defs gr dep thyname b t =
-  case (Option.map chr o dest_char) t 
-   of SOME c =>
-        if Symbol.is_printable c
-        then SOME (gr, (Pretty.quote o Pretty.str) c)
-        else NONE
-    | NONE => NONE;
-
-val print_list = Pretty.enum "," "[" "]";
-
-fun print_char c =
-  let
-    val i = ord c
-  in if i < 32
-    then prefix "\\" (string_of_int i)
-    else c
-  end;
-
-val print_string = quote;
-
-in
-
-val list_codegen_setup =
-  Codegen.add_codegen "list_codegen" list_codegen
-  #> Codegen.add_codegen "char_codegen" char_codegen
-  #> CodegenPackage.add_pretty_list "ml" "List.list.Nil" "List.list.Cons"
-       print_list NONE (7, "::")
-  #> CodegenPackage.add_pretty_list "haskell" "List.list.Nil" "List.list.Cons"
-       print_list (SOME (print_char, print_string)) (5, ":")
-  #> CodegenPackage.add_appconst
-       ("List.char.Char", CodegenPackage.appgen_char dest_char);
-
-end;
-*}
-
 types_code
   "list" ("_ list")
 attach (term_of) {*
@@ -2773,26 +2743,50 @@
 
 consts_code "Cons" ("(_ ::/ _)")
 
-code_typapp
-  list
-    ml ("_ list")
-    haskell (target_atom "[_]")
-
-code_constapp
-  Nil
-    ml (target_atom "[]")
-    haskell (target_atom "[]")
-
-code_typapp
-  char
-    ml (target_atom "char")
-    haskell (target_atom "Char")
-
-code_constapp
-  Char
-    ml (target_atom "(__,/ __)")
-    haskell (target_atom "(__,/ __)")
-
-setup list_codegen_setup
+code_type list
+  (SML "_ list")
+  (Haskell target_atom "[_]")
+
+code_const Nil
+  (SML target_atom "[]")
+  (Haskell target_atom "[]")
+
+code_type char
+  (SML target_atom "char")
+  (Haskell target_atom "Char")
+
+code_const Char
+  (SML target_atom "(__,/ __)")
+  (Haskell target_atom "(__,/ __)")
+
+setup {*
+let
+
+fun list_codegen thy defs gr dep thyname b t =
+  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
+    (gr, HOLogic.dest_list t)
+  in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
+
+fun char_codegen thy defs gr dep thyname b t =
+  case (Option.map chr o HOList.dest_char) t 
+   of SOME c =>
+        if Symbol.is_printable c
+        then SOME (gr, (Pretty.quote o Pretty.str) c)
+        else NONE
+    | NONE => NONE;
+
+in
+
+  Codegen.add_codegen "list_codegen" list_codegen
+  #> Codegen.add_codegen "char_codegen" char_codegen
+  #> CodegenPackage.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
+       HOList.print_list NONE (7, "::")
+  #> CodegenPackage.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
+       HOList.print_list (SOME (HOList.print_char, HOList.print_string)) (5, ":")
+  #> CodegenPackage.add_appconst
+       ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char)
+
+end;
+*}
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -295,10 +295,9 @@
   CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
 *}
 
-code_constapp
-  wfrec
-    ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
-    haskell (target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
+code_const wfrec
+  (SML target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
+  (Haskell target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
 
 subsection{*Variants for TFL: the Recdef Package*}
 
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -319,10 +319,10 @@
   "x2 = X (1::int) 2 3"
   "y2 = Y (1::int) 2 3"
 
-code_generate "op \<otimes>" \<one> inv
-code_generate (ml, haskell) X Y
-code_generate (ml, haskell) x1 x2 y2
+code_gen "op \<otimes>" \<one> inv
+code_gen X Y (SML) (Haskell)
+code_gen x1 x2 y2 (SML) (Haskell)
 
-code_serialize ml (-)
+code_gen (SML -)
 
 end
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeCollections.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -402,16 +402,16 @@
   "test1 = sum [None, Some True, None, Some False]"
   "test2 = (inf :: nat \<times> unit)"
 
-code_generate eq
-code_generate "op <<="
-code_generate "op <<"
-code_generate inf
-code_generate between
-code_generate index
-code_generate sum
-code_generate test1
-code_generate test2
+code_gen eq
+code_gen "op <<="
+code_gen "op <<"
+code_gen inf
+code_gen between
+code_gen index
+code_gen sum
+code_gen test1
+code_gen test2
 
-code_serialize ml (-)
+code_gen (SML -)
 
 end
\ No newline at end of file
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeEmbed.thy
--- a/src/HOL/ex/CodeEmbed.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeEmbed.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -77,15 +77,12 @@
 
 subsection {* Code serialization setup *}
 
-code_typapp
-  "typ"  ml (target_atom "Term.typ")
-  "term" ml (target_atom "Term.term")
+code_type "typ" and "term"
+  (SML target_atom "Term.typ" and target_atom "Term.term")
 
-code_constapp
-  Type  ml ("Term.Type (_, _)")
-  TFix  ml ("Term.TFree (_, _)")
-  Const ml ("Term.Const (_, _)")
-  App   ml ("Term.$ (_, _)")
-  Fix   ml ("Term.Free (_, _)")
+code_const Type and TFix
+  and Const and App and Fix
+  (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
+    and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
 
 end
\ No newline at end of file
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -194,7 +194,7 @@
 and ('a, 'b) cair =
     Cair 'a 'b
 
-code_generate term_of
+code_gen term_of
 
 ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
 
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeOperationalEquality.thy
--- a/src/HOL/ex/CodeOperationalEquality.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeOperationalEquality.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -117,9 +117,9 @@
   "eq k l = eq_integer k l"
 unfolding eq_integer_def eq_def ..
 
-code_constapp eq_integer
-  ml (infixl 6 "=")
-  haskell (infixl 4 "==")
+code_const eq_integer
+  (SML infixl 6 "=")
+  (Haskell infixl 4 "==")
 
 
 subsection {* codegenerator setup *}
@@ -134,33 +134,34 @@
 subsection {* haskell setup *}
 
 code_class eq
-  haskell "Eq" (eq "(==)")
+  (Haskell "Eq" where eq \<equiv> "(==)")
+
+code_instance eq :: bool and eq :: unit and eq :: *
+  and eq :: option and eq :: list and eq :: char and eq :: int
+  (Haskell - and - and - and - and - and - and -)
 
-code_instance
-  (eq :: bool) haskell
-  (eq :: unit) haskell
-  (eq :: *) haskell
-  (eq :: option) haskell
-  (eq :: list) haskell
-  (eq :: char) haskell
-  (eq :: int) haskell
+code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
 
-code_constapp
-  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
-    haskell (infixl 4 "==")
-  "eq"
-    haskell (infixl 4 "==")
+code_const "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const "eq"
+  (Haskell infixl 4 "==")
 
 end
\ No newline at end of file
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeRandom.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -167,12 +167,13 @@
 end;
 *}
 
-code_typapp randseed
-  ml (target_atom "Random.seed")
+code_type randseed
+  (SML target_atom "Random.seed")
 
-code_constapp random_int
-  ml (target_atom "Random.value")
+code_const random_int
+  (SML target_atom "Random.value")
 
-code_serialize ml select select_weight (-)
+code_gen select select_weight
+  (SML -)
 
 end
\ No newline at end of file
diff -r 6d8b29c7a960 -r 855f07fabd76 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Fri Sep 01 08:36:51 2006 +0200
@@ -90,21 +90,19 @@
   g "Mymod.A.f"
   h "Mymod.A.B.f"
 
-code_generate (ml, haskell)
-  n one "0::int" "0::nat" "1::int" "1::nat"
-code_generate (ml, haskell)
-  fac
-code_generate
-  xor
-code_generate
+code_gen xor
+code_gen one "0::nat" "1::nat"
+code_gen "0::int" "1::int" n fac
+  (SML) (Haskell)
+code_gen
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
-code_generate
+code_gen
   Pair fst snd Let split swap swapp appl
-code_generate (ml, haskell)
+code_gen
   k
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   "op - :: int \<Rightarrow> int \<Rightarrow> int"
@@ -114,15 +112,16 @@
   fac
   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
-code_generate
+  (SML) (Haskell)
+code_gen
   Inl Inr
-code_generate
+code_gen
   None Some
-code_generate
+code_gen
   hd tl "op @" ps qs
-code_generate
+code_gen
   mut1 mut2
-code_generate (ml, haskell)
+code_gen
   "op @" filter concat foldl foldr hd tl
   last butlast list_all2
   map 
@@ -143,9 +142,10 @@
   rotate1
   rotate
   splice
-code_generate
+  (SML) (Haskell)
+code_gen
   foo1 foo3
-code_generate (ml, haskell)
+code_gen
   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
@@ -156,9 +156,9 @@
   "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-code_generate
+code_gen
   f g h
 
-code_serialize ml (-)
+code_gen (SML -)
 
 end
\ No newline at end of file