final syntax for some Isar code generator keywords
authorhaftmann
Fri Sep 01 08:36:51 2006 +0200 (2006-09-01)
changeset 20453855f07fabd76
parent 20452 6d8b29c7a960
child 20454 7e948db7e42d
final syntax for some Isar code generator keywords
NEWS
etc/isar-keywords-HOL-Nominal.el
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/HOL/Datatype.thy
src/HOL/HOL.thy
src/HOL/Integ/IntDef.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Library/ExecutableRat.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/Library/MLString.thy
src/HOL/List.thy
src/HOL/Wellfounded_Recursion.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/CodeEmbed.thy
src/HOL/ex/CodeEval.thy
src/HOL/ex/CodeOperationalEquality.thy
src/HOL/ex/CodeRandom.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/NEWS	Thu Aug 31 23:01:16 2006 +0200
     1.2 +++ b/NEWS	Fri Sep 01 08:36:51 2006 +0200
     1.3 @@ -48,16 +48,45 @@
     1.4  Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples.
     1.5  
     1.6  * Yet another code generator framework allows to generate executable code
     1.7 -for ML and Haskell (including "class"es). Most basic use cases:
     1.8 +for ML and Haskell (including "class"es). A short usage sketch:
     1.9  
    1.10      internal compilation:
    1.11 -        code_serialize ml <list of constants (term syntax)> (-)
    1.12 -    writing ML code to a file:
    1.13 -        code_serialize ml <list of constants (term syntax)> (<filename>)
    1.14 +        code_gen <list of constants (term syntax)> (SML -)
    1.15 +    writing SML code to a file:
    1.16 +        code_gen <list of constants (term syntax)> (SML <filename>)
    1.17      writing Haskell code to a bunch of files:
    1.18 -        code_serialize haskell <list of constants (term syntax)> (<filename>)
    1.19 -
    1.20 -See HOL/ex/Codegenerator.thy for examples.
    1.21 +        code_gen <list of constants (term syntax)> (Haskell <filename>)
    1.22 +
    1.23 +Reasonable default setup of framework in HOL/Main.
    1.24 +
    1.25 +See HOL/ex/Code*.thy for examples.
    1.26 +
    1.27 +Theorem attributs for selecting and transforming function equations theorems:
    1.28 +
    1.29 +    [code fun]:       select a theorem as function equation for a specific constant
    1.30 +    [code nofun]:     deselect a theorem as function equation for a specific constant
    1.31 +    [code inline]:    select an equation theorem for unfolding (inlining) in place
    1.32 +    [code noinline]:  deselect an equation theorem for unfolding (inlining) in place
    1.33 +
    1.34 +User-defined serializations (target in {SML, Haskell}):
    1.35 +
    1.36 +    code_const <and-list of constants (term syntax)>
    1.37 +      {(target) <and-list of const target syntax>}+
    1.38 +
    1.39 +    code_type <and-list of type constructors>
    1.40 +      {(target) <and-list of type target syntax>}+
    1.41 +
    1.42 +    code_instance <and-list of instances>
    1.43 +      {(target)}+
    1.44 +        where instance ::= <type constructor> :: <class>
    1.45 +
    1.46 +    code_class <and_list of classes>
    1.47 +      {(target) <and-list of class target syntax>}+
    1.48 +        where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
    1.49 +
    1.50 +For code_instance and code_class, target SML is silently ignored.
    1.51 +
    1.52 +See HOL theories and HOL/ex/Code*.thy for usage examples.
    1.53  
    1.54  * Command 'no_translations' removes translation rules from theory
    1.55  syntax.
     2.1 --- a/etc/isar-keywords-HOL-Nominal.el	Thu Aug 31 23:01:16 2006 +0200
     2.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Fri Sep 01 08:36:51 2006 +0200
     2.3 @@ -43,8 +43,9 @@
     2.4      "classrel"
     2.5      "clear_undos"
     2.6      "code_class"
     2.7 -    "code_constapp"
     2.8 +    "code_const"
     2.9      "code_constname"
    2.10 +    "code_gen"
    2.11      "code_generate"
    2.12      "code_instance"
    2.13      "code_library"
    2.14 @@ -52,7 +53,7 @@
    2.15      "code_purge"
    2.16      "code_serialize"
    2.17      "code_simtype"
    2.18 -    "code_typapp"
    2.19 +    "code_type"
    2.20      "code_typename"
    2.21      "coinductive"
    2.22      "commit"
    2.23 @@ -368,15 +369,16 @@
    2.24      "classes"
    2.25      "classrel"
    2.26      "code_class"
    2.27 -    "code_constapp"
    2.28 +    "code_const"
    2.29      "code_constname"
    2.30 +    "code_gen"
    2.31      "code_generate"
    2.32      "code_instance"
    2.33      "code_library"
    2.34      "code_module"
    2.35      "code_purge"
    2.36      "code_serialize"
    2.37 -    "code_typapp"
    2.38 +    "code_type"
    2.39      "code_typename"
    2.40      "coinductive"
    2.41      "const_syntax"
     3.1 --- a/etc/isar-keywords-ZF.el	Thu Aug 31 23:01:16 2006 +0200
     3.2 +++ b/etc/isar-keywords-ZF.el	Fri Sep 01 08:36:51 2006 +0200
     3.3 @@ -41,8 +41,9 @@
     3.4      "clear_undos"
     3.5      "codatatype"
     3.6      "code_class"
     3.7 -    "code_constapp"
     3.8 +    "code_const"
     3.9      "code_constname"
    3.10 +    "code_gen"
    3.11      "code_generate"
    3.12      "code_instance"
    3.13      "code_library"
    3.14 @@ -50,7 +51,7 @@
    3.15      "code_purge"
    3.16      "code_serialize"
    3.17      "code_simtype"
    3.18 -    "code_typapp"
    3.19 +    "code_type"
    3.20      "code_typename"
    3.21      "coinductive"
    3.22      "commit"
    3.23 @@ -354,15 +355,16 @@
    3.24      "classrel"
    3.25      "codatatype"
    3.26      "code_class"
    3.27 -    "code_constapp"
    3.28 +    "code_const"
    3.29      "code_constname"
    3.30 +    "code_gen"
    3.31      "code_generate"
    3.32      "code_instance"
    3.33      "code_library"
    3.34      "code_module"
    3.35      "code_purge"
    3.36      "code_serialize"
    3.37 -    "code_typapp"
    3.38 +    "code_type"
    3.39      "code_typename"
    3.40      "coinductive"
    3.41      "const_syntax"
     4.1 --- a/etc/isar-keywords.el	Thu Aug 31 23:01:16 2006 +0200
     4.2 +++ b/etc/isar-keywords.el	Fri Sep 01 08:36:51 2006 +0200
     4.3 @@ -43,8 +43,9 @@
     4.4      "classrel"
     4.5      "clear_undos"
     4.6      "code_class"
     4.7 -    "code_constapp"
     4.8 +    "code_const"
     4.9      "code_constname"
    4.10 +    "code_gen"
    4.11      "code_generate"
    4.12      "code_instance"
    4.13      "code_library"
    4.14 @@ -52,7 +53,7 @@
    4.15      "code_purge"
    4.16      "code_serialize"
    4.17      "code_simtype"
    4.18 -    "code_typapp"
    4.19 +    "code_type"
    4.20      "code_typename"
    4.21      "coinductive"
    4.22      "commit"
    4.23 @@ -389,15 +390,16 @@
    4.24      "classes"
    4.25      "classrel"
    4.26      "code_class"
    4.27 -    "code_constapp"
    4.28 +    "code_const"
    4.29      "code_constname"
    4.30 +    "code_gen"
    4.31      "code_generate"
    4.32      "code_instance"
    4.33      "code_library"
    4.34      "code_module"
    4.35      "code_purge"
    4.36      "code_serialize"
    4.37 -    "code_typapp"
    4.38 +    "code_type"
    4.39      "code_typename"
    4.40      "coinductive"
    4.41      "const_syntax"
     5.1 --- a/src/HOL/Datatype.thy	Thu Aug 31 23:01:16 2006 +0200
     5.2 +++ b/src/HOL/Datatype.thy	Fri Sep 01 08:36:51 2006 +0200
     5.3 @@ -261,61 +261,40 @@
     5.4    "split = prod_case"
     5.5  by (simp add: expand_fun_eq split_def prod.cases)
     5.6  
     5.7 -code_typapp bool
     5.8 -  ml (target_atom "bool")
     5.9 -  haskell (target_atom "Bool")
    5.10 +code_type bool
    5.11 +  (SML target_atom "bool")
    5.12 +  (Haskell target_atom "Bool")
    5.13  
    5.14 -code_constapp
    5.15 -  True
    5.16 -    ml (target_atom "true")
    5.17 -    haskell (target_atom "True")
    5.18 -  False
    5.19 -    ml (target_atom "false")
    5.20 -    haskell (target_atom "False")
    5.21 -  Not
    5.22 -    ml (target_atom "not")
    5.23 -    haskell (target_atom "not")
    5.24 -  "op &"
    5.25 -    ml (infixl 1 "andalso")
    5.26 -    haskell (infixl 3 "&&")
    5.27 -  "op |"
    5.28 -    ml (infixl 0 "orelse")
    5.29 -    haskell (infixl 2 "||")
    5.30 -  If
    5.31 -    ml (target_atom "(if __/ then __/ else __)")
    5.32 -    haskell (target_atom "(if __/ then __/ else __)")
    5.33 +code_const True and False and Not and "op &" and "op |" and If
    5.34 +  (SML target_atom "true" and target_atom "false" and target_atom "not"
    5.35 +    and infixl 1 "andalso" and infixl 0 "orelse"
    5.36 +    and target_atom "(if __/ then __/ else __)")
    5.37 +  (Haskell target_atom "True" and target_atom "False" and target_atom "not"
    5.38 +    and infixl 3 "&&" and infixl 2 "||"
    5.39 +    and target_atom "(if __/ then __/ else __)")
    5.40 +
    5.41 +code_type *
    5.42 +  (SML infix 2 "*")
    5.43 +  (Haskell target_atom "(__,/ __)")
    5.44  
    5.45 -code_typapp
    5.46 -  *
    5.47 -    ml (infix 2 "*")
    5.48 -    haskell (target_atom "(__,/ __)")
    5.49 +code_const Pair
    5.50 +  (SML target_atom "(__,/ __)")
    5.51 +  (Haskell target_atom "(__,/ __)")
    5.52  
    5.53 -code_constapp
    5.54 -  Pair
    5.55 -    ml (target_atom "(__,/ __)")
    5.56 -    haskell (target_atom "(__,/ __)")
    5.57 -
    5.58 -code_typapp
    5.59 -  unit
    5.60 -    ml (target_atom "unit")
    5.61 -    haskell (target_atom "()")
    5.62 +code_type unit
    5.63 +  (SML target_atom "unit")
    5.64 +  (Haskell target_atom "()")
    5.65  
    5.66 -code_constapp
    5.67 -  Unity
    5.68 -    ml (target_atom "()")
    5.69 -    haskell (target_atom "()")
    5.70 +code_const Unity
    5.71 +  (SML target_atom "()")
    5.72 +  (Haskell target_atom "()")
    5.73  
    5.74 -code_typapp
    5.75 -  option
    5.76 -    ml ("_ option")
    5.77 -    haskell ("Maybe _")
    5.78 +code_type option
    5.79 +  (SML "_ option")
    5.80 +  (Haskell "Maybe _")
    5.81  
    5.82 -code_constapp
    5.83 -  None
    5.84 -    ml (target_atom "NONE")
    5.85 -    haskell (target_atom "Nothing")
    5.86 -  Some
    5.87 -    ml (target_atom "SOME")
    5.88 -    haskell (target_atom "Just")
    5.89 +code_const None and Some
    5.90 +  (SML target_atom "NONE" and target_atom "SOME")
    5.91 +  (Haskell target_atom "Nothing" and target_atom "Just")
    5.92  
    5.93  end
     6.1 --- a/src/HOL/HOL.thy	Thu Aug 31 23:01:16 2006 +0200
     6.2 +++ b/src/HOL/HOL.thy	Fri Sep 01 08:36:51 2006 +0200
     6.3 @@ -1420,9 +1420,8 @@
     6.4    CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
     6.5  *}
     6.6  
     6.7 -code_constapp
     6.8 -  "op =" (* an intermediate solution for polymorphic equality *)
     6.9 -    ml (infixl 6 "=")
    6.10 -    haskell (infixl 4 "==")
    6.11 +code_const "op =" (* an intermediate solution for polymorphic equality *)
    6.12 +  (SML infixl 6 "=")
    6.13 +  (Haskell infixl 4 "==")
    6.14  
    6.15  end
     7.1 --- a/src/HOL/Integ/IntDef.thy	Thu Aug 31 23:01:16 2006 +0200
     7.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Sep 01 08:36:51 2006 +0200
     7.3 @@ -902,26 +902,29 @@
     7.4    "Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
     7.5    "neg"                              ("(_ < 0)")
     7.6  
     7.7 -code_typapp int
     7.8 -  ml (target_atom "IntInf.int")
     7.9 -  haskell (target_atom "Integer")
    7.10 +code_type int
    7.11 +  (SML target_atom "IntInf.int")
    7.12 +  (Haskell target_atom "Integer")
    7.13 +
    7.14 +code_const "op + :: int \<Rightarrow> int \<Rightarrow> int"
    7.15 +  (SML "IntInf.+ (_, _)")
    7.16 +  (Haskell infixl 6 "+")
    7.17 +
    7.18 +code_const "op * :: int \<Rightarrow> int \<Rightarrow> int"
    7.19 +  (SML "IntInf.* (_, _)")
    7.20 +  (Haskell infixl 7 "*")
    7.21  
    7.22 -code_constapp
    7.23 -  "op + :: int \<Rightarrow> int \<Rightarrow> int"
    7.24 -    ml ("IntInf.+ (_, _)")
    7.25 -    haskell (infixl 6 "+")
    7.26 -  "op * :: int \<Rightarrow> int \<Rightarrow> int"
    7.27 -    ml ("IntInf.* (_, _)")
    7.28 -    haskell (infixl 7 "*")
    7.29 -  "uminus :: int \<Rightarrow> int"
    7.30 -    ml (target_atom "IntInf.~")
    7.31 -    haskell (target_atom "negate")
    7.32 -  "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    7.33 -    ml ("(op =) (_ : IntInf.int, _)")
    7.34 -    haskell (infixl 4 "==")
    7.35 -  "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    7.36 -    ml ("IntInf.<= (_, _)")
    7.37 -    haskell (infix 4 "<=")
    7.38 +code_const "uminus :: int \<Rightarrow> int"
    7.39 +  (SML target_atom "IntInf.~")
    7.40 +  (Haskell target_atom "negate")
    7.41 +
    7.42 +code_const "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    7.43 +  (SML "(op =) (_ : IntInf.int, _)")
    7.44 +  (Haskell infixl 4 "==")
    7.45 +
    7.46 +code_const "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
    7.47 +  (SML "IntInf.<= (_, _)")
    7.48 +  (Haskell infix 4 "<=")
    7.49  
    7.50  ML {*
    7.51  fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
     8.1 --- a/src/HOL/Lambda/WeakNorm.thy	Thu Aug 31 23:01:16 2006 +0200
     8.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Fri Sep 01 08:36:51 2006 +0200
     8.3 @@ -501,9 +501,9 @@
     8.4    arbitrary :: "'a"       ("(error \"arbitrary\")")
     8.5    arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
     8.6  
     8.7 -code_constapp
     8.8 -  "arbitrary :: 'a"       ml (target_atom "(error \"arbitrary\")")
     8.9 -  "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
    8.10 +code_const "arbitrary :: 'a" and "arbitrary :: 'a \<Rightarrow> 'b"
    8.11 +  (SML target_atom "(error \"arbitrary\")"
    8.12 +    and target_atom "(fn '_ => error \"arbitrary\")")
    8.13  
    8.14  code_module Norm
    8.15  contains
     9.1 --- a/src/HOL/Library/EfficientNat.thy	Thu Aug 31 23:01:16 2006 +0200
     9.2 +++ b/src/HOL/Library/EfficientNat.thy	Fri Sep 01 08:36:51 2006 +0200
     9.3 @@ -61,23 +61,17 @@
     9.4    "nat_less_equal m n = (int m <= int n)"
     9.5    "nat_eq m n = (int m = int n)"
     9.6  
     9.7 -code_typapp nat
     9.8 -  ml (target_atom "IntInf.int")
     9.9 -  haskell (target_atom "Integer")
    9.10 +code_type nat
    9.11 +  (SML target_atom "IntInf.int")
    9.12 +  (Haskell target_atom "Integer")
    9.13  
    9.14 -code_constapp
    9.15 -  "0::nat" (* all constructors of nat must be hidden *)
    9.16 -    ml (target_atom "(0 :: IntInf.int)")
    9.17 -    haskell (target_atom "0")
    9.18 -  Suc (* all constructors of nat must be hidden *)
    9.19 -    ml ("IntInf.+ (_, 1)")
    9.20 -    haskell ("(+) 1 _")
    9.21 -  nat
    9.22 -    ml (target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)")
    9.23 -    haskell (target_atom "(\\n :: Int -> if n < 0 then 0 else n)")
    9.24 -  int
    9.25 -    ml ("_")
    9.26 -    haskell ("_")
    9.27 +code_const "0::nat" and Suc (*all constructors of nat must be hidden*)
    9.28 +  (SML target_atom "(0 :: IntInf.int)" and "IntInf.+ (_, 1)")
    9.29 +  (Haskell target_atom "0" and "(+) 1 _")
    9.30 +
    9.31 +code_const nat and int
    9.32 +  (SML target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)" and "_")
    9.33 +  (Haskell target_atom "(\\n :: Int -> if n < 0 then 0 else n)" and "_")
    9.34  
    9.35  text {*
    9.36    Eliminate @{const "0::nat"} and @{const "1::nat"}
    10.1 --- a/src/HOL/Library/ExecutableRat.thy	Thu Aug 31 23:01:16 2006 +0200
    10.2 +++ b/src/HOL/Library/ExecutableRat.thy	Fri Sep 01 08:36:51 2006 +0200
    10.3 @@ -81,11 +81,12 @@
    10.4  types_code
    10.5    rat ("{*erat*}")
    10.6  
    10.7 -code_generate (ml, haskell) Rat
    10.8 +code_gen Rat
    10.9 +  (SML) (Haskell)
   10.10  
   10.11 -code_typapp rat
   10.12 -  ml ("{*erat*}")
   10.13 -  haskell ("{*erat*}")
   10.14 +code_type rat
   10.15 +  (SML "{*erat*}")
   10.16 +  (Haskell "{*erat*}")
   10.17  
   10.18  
   10.19  section {* const serializations *}
   10.20 @@ -103,12 +104,11 @@
   10.21    Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   10.22    "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}")
   10.23  
   10.24 -code_constapp
   10.25 -  "arbitrary :: erat"
   10.26 -    ml ("raise/ (Fail/ \"non-defined rational number\")")
   10.27 -    haskell ("error/ \"non-defined rational number\"")
   10.28 +code_const "arbitrary :: erat"
   10.29 +  (SML "raise/ (Fail/ \"non-defined rational number\")")
   10.30 +  (Haskell "error/ \"non-defined rational number\"")
   10.31  
   10.32 -code_generate (ml, haskell)
   10.33 +code_gen
   10.34    of_quotient
   10.35    "0::erat"
   10.36    "1::erat"
   10.37 @@ -118,37 +118,46 @@
   10.38    "inverse :: erat \<Rightarrow> erat"
   10.39    "op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
   10.40    eq_rat
   10.41 +  (SML) (Haskell)
   10.42  
   10.43 -code_constapp
   10.44 -  Fract
   10.45 -    ml ("{*of_quotient*}")
   10.46 -    haskell ("{*of_quotient*}")
   10.47 -  "0 :: rat"
   10.48 -    ml ("{*0::erat*}")
   10.49 -    haskell ("{*1::erat*}")
   10.50 -  "1 :: rat"
   10.51 -    ml ("{*1::erat*}")
   10.52 -    haskell ("{*1::erat*}")
   10.53 -  "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
   10.54 -    ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.55 -    haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.56 -  "uminus :: rat \<Rightarrow> rat"
   10.57 -    ml ("{*uminus :: erat \<Rightarrow> erat*}")
   10.58 -    haskell ("{*uminus :: erat \<Rightarrow> erat*}")
   10.59 -  "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
   10.60 -    ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.61 -    haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.62 -  "inverse :: rat \<Rightarrow> rat"
   10.63 -    ml ("{*inverse :: erat \<Rightarrow> erat*}")
   10.64 -    haskell ("{*inverse :: erat \<Rightarrow> erat*}")
   10.65 -  "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
   10.66 -    ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
   10.67 -    haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
   10.68 -  "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
   10.69 -    ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   10.70 -    haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   10.71 -  "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
   10.72 -    ml ("{*eq_rat*}")
   10.73 -    haskell ("{*eq_rat*}")
   10.74 +code_const Fract
   10.75 +  (SML "{*of_quotient*}")
   10.76 +  (Haskell "{*of_quotient*}")
   10.77 +
   10.78 +code_const "0 :: rat"
   10.79 +  (SML "{*0::erat*}")
   10.80 +  (Haskell "{*1::erat*}")
   10.81 +
   10.82 +code_const "1 :: rat"
   10.83 +  (SML "{*1::erat*}")
   10.84 +  (Haskell "{*1::erat*}")
   10.85 +
   10.86 +code_const "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
   10.87 +  (SML "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.88 +  (Haskell "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.89 +
   10.90 +code_const "uminus :: rat \<Rightarrow> rat"
   10.91 +  (SML "{*uminus :: erat \<Rightarrow> erat*}")
   10.92 +  (Haskell "{*uminus :: erat \<Rightarrow> erat*}")
   10.93 +
   10.94 +code_const "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
   10.95 +  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.96 +  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
   10.97 +
   10.98 +code_const "inverse :: rat \<Rightarrow> rat"
   10.99 +  (SML "{*inverse :: erat \<Rightarrow> erat*}")
  10.100 +  (Haskell "{*inverse :: erat \<Rightarrow> erat*}")
  10.101 +
  10.102 +code_const "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
  10.103 +  (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
  10.104 +  (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
  10.105 +
  10.106 +code_const "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
  10.107 +  (SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
  10.108 +  (Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
  10.109 +
  10.110 +code_const "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
  10.111 +  (SML "{*eq_rat*}")
  10.112 +  (Haskell "{*eq_rat*}")
  10.113  
  10.114  end
    11.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu Aug 31 23:01:16 2006 +0200
    11.2 +++ b/src/HOL/Library/ExecutableSet.thy	Fri Sep 01 08:36:51 2006 +0200
    11.3 @@ -234,9 +234,9 @@
    11.4  and gen_set aG i = gen_set' aG i i;
    11.5  *}
    11.6  
    11.7 -code_typapp set
    11.8 -  ml ("_ list")
    11.9 -  haskell (target_atom "[_]")
   11.10 +code_type set
   11.11 +  (SML "_ list")
   11.12 +  (Haskell target_atom "[_]")
   11.13  
   11.14  
   11.15  subsection {* const serializations *}
   11.16 @@ -261,46 +261,57 @@
   11.17    "ExecutableSet.insertl" "List.insertl"
   11.18    "ExecutableSet.drop_first" "List.drop_first"
   11.19  
   11.20 -code_generate (ml, haskell) 
   11.21 +code_gen
   11.22    insertl unionl intersect flip subtract map_distinct
   11.23    unions intersects map_union map_inter Blall Blex
   11.24 +  (SML) (Haskell) 
   11.25  
   11.26 -code_constapp
   11.27 -  "{}"
   11.28 -    ml (target_atom "[]")
   11.29 -    haskell (target_atom "[]")
   11.30 -  insert
   11.31 -    ml ("{*insertl*}")
   11.32 -    haskell ("{*insertl*}")
   11.33 -  "op \<union>"
   11.34 -    ml ("{*unionl*}")
   11.35 -    haskell ("{*unionl*}")
   11.36 -  "op \<inter>"
   11.37 -    ml ("{*intersect*}")
   11.38 -    haskell ("{*intersect*}")
   11.39 -  "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
   11.40 -    ml ("{*flip subtract*}")
   11.41 -    haskell ("{*flip subtract*}")
   11.42 -  image
   11.43 -    ml ("{*map_distinct*}")
   11.44 -    haskell ("{*map_distinct*}")
   11.45 -  "Union"
   11.46 -    ml ("{*unions*}")
   11.47 -    haskell ("{*unions*}")
   11.48 -  "Inter"
   11.49 -    ml ("{*intersects*}")
   11.50 -    haskell ("{*intersects*}")
   11.51 -  UNION
   11.52 -    ml ("{*map_union*}")
   11.53 -    haskell ("{*map_union*}")
   11.54 -  INTER
   11.55 -    ml ("{*map_inter*}")
   11.56 -    haskell ("{*map_inter*}")
   11.57 -  Ball
   11.58 -    ml ("{*Blall*}")
   11.59 -    haskell ("{*Blall*}")
   11.60 -  Bex
   11.61 -    ml ("{*Blex*}")
   11.62 -    haskell ("{*Blex*}")
   11.63 +code_const "{}"
   11.64 +  (SML target_atom "[]")
   11.65 +  (Haskell target_atom "[]")
   11.66 +
   11.67 +code_const insert
   11.68 +  (SML "{*insertl*}")
   11.69 +  (Haskell "{*insertl*}")
   11.70 +
   11.71 +code_const "op \<union>"
   11.72 +  (SML "{*unionl*}")
   11.73 +  (Haskell "{*unionl*}")
   11.74 +
   11.75 +code_const "op \<inter>"
   11.76 +  (SML "{*intersect*}")
   11.77 +  (Haskell "{*intersect*}")
   11.78 +
   11.79 +code_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
   11.80 +  (SML "{*flip subtract*}")
   11.81 +  (Haskell "{*flip subtract*}")
   11.82 +
   11.83 +code_const image
   11.84 +  (SML "{*map_distinct*}")
   11.85 +  (Haskell "{*map_distinct*}")
   11.86 +
   11.87 +code_const "Union"
   11.88 +  (SML "{*unions*}")
   11.89 +  (Haskell "{*unions*}")
   11.90 +
   11.91 +code_const "Inter"
   11.92 +  (SML "{*intersects*}")
   11.93 +  (Haskell "{*intersects*}")
   11.94 +
   11.95 +code_const UNION
   11.96 +  (SML "{*map_union*}")
   11.97 +  (Haskell "{*map_union*}")
   11.98 +
   11.99 +code_const INTER
  11.100 +  (SML "{*map_inter*}")
  11.101 +  (Haskell "{*map_inter*}")
  11.102 +
  11.103 +code_const Ball
  11.104 +  (SML "{*Blall*}")
  11.105 +  (Haskell "{*Blall*}")
  11.106 +
  11.107 +code_const Bex
  11.108 +  (SML "{*Blex*}")
  11.109 +  (Haskell "{*Blex*}")
  11.110  
  11.111  end
    12.1 --- a/src/HOL/Library/MLString.thy	Thu Aug 31 23:01:16 2006 +0200
    12.2 +++ b/src/HOL/Library/MLString.thy	Fri Sep 01 08:36:51 2006 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  header {* Monolithic strings for ML  *}
    12.5  
    12.6  theory MLString
    12.7 -imports Main
    12.8 +imports List
    12.9  begin
   12.10  
   12.11  section {* Monolithic strings for ML *}
   12.12 @@ -58,31 +58,20 @@
   12.13  
   12.14  subsection {* Code serialization *}
   12.15  
   12.16 -code_typapp ml_string
   12.17 -  ml (target_atom "string")
   12.18 -  haskell (target_atom "String")
   12.19 +code_type ml_string
   12.20 +  (SML target_atom "string")
   12.21 +  (Haskell target_atom "String")
   12.22  
   12.23 -code_constapp STR
   12.24 -  haskell ("_")
   12.25 +code_const STR
   12.26 +  (Haskell "_")
   12.27  
   12.28  setup {*
   12.29 -let
   12.30 -  fun print_char c =
   12.31 -    let
   12.32 -      val i = ord c
   12.33 -    in if i < 32
   12.34 -      then prefix "\\" (string_of_int i)
   12.35 -      else c
   12.36 -    end;
   12.37 -  val print_string = quote;
   12.38 -in 
   12.39 -  CodegenPackage.add_pretty_ml_string "ml" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
   12.40 -    print_char print_string "String.implode"
   12.41 -end
   12.42 +  CodegenPackage.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
   12.43 +    HOList.print_char HOList.print_string "String.implode"
   12.44  *}
   12.45  
   12.46 -code_constapp explode
   12.47 -  ml (target_atom "String.explode")
   12.48 -  haskell ("_")
   12.49 +code_const explode
   12.50 +  (SML target_atom "String.explode")
   12.51 +  (Haskell "_")
   12.52  
   12.53 -end
   12.54 \ No newline at end of file
   12.55 +end
    13.1 --- a/src/HOL/List.thy	Thu Aug 31 23:01:16 2006 +0200
    13.2 +++ b/src/HOL/List.thy	Fri Sep 01 08:36:51 2006 +0200
    13.3 @@ -2650,6 +2650,28 @@
    13.4  fun nibble_of_int i =
    13.5    if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
    13.6  
    13.7 +fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
    13.8 +      let
    13.9 +        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
   13.10 +          | dest_nibble _ = raise Match;
   13.11 +      in
   13.12 +        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
   13.13 +        handle Fail _ => NONE | Match => NONE)
   13.14 +      end
   13.15 +  | dest_char _ = NONE;
   13.16 +
   13.17 +val print_list = Pretty.enum "," "[" "]";
   13.18 +
   13.19 +fun print_char c =
   13.20 +  let
   13.21 +    val i = ord c
   13.22 +  in if i < 32
   13.23 +    then prefix "\\" (string_of_int i)
   13.24 +    else c
   13.25 +  end;
   13.26 +
   13.27 +val print_string = quote;
   13.28 +
   13.29  fun term_string s =
   13.30    let
   13.31      val ty_n = Type ("List.nibble", []);
   13.32 @@ -2693,61 +2715,9 @@
   13.33    in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
   13.34  *}
   13.35  
   13.36 +
   13.37  subsubsection {* Code generator setup *}
   13.38  
   13.39 -ML {*
   13.40 -local
   13.41 -
   13.42 -fun list_codegen thy defs gr dep thyname b t =
   13.43 -  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
   13.44 -    (gr, HOLogic.dest_list t)
   13.45 -  in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
   13.46 -
   13.47 -fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
   13.48 -      let
   13.49 -        fun dest_nibble (Const (s, _)) = (HOList.int_of_nibble o unprefix "List.nibble.Nibble") s
   13.50 -          | dest_nibble _ = raise Match;
   13.51 -      in
   13.52 -        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
   13.53 -        handle Fail _ => NONE | Match => NONE)
   13.54 -      end
   13.55 -  | dest_char _ = NONE;
   13.56 -
   13.57 -fun char_codegen thy defs gr dep thyname b t =
   13.58 -  case (Option.map chr o dest_char) t 
   13.59 -   of SOME c =>
   13.60 -        if Symbol.is_printable c
   13.61 -        then SOME (gr, (Pretty.quote o Pretty.str) c)
   13.62 -        else NONE
   13.63 -    | NONE => NONE;
   13.64 -
   13.65 -val print_list = Pretty.enum "," "[" "]";
   13.66 -
   13.67 -fun print_char c =
   13.68 -  let
   13.69 -    val i = ord c
   13.70 -  in if i < 32
   13.71 -    then prefix "\\" (string_of_int i)
   13.72 -    else c
   13.73 -  end;
   13.74 -
   13.75 -val print_string = quote;
   13.76 -
   13.77 -in
   13.78 -
   13.79 -val list_codegen_setup =
   13.80 -  Codegen.add_codegen "list_codegen" list_codegen
   13.81 -  #> Codegen.add_codegen "char_codegen" char_codegen
   13.82 -  #> CodegenPackage.add_pretty_list "ml" "List.list.Nil" "List.list.Cons"
   13.83 -       print_list NONE (7, "::")
   13.84 -  #> CodegenPackage.add_pretty_list "haskell" "List.list.Nil" "List.list.Cons"
   13.85 -       print_list (SOME (print_char, print_string)) (5, ":")
   13.86 -  #> CodegenPackage.add_appconst
   13.87 -       ("List.char.Char", CodegenPackage.appgen_char dest_char);
   13.88 -
   13.89 -end;
   13.90 -*}
   13.91 -
   13.92  types_code
   13.93    "list" ("_ list")
   13.94  attach (term_of) {*
   13.95 @@ -2773,26 +2743,50 @@
   13.96  
   13.97  consts_code "Cons" ("(_ ::/ _)")
   13.98  
   13.99 -code_typapp
  13.100 -  list
  13.101 -    ml ("_ list")
  13.102 -    haskell (target_atom "[_]")
  13.103 -
  13.104 -code_constapp
  13.105 -  Nil
  13.106 -    ml (target_atom "[]")
  13.107 -    haskell (target_atom "[]")
  13.108 -
  13.109 -code_typapp
  13.110 -  char
  13.111 -    ml (target_atom "char")
  13.112 -    haskell (target_atom "Char")
  13.113 -
  13.114 -code_constapp
  13.115 -  Char
  13.116 -    ml (target_atom "(__,/ __)")
  13.117 -    haskell (target_atom "(__,/ __)")
  13.118 -
  13.119 -setup list_codegen_setup
  13.120 +code_type list
  13.121 +  (SML "_ list")
  13.122 +  (Haskell target_atom "[_]")
  13.123 +
  13.124 +code_const Nil
  13.125 +  (SML target_atom "[]")
  13.126 +  (Haskell target_atom "[]")
  13.127 +
  13.128 +code_type char
  13.129 +  (SML target_atom "char")
  13.130 +  (Haskell target_atom "Char")
  13.131 +
  13.132 +code_const Char
  13.133 +  (SML target_atom "(__,/ __)")
  13.134 +  (Haskell target_atom "(__,/ __)")
  13.135 +
  13.136 +setup {*
  13.137 +let
  13.138 +
  13.139 +fun list_codegen thy defs gr dep thyname b t =
  13.140 +  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
  13.141 +    (gr, HOLogic.dest_list t)
  13.142 +  in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
  13.143 +
  13.144 +fun char_codegen thy defs gr dep thyname b t =
  13.145 +  case (Option.map chr o HOList.dest_char) t 
  13.146 +   of SOME c =>
  13.147 +        if Symbol.is_printable c
  13.148 +        then SOME (gr, (Pretty.quote o Pretty.str) c)
  13.149 +        else NONE
  13.150 +    | NONE => NONE;
  13.151 +
  13.152 +in
  13.153 +
  13.154 +  Codegen.add_codegen "list_codegen" list_codegen
  13.155 +  #> Codegen.add_codegen "char_codegen" char_codegen
  13.156 +  #> CodegenPackage.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
  13.157 +       HOList.print_list NONE (7, "::")
  13.158 +  #> CodegenPackage.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
  13.159 +       HOList.print_list (SOME (HOList.print_char, HOList.print_string)) (5, ":")
  13.160 +  #> CodegenPackage.add_appconst
  13.161 +       ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char)
  13.162 +
  13.163 +end;
  13.164 +*}
  13.165  
  13.166  end
    14.1 --- a/src/HOL/Wellfounded_Recursion.thy	Thu Aug 31 23:01:16 2006 +0200
    14.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Fri Sep 01 08:36:51 2006 +0200
    14.3 @@ -295,10 +295,9 @@
    14.4    CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
    14.5  *}
    14.6  
    14.7 -code_constapp
    14.8 -  wfrec
    14.9 -    ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
   14.10 -    haskell (target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
   14.11 +code_const wfrec
   14.12 +  (SML target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
   14.13 +  (Haskell target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
   14.14  
   14.15  subsection{*Variants for TFL: the Recdef Package*}
   14.16  
    15.1 --- a/src/HOL/ex/Classpackage.thy	Thu Aug 31 23:01:16 2006 +0200
    15.2 +++ b/src/HOL/ex/Classpackage.thy	Fri Sep 01 08:36:51 2006 +0200
    15.3 @@ -319,10 +319,10 @@
    15.4    "x2 = X (1::int) 2 3"
    15.5    "y2 = Y (1::int) 2 3"
    15.6  
    15.7 -code_generate "op \<otimes>" \<one> inv
    15.8 -code_generate (ml, haskell) X Y
    15.9 -code_generate (ml, haskell) x1 x2 y2
   15.10 +code_gen "op \<otimes>" \<one> inv
   15.11 +code_gen X Y (SML) (Haskell)
   15.12 +code_gen x1 x2 y2 (SML) (Haskell)
   15.13  
   15.14 -code_serialize ml (-)
   15.15 +code_gen (SML -)
   15.16  
   15.17  end
    16.1 --- a/src/HOL/ex/CodeCollections.thy	Thu Aug 31 23:01:16 2006 +0200
    16.2 +++ b/src/HOL/ex/CodeCollections.thy	Fri Sep 01 08:36:51 2006 +0200
    16.3 @@ -402,16 +402,16 @@
    16.4    "test1 = sum [None, Some True, None, Some False]"
    16.5    "test2 = (inf :: nat \<times> unit)"
    16.6  
    16.7 -code_generate eq
    16.8 -code_generate "op <<="
    16.9 -code_generate "op <<"
   16.10 -code_generate inf
   16.11 -code_generate between
   16.12 -code_generate index
   16.13 -code_generate sum
   16.14 -code_generate test1
   16.15 -code_generate test2
   16.16 +code_gen eq
   16.17 +code_gen "op <<="
   16.18 +code_gen "op <<"
   16.19 +code_gen inf
   16.20 +code_gen between
   16.21 +code_gen index
   16.22 +code_gen sum
   16.23 +code_gen test1
   16.24 +code_gen test2
   16.25  
   16.26 -code_serialize ml (-)
   16.27 +code_gen (SML -)
   16.28  
   16.29  end
   16.30 \ No newline at end of file
    17.1 --- a/src/HOL/ex/CodeEmbed.thy	Thu Aug 31 23:01:16 2006 +0200
    17.2 +++ b/src/HOL/ex/CodeEmbed.thy	Fri Sep 01 08:36:51 2006 +0200
    17.3 @@ -77,15 +77,12 @@
    17.4  
    17.5  subsection {* Code serialization setup *}
    17.6  
    17.7 -code_typapp
    17.8 -  "typ"  ml (target_atom "Term.typ")
    17.9 -  "term" ml (target_atom "Term.term")
   17.10 +code_type "typ" and "term"
   17.11 +  (SML target_atom "Term.typ" and target_atom "Term.term")
   17.12  
   17.13 -code_constapp
   17.14 -  Type  ml ("Term.Type (_, _)")
   17.15 -  TFix  ml ("Term.TFree (_, _)")
   17.16 -  Const ml ("Term.Const (_, _)")
   17.17 -  App   ml ("Term.$ (_, _)")
   17.18 -  Fix   ml ("Term.Free (_, _)")
   17.19 +code_const Type and TFix
   17.20 +  and Const and App and Fix
   17.21 +  (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
   17.22 +    and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
   17.23  
   17.24  end
   17.25 \ No newline at end of file
    18.1 --- a/src/HOL/ex/CodeEval.thy	Thu Aug 31 23:01:16 2006 +0200
    18.2 +++ b/src/HOL/ex/CodeEval.thy	Fri Sep 01 08:36:51 2006 +0200
    18.3 @@ -194,7 +194,7 @@
    18.4  and ('a, 'b) cair =
    18.5      Cair 'a 'b
    18.6  
    18.7 -code_generate term_of
    18.8 +code_gen term_of
    18.9  
   18.10  ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
   18.11  
    19.1 --- a/src/HOL/ex/CodeOperationalEquality.thy	Thu Aug 31 23:01:16 2006 +0200
    19.2 +++ b/src/HOL/ex/CodeOperationalEquality.thy	Fri Sep 01 08:36:51 2006 +0200
    19.3 @@ -117,9 +117,9 @@
    19.4    "eq k l = eq_integer k l"
    19.5  unfolding eq_integer_def eq_def ..
    19.6  
    19.7 -code_constapp eq_integer
    19.8 -  ml (infixl 6 "=")
    19.9 -  haskell (infixl 4 "==")
   19.10 +code_const eq_integer
   19.11 +  (SML infixl 6 "=")
   19.12 +  (Haskell infixl 4 "==")
   19.13  
   19.14  
   19.15  subsection {* codegenerator setup *}
   19.16 @@ -134,33 +134,34 @@
   19.17  subsection {* haskell setup *}
   19.18  
   19.19  code_class eq
   19.20 -  haskell "Eq" (eq "(==)")
   19.21 +  (Haskell "Eq" where eq \<equiv> "(==)")
   19.22 +
   19.23 +code_instance eq :: bool and eq :: unit and eq :: *
   19.24 +  and eq :: option and eq :: list and eq :: char and eq :: int
   19.25 +  (Haskell - and - and - and - and - and - and -)
   19.26  
   19.27 -code_instance
   19.28 -  (eq :: bool) haskell
   19.29 -  (eq :: unit) haskell
   19.30 -  (eq :: *) haskell
   19.31 -  (eq :: option) haskell
   19.32 -  (eq :: list) haskell
   19.33 -  (eq :: char) haskell
   19.34 -  (eq :: int) haskell
   19.35 +code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   19.36 +  (Haskell infixl 4 "==")
   19.37 +
   19.38 +code_const "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   19.39 +  (Haskell infixl 4 "==")
   19.40 +
   19.41 +code_const "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   19.42 +  (Haskell infixl 4 "==")
   19.43  
   19.44 -code_constapp
   19.45 -  "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   19.46 -    haskell (infixl 4 "==")
   19.47 -  "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   19.48 -    haskell (infixl 4 "==")
   19.49 -  "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   19.50 -    haskell (infixl 4 "==")
   19.51 -  "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   19.52 -    haskell (infixl 4 "==")
   19.53 -  "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   19.54 -    haskell (infixl 4 "==")
   19.55 -  "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   19.56 -    haskell (infixl 4 "==")
   19.57 -  "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   19.58 -    haskell (infixl 4 "==")
   19.59 -  "eq"
   19.60 -    haskell (infixl 4 "==")
   19.61 +code_const "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   19.62 +  (Haskell infixl 4 "==")
   19.63 +
   19.64 +code_const "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   19.65 +  (Haskell infixl 4 "==")
   19.66 +
   19.67 +code_const "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   19.68 +  (Haskell infixl 4 "==")
   19.69 +
   19.70 +code_const "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   19.71 +  (Haskell infixl 4 "==")
   19.72 +
   19.73 +code_const "eq"
   19.74 +  (Haskell infixl 4 "==")
   19.75  
   19.76  end
   19.77 \ No newline at end of file
    20.1 --- a/src/HOL/ex/CodeRandom.thy	Thu Aug 31 23:01:16 2006 +0200
    20.2 +++ b/src/HOL/ex/CodeRandom.thy	Fri Sep 01 08:36:51 2006 +0200
    20.3 @@ -167,12 +167,13 @@
    20.4  end;
    20.5  *}
    20.6  
    20.7 -code_typapp randseed
    20.8 -  ml (target_atom "Random.seed")
    20.9 +code_type randseed
   20.10 +  (SML target_atom "Random.seed")
   20.11  
   20.12 -code_constapp random_int
   20.13 -  ml (target_atom "Random.value")
   20.14 +code_const random_int
   20.15 +  (SML target_atom "Random.value")
   20.16  
   20.17 -code_serialize ml select select_weight (-)
   20.18 +code_gen select select_weight
   20.19 +  (SML -)
   20.20  
   20.21  end
   20.22 \ No newline at end of file
    21.1 --- a/src/HOL/ex/Codegenerator.thy	Thu Aug 31 23:01:16 2006 +0200
    21.2 +++ b/src/HOL/ex/Codegenerator.thy	Fri Sep 01 08:36:51 2006 +0200
    21.3 @@ -90,21 +90,19 @@
    21.4    g "Mymod.A.f"
    21.5    h "Mymod.A.B.f"
    21.6  
    21.7 -code_generate (ml, haskell)
    21.8 -  n one "0::int" "0::nat" "1::int" "1::nat"
    21.9 -code_generate (ml, haskell)
   21.10 -  fac
   21.11 -code_generate
   21.12 -  xor
   21.13 -code_generate
   21.14 +code_gen xor
   21.15 +code_gen one "0::nat" "1::nat"
   21.16 +code_gen "0::int" "1::int" n fac
   21.17 +  (SML) (Haskell)
   21.18 +code_gen
   21.19    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   21.20    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   21.21    "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   21.22    "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   21.23    "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   21.24 -code_generate
   21.25 +code_gen
   21.26    Pair fst snd Let split swap swapp appl
   21.27 -code_generate (ml, haskell)
   21.28 +code_gen
   21.29    k
   21.30    "op + :: int \<Rightarrow> int \<Rightarrow> int"
   21.31    "op - :: int \<Rightarrow> int \<Rightarrow> int"
   21.32 @@ -114,15 +112,16 @@
   21.33    fac
   21.34    "op div :: int \<Rightarrow> int \<Rightarrow> int"
   21.35    "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   21.36 -code_generate
   21.37 +  (SML) (Haskell)
   21.38 +code_gen
   21.39    Inl Inr
   21.40 -code_generate
   21.41 +code_gen
   21.42    None Some
   21.43 -code_generate
   21.44 +code_gen
   21.45    hd tl "op @" ps qs
   21.46 -code_generate
   21.47 +code_gen
   21.48    mut1 mut2
   21.49 -code_generate (ml, haskell)
   21.50 +code_gen
   21.51    "op @" filter concat foldl foldr hd tl
   21.52    last butlast list_all2
   21.53    map 
   21.54 @@ -143,9 +142,10 @@
   21.55    rotate1
   21.56    rotate
   21.57    splice
   21.58 -code_generate
   21.59 +  (SML) (Haskell)
   21.60 +code_gen
   21.61    foo1 foo3
   21.62 -code_generate (ml, haskell)
   21.63 +code_gen
   21.64    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   21.65    "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   21.66    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   21.67 @@ -156,9 +156,9 @@
   21.68    "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   21.69    "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   21.70    "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   21.71 -code_generate
   21.72 +code_gen
   21.73    f g h
   21.74  
   21.75 -code_serialize ml (-)
   21.76 +code_gen (SML -)
   21.77  
   21.78  end
   21.79 \ No newline at end of file