migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
authorhaftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 524356646bb548c6b
parent 52434 cbb94074682b
child 52436 c54e551de6f9
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
NEWS
src/Doc/IsarRef/HOL_Specific.thy
src/HOL/Code_Evaluation.thy
src/HOL/Code_Numeral.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Fields.thy
src/HOL/Fun.thy
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Int.thy
src/HOL/Library/Code_Binary_Nat.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Code_Target_Nat.thy
src/HOL/Library/Debug.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Parallel.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/Nat.thy
src/HOL/Num.thy
src/HOL/Option.thy
src/HOL/Power.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quickcheck_Random.thy
src/HOL/Rings.thy
src/HOL/Semiring_Normalization.thy
src/HOL/String.thy
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/HOL/Typerep.thy
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Sun Jun 23 21:16:06 2013 +0200
     1.2 +++ b/NEWS	Sun Jun 23 21:16:07 2013 +0200
     1.3 @@ -68,6 +68,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Code generator:
     1.8 +  * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
     1.9 +  * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
    1.10 +    subsuming 'code_modulename'.
    1.11 +  See the Isar reference manual for syntax diagrams, and the HOL theories for examples.
    1.12 +
    1.13  * Library/Polynomial.thy:
    1.14    * Use lifting for primitive definitions.
    1.15    * Explicit conversions from and to lists of coefficients, used for generated code.
     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Jun 23 21:16:06 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Jun 23 21:16:07 2013 +0200
     2.3 @@ -2224,7 +2224,7 @@
     2.4    @{rail "
     2.5      @@{command (HOL) export_code} ( constexpr + ) \\
     2.6         ( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
     2.7 -        ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     2.8 +        ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
     2.9      ;
    2.10  
    2.11      const: @{syntax term}
     3.1 --- a/src/HOL/Code_Evaluation.thy	Sun Jun 23 21:16:06 2013 +0200
     3.2 +++ b/src/HOL/Code_Evaluation.thy	Sun Jun 23 21:16:07 2013 +0200
     3.3 @@ -125,18 +125,14 @@
     3.4        (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
     3.5    by (subst term_of_anything) rule 
     3.6  
     3.7 -code_type "term"
     3.8 -  (Eval "Term.term")
     3.9 -
    3.10 -code_const Const and App and Abs and Free
    3.11 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
    3.12 -     and "Term.Free/ ((_), (_))")
    3.13 -
    3.14 -code_const "term_of \<Colon> integer \<Rightarrow> term"
    3.15 -  (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
    3.16 -  
    3.17 -code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    3.18 -  (Eval "HOLogic.mk'_literal")
    3.19 +code_printing
    3.20 +  type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
    3.21 +| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
    3.22 +| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
    3.23 +| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
    3.24 +| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
    3.25 +| constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
    3.26 +| constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
    3.27  
    3.28  code_reserved Eval HOLogic
    3.29  
    3.30 @@ -161,8 +157,8 @@
    3.31  definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
    3.32    [code del]: "tracing s x = x"
    3.33  
    3.34 -code_const "tracing :: String.literal => 'a => 'a"
    3.35 -  (Eval "Code'_Evaluation.tracing")
    3.36 +code_printing
    3.37 +  constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
    3.38  
    3.39  
    3.40  subsection {* Generic reification *}
     4.1 --- a/src/HOL/Code_Numeral.thy	Sun Jun 23 21:16:06 2013 +0200
     4.2 +++ b/src/HOL/Code_Numeral.thy	Sun Jun 23 21:16:07 2013 +0200
     4.3 @@ -519,21 +519,22 @@
     4.4  
     4.5  code_reserved Eval int Integer abs
     4.6  
     4.7 -code_type integer
     4.8 -  (SML "IntInf.int")
     4.9 -  (OCaml "Big'_int.big'_int")
    4.10 -  (Haskell "Integer")
    4.11 -  (Scala "BigInt")
    4.12 -  (Eval "int")
    4.13 +code_printing
    4.14 +  type_constructor integer \<rightharpoonup>
    4.15 +    (SML) "IntInf.int"
    4.16 +    and (OCaml) "Big'_int.big'_int"
    4.17 +    and (Haskell) "Integer"
    4.18 +    and (Scala) "BigInt"
    4.19 +    and (Eval) "int"
    4.20 +| class_instance integer :: equal \<rightharpoonup>
    4.21 +    (Haskell) -
    4.22  
    4.23 -code_instance integer :: equal
    4.24 -  (Haskell -)
    4.25 -
    4.26 -code_const "0::integer"
    4.27 -  (SML "0")
    4.28 -  (OCaml "Big'_int.zero'_big'_int")
    4.29 -  (Haskell "0")
    4.30 -  (Scala "BigInt(0)")
    4.31 +code_printing
    4.32 +  constant "0::integer" \<rightharpoonup>
    4.33 +    (SML) "0"
    4.34 +    and (OCaml) "Big'_int.zero'_big'_int"
    4.35 +    and (Haskell) "0"
    4.36 +    and (Scala) "BigInt(0)"
    4.37  
    4.38  setup {*
    4.39    fold (Numeral.add_code @{const_name Code_Numeral.Pos}
    4.40 @@ -545,83 +546,69 @@
    4.41      true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
    4.42  *}
    4.43  
    4.44 -code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _"
    4.45 -  (SML "IntInf.+ ((_), (_))")
    4.46 -  (OCaml "Big'_int.add'_big'_int")
    4.47 -  (Haskell infixl 6 "+")
    4.48 -  (Scala infixl 7 "+")
    4.49 -  (Eval infixl 8 "+")
    4.50 -
    4.51 -code_const "uminus :: integer \<Rightarrow> _"
    4.52 -  (SML "IntInf.~")
    4.53 -  (OCaml "Big'_int.minus'_big'_int")
    4.54 -  (Haskell "negate")
    4.55 -  (Scala "!(- _)")
    4.56 -  (Eval "~/ _")
    4.57 -
    4.58 -code_const "minus :: integer \<Rightarrow> _"
    4.59 -  (SML "IntInf.- ((_), (_))")
    4.60 -  (OCaml "Big'_int.sub'_big'_int")
    4.61 -  (Haskell infixl 6 "-")
    4.62 -  (Scala infixl 7 "-")
    4.63 -  (Eval infixl 8 "-")
    4.64 -
    4.65 -code_const Code_Numeral.dup
    4.66 -  (SML "IntInf.*/ (2,/ (_))")
    4.67 -  (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
    4.68 -  (Haskell "!(2 * _)")
    4.69 -  (Scala "!(2 * _)")
    4.70 -  (Eval "!(2 * _)")
    4.71 -
    4.72 -code_const Code_Numeral.sub
    4.73 -  (SML "!(raise/ Fail/ \"sub\")")
    4.74 -  (OCaml "failwith/ \"sub\"")
    4.75 -  (Haskell "error/ \"sub\"")
    4.76 -  (Scala "!sys.error(\"sub\")")
    4.77 +code_printing
    4.78 +  constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
    4.79 +    (SML) "IntInf.+ ((_), (_))"
    4.80 +    and (OCaml) "Big'_int.add'_big'_int"
    4.81 +    and (Haskell) infixl 6 "+"
    4.82 +    and (Scala) infixl 7 "+"
    4.83 +    and (Eval) infixl 8 "+"
    4.84 +| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
    4.85 +    (SML) "IntInf.~"
    4.86 +    and (OCaml) "Big'_int.minus'_big'_int"
    4.87 +    and (Haskell) "negate"
    4.88 +    and (Scala) "!(- _)"
    4.89 +    and (Eval) "~/ _"
    4.90 +| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
    4.91 +    (SML) "IntInf.- ((_), (_))"
    4.92 +    and (OCaml) "Big'_int.sub'_big'_int"
    4.93 +    and (Haskell) infixl 6 "-"
    4.94 +    and (Scala) infixl 7 "-"
    4.95 +    and (Eval) infixl 8 "-"
    4.96 +| constant Code_Numeral.dup \<rightharpoonup>
    4.97 +    (SML) "IntInf.*/ (2,/ (_))"
    4.98 +    and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
    4.99 +    and (Haskell) "!(2 * _)"
   4.100 +    and (Scala) "!(2 * _)"
   4.101 +    and (Eval) "!(2 * _)"
   4.102 +| constant Code_Numeral.sub \<rightharpoonup>
   4.103 +    (SML) "!(raise/ Fail/ \"sub\")"
   4.104 +    and (OCaml) "failwith/ \"sub\""
   4.105 +    and (Haskell) "error/ \"sub\""
   4.106 +    and (Scala) "!sys.error(\"sub\")"
   4.107 +| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
   4.108 +    (SML) "IntInf.* ((_), (_))"
   4.109 +    and (OCaml) "Big'_int.mult'_big'_int"
   4.110 +    and (Haskell) infixl 7 "*"
   4.111 +    and (Scala) infixl 8 "*"
   4.112 +    and (Eval) infixl 9 "*"
   4.113 +| constant Code_Numeral.divmod_abs \<rightharpoonup>
   4.114 +    (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
   4.115 +    and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
   4.116 +    and (Haskell) "divMod/ (abs _)/ (abs _)"
   4.117 +    and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
   4.118 +    and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
   4.119 +| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   4.120 +    (SML) "!((_ : IntInf.int) = _)"
   4.121 +    and (OCaml) "Big'_int.eq'_big'_int"
   4.122 +    and (Haskell) infix 4 "=="
   4.123 +    and (Scala) infixl 5 "=="
   4.124 +    and (Eval) infixl 6 "="
   4.125 +| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   4.126 +    (SML) "IntInf.<= ((_), (_))"
   4.127 +    and (OCaml) "Big'_int.le'_big'_int"
   4.128 +    and (Haskell) infix 4 "<="
   4.129 +    and (Scala) infixl 4 "<="
   4.130 +    and (Eval) infixl 6 "<="
   4.131 +| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
   4.132 +    (SML) "IntInf.< ((_), (_))"
   4.133 +    and (OCaml) "Big'_int.lt'_big'_int"
   4.134 +    and (Haskell) infix 4 "<"
   4.135 +    and (Scala) infixl 4 "<"
   4.136 +    and (Eval) infixl 6 "<"
   4.137  
   4.138 -code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _"
   4.139 -  (SML "IntInf.* ((_), (_))")
   4.140 -  (OCaml "Big'_int.mult'_big'_int")
   4.141 -  (Haskell infixl 7 "*")
   4.142 -  (Scala infixl 8 "*")
   4.143 -  (Eval infixl 9 "*")
   4.144 -
   4.145 -code_const Code_Numeral.divmod_abs
   4.146 -  (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
   4.147 -  (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
   4.148 -  (Haskell "divMod/ (abs _)/ (abs _)")
   4.149 -  (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   4.150 -  (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
   4.151 -
   4.152 -code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool"
   4.153 -  (SML "!((_ : IntInf.int) = _)")
   4.154 -  (OCaml "Big'_int.eq'_big'_int")
   4.155 -  (Haskell infix 4 "==")
   4.156 -  (Scala infixl 5 "==")
   4.157 -  (Eval infixl 6 "=")
   4.158 -
   4.159 -code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool"
   4.160 -  (SML "IntInf.<= ((_), (_))")
   4.161 -  (OCaml "Big'_int.le'_big'_int")
   4.162 -  (Haskell infix 4 "<=")
   4.163 -  (Scala infixl 4 "<=")
   4.164 -  (Eval infixl 6 "<=")
   4.165 -
   4.166 -code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool"
   4.167 -  (SML "IntInf.< ((_), (_))")
   4.168 -  (OCaml "Big'_int.lt'_big'_int")
   4.169 -  (Haskell infix 4 "<")
   4.170 -  (Scala infixl 4 "<")
   4.171 -  (Eval infixl 6 "<")
   4.172 -
   4.173 -code_modulename SML
   4.174 -  Code_Numeral Arith
   4.175 -
   4.176 -code_modulename OCaml
   4.177 -  Code_Numeral Arith
   4.178 -
   4.179 -code_modulename Haskell
   4.180 -  Code_Numeral Arith
   4.181 +code_identifier
   4.182 +  code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   4.183  
   4.184  
   4.185  subsection {* Type of target language naturals *}
     5.1 --- a/src/HOL/Divides.thy	Sun Jun 23 21:16:06 2013 +0200
     5.2 +++ b/src/HOL/Divides.thy	Sun Jun 23 21:16:07 2013 +0200
     5.3 @@ -2381,13 +2381,8 @@
     5.4    then show ?thesis by (simp add: divmod_int_pdivmod)
     5.5  qed
     5.6  
     5.7 -code_modulename SML
     5.8 -  Divides Arith
     5.9 -
    5.10 -code_modulename OCaml
    5.11 -  Divides Arith
    5.12 -
    5.13 -code_modulename Haskell
    5.14 -  Divides Arith
    5.15 +code_identifier
    5.16 +  code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    5.17  
    5.18  end
    5.19 +
     6.1 --- a/src/HOL/Enum.thy	Sun Jun 23 21:16:06 2013 +0200
     6.2 +++ b/src/HOL/Enum.thy	Sun Jun 23 21:16:07 2013 +0200
     6.3 @@ -117,7 +117,9 @@
     6.4  qed
     6.5  
     6.6  code_abort enum_the
     6.7 -code_const enum_the (Eval "(fn p => raise Match)")
     6.8 +
     6.9 +code_printing
    6.10 +  constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"
    6.11  
    6.12  
    6.13  subsubsection {* Equality and order on functions *}
     7.1 --- a/src/HOL/Fields.thy	Sun Jun 23 21:16:06 2013 +0200
     7.2 +++ b/src/HOL/Fields.thy	Sun Jun 23 21:16:07 2013 +0200
     7.3 @@ -1176,13 +1176,7 @@
     7.4  
     7.5  end
     7.6  
     7.7 -code_modulename SML
     7.8 -  Fields Arith
     7.9 -
    7.10 -code_modulename OCaml
    7.11 -  Fields Arith
    7.12 -
    7.13 -code_modulename Haskell
    7.14 -  Fields Arith
    7.15 +code_identifier
    7.16 +  code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    7.17  
    7.18  end
     8.1 --- a/src/HOL/Fun.thy	Sun Jun 23 21:16:06 2013 +0200
     8.2 +++ b/src/HOL/Fun.thy	Sun Jun 23 21:16:07 2013 +0200
     8.3 @@ -29,6 +29,9 @@
     8.4  lemma vimage_id [simp]: "vimage id = id"
     8.5    by (simp add: id_def fun_eq_iff)
     8.6  
     8.7 +code_printing
     8.8 +  constant id \<rightharpoonup> (Haskell) "id"
     8.9 +
    8.10  
    8.11  subsection {* The Composition Operator @{text "f \<circ> g"} *}
    8.12  
    8.13 @@ -77,6 +80,9 @@
    8.14    "SUPR A (g \<circ> f) = SUPR (f ` A) g"
    8.15    by (simp add: SUP_def image_comp)
    8.16  
    8.17 +code_printing
    8.18 +  constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
    8.19 +
    8.20  
    8.21  subsection {* The Forward Composition Operator @{text fcomp} *}
    8.22  
    8.23 @@ -95,8 +101,8 @@
    8.24  lemma fcomp_id [simp]: "f \<circ>> id = f"
    8.25    by (simp add: fcomp_def)
    8.26  
    8.27 -code_const fcomp
    8.28 -  (Eval infixl 1 "#>")
    8.29 +code_printing
    8.30 +  constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
    8.31  
    8.32  no_notation fcomp (infixl "\<circ>>" 60)
    8.33  
    8.34 @@ -814,16 +820,6 @@
    8.35  *}
    8.36  
    8.37  
    8.38 -subsubsection {* Code generator *}
    8.39 -
    8.40 -code_const "op \<circ>"
    8.41 -  (SML infixl 5 "o")
    8.42 -  (Haskell infixr 9 ".")
    8.43 -
    8.44 -code_const "id"
    8.45 -  (Haskell "id")
    8.46 -
    8.47 -
    8.48  subsubsection {* Functorial structure of types *}
    8.49  
    8.50  ML_file "Tools/enriched_type.ML"
     9.1 --- a/src/HOL/Groups.thy	Sun Jun 23 21:16:06 2013 +0200
     9.2 +++ b/src/HOL/Groups.thy	Sun Jun 23 21:16:07 2013 +0200
     9.3 @@ -1359,14 +1359,8 @@
     9.4  by (auto intro: add_strict_right_mono add_strict_left_mono
     9.5    add_less_le_mono add_le_less_mono add_strict_mono)
     9.6  
     9.7 -code_modulename SML
     9.8 -  Groups Arith
     9.9 -
    9.10 -code_modulename OCaml
    9.11 -  Groups Arith
    9.12 -
    9.13 -code_modulename Haskell
    9.14 -  Groups Arith
    9.15 +code_identifier
    9.16 +  code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
    9.17  
    9.18  
    9.19  text {* Legacy *}
    10.1 --- a/src/HOL/HOL.thy	Sun Jun 23 21:16:06 2013 +0200
    10.2 +++ b/src/HOL/HOL.thy	Sun Jun 23 21:16:07 2013 +0200
    10.3 @@ -1830,61 +1830,67 @@
    10.4  
    10.5  text {* type @{typ bool} *}
    10.6  
    10.7 -code_type bool
    10.8 -  (SML "bool")
    10.9 -  (OCaml "bool")
   10.10 -  (Haskell "Bool")
   10.11 -  (Scala "Boolean")
   10.12 -
   10.13 -code_const True and False and Not and HOL.conj and HOL.disj and HOL.implies and If 
   10.14 -  (SML "true" and "false" and "not"
   10.15 -    and infixl 1 "andalso" and infixl 0 "orelse"
   10.16 -    and "!(if (_)/ then (_)/ else true)"
   10.17 -    and "!(if (_)/ then (_)/ else (_))")
   10.18 -  (OCaml "true" and "false" and "not"
   10.19 -    and infixl 3 "&&" and infixl 2 "||"
   10.20 -    and "!(if (_)/ then (_)/ else true)"
   10.21 -    and "!(if (_)/ then (_)/ else (_))")
   10.22 -  (Haskell "True" and "False" and "not"
   10.23 -    and infixr 3 "&&" and infixr 2 "||"
   10.24 -    and "!(if (_)/ then (_)/ else True)"
   10.25 -    and "!(if (_)/ then (_)/ else (_))")
   10.26 -  (Scala "true" and "false" and "'! _"
   10.27 -    and infixl 3 "&&" and infixl 1 "||"
   10.28 -    and "!(if ((_))/ (_)/ else true)"
   10.29 -    and "!(if ((_))/ (_)/ else (_))")
   10.30 +code_printing
   10.31 +  type_constructor bool \<rightharpoonup>
   10.32 +    (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
   10.33 +| constant True \<rightharpoonup>
   10.34 +    (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
   10.35 +| constant False \<rightharpoonup>
   10.36 +    (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false" 
   10.37  
   10.38  code_reserved SML
   10.39 -  bool true false not
   10.40 +  bool true false
   10.41  
   10.42  code_reserved OCaml
   10.43 -  bool not
   10.44 +  bool
   10.45  
   10.46  code_reserved Scala
   10.47    Boolean
   10.48  
   10.49 -code_modulename SML Pure HOL
   10.50 -code_modulename OCaml Pure HOL
   10.51 -code_modulename Haskell Pure HOL
   10.52 +code_printing
   10.53 +  constant Not \<rightharpoonup>
   10.54 +    (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
   10.55 +| constant HOL.conj \<rightharpoonup>
   10.56 +    (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
   10.57 +| constant HOL.disj \<rightharpoonup>
   10.58 +    (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
   10.59 +| constant HOL.implies \<rightharpoonup>
   10.60 +    (SML) "!(if (_)/ then (_)/ else true)"
   10.61 +    and (OCaml) "!(if (_)/ then (_)/ else true)"
   10.62 +    and (Haskell) "!(if (_)/ then (_)/ else True)"
   10.63 +    and (Scala) "!(if ((_))/ (_)/ else true)"
   10.64 +| constant If \<rightharpoonup>
   10.65 +    (SML) "!(if (_)/ then (_)/ else (_))"
   10.66 +    and (OCaml) "!(if (_)/ then (_)/ else (_))"
   10.67 +    and (Haskell) "!(if (_)/ then (_)/ else (_))"
   10.68 +    and (Scala) "!(if ((_))/ (_)/ else (_))"
   10.69 +
   10.70 +code_reserved SML
   10.71 +  not
   10.72 +
   10.73 +code_reserved OCaml
   10.74 +  not
   10.75 +
   10.76 +code_identifier
   10.77 +  code_module Pure \<rightharpoonup>
   10.78 +    (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
   10.79  
   10.80  text {* using built-in Haskell equality *}
   10.81  
   10.82 -code_class equal
   10.83 -  (Haskell "Eq")
   10.84 -
   10.85 -code_const "HOL.equal"
   10.86 -  (Haskell infix 4 "==")
   10.87 -
   10.88 -code_const HOL.eq
   10.89 -  (Haskell infix 4 "==")
   10.90 +code_printing
   10.91 +  type_class equal \<rightharpoonup> (Haskell) "Eq"
   10.92 +| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
   10.93 +| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
   10.94  
   10.95  text {* undefined *}
   10.96  
   10.97 -code_const undefined
   10.98 -  (SML "!(raise/ Fail/ \"undefined\")")
   10.99 -  (OCaml "failwith/ \"undefined\"")
  10.100 -  (Haskell "error/ \"undefined\"")
  10.101 -  (Scala "!sys.error(\"undefined\")")
  10.102 +code_printing
  10.103 +  constant undefined \<rightharpoonup>
  10.104 +    (SML) "!(raise/ Fail/ \"undefined\")"
  10.105 +    and (OCaml) "failwith/ \"undefined\""
  10.106 +    and (Haskell) "error/ \"undefined\""
  10.107 +    and (Scala) "!sys.error(\"undefined\")"
  10.108 +
  10.109  
  10.110  subsubsection {* Evaluation and normalization by evaluation *}
  10.111  
    11.1 --- a/src/HOL/Imperative_HOL/Array.thy	Sun Jun 23 21:16:06 2013 +0200
    11.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Sun Jun 23 21:16:07 2013 +0200
    11.3 @@ -445,60 +445,60 @@
    11.4  
    11.5  text {* SML *}
    11.6  
    11.7 -code_type array (SML "_/ array")
    11.8 -code_const Array (SML "raise/ (Fail/ \"bare Array\")")
    11.9 -code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
   11.10 -code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
   11.11 -code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
   11.12 -code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
   11.13 -code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
   11.14 -code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
   11.15 -code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (SML infixl 6 "=")
   11.16 +code_printing type_constructor array \<rightharpoonup> (SML) "_/ array"
   11.17 +code_printing constant Array \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Array\")"
   11.18 +code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))"
   11.19 +code_printing constant Array.of_list \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.fromList/ _)"
   11.20 +code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))"
   11.21 +code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.length/ _)"
   11.22 +code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))"
   11.23 +code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))"
   11.24 +code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
   11.25  
   11.26  code_reserved SML Array
   11.27  
   11.28  
   11.29  text {* OCaml *}
   11.30  
   11.31 -code_type array (OCaml "_/ array")
   11.32 -code_const Array (OCaml "failwith/ \"bare Array\"")
   11.33 -code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
   11.34 -code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
   11.35 -code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/
   11.36 -  (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))")
   11.37 -code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
   11.38 -code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
   11.39 -code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
   11.40 -code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (OCaml infixl 4 "=")
   11.41 +code_printing type_constructor array \<rightharpoonup> (OCaml) "_/ array"
   11.42 +code_printing constant Array \<rightharpoonup> (OCaml) "failwith/ \"bare Array\""
   11.43 +code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)"
   11.44 +code_printing constant Array.of_list \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)"
   11.45 +code_printing constant Array.make' \<rightharpoonup> (OCaml)
   11.46 +  "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))"
   11.47 +code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))"
   11.48 +code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))"
   11.49 +code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)"
   11.50 +code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
   11.51  
   11.52  code_reserved OCaml Array
   11.53  
   11.54  
   11.55  text {* Haskell *}
   11.56  
   11.57 -code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
   11.58 -code_const Array (Haskell "error/ \"bare Array\"")
   11.59 -code_const Array.new' (Haskell "Heap.newArray")
   11.60 -code_const Array.of_list (Haskell "Heap.newListArray")
   11.61 -code_const Array.make' (Haskell "Heap.newFunArray")
   11.62 -code_const Array.len' (Haskell "Heap.lengthArray")
   11.63 -code_const Array.nth' (Haskell "Heap.readArray")
   11.64 -code_const Array.upd' (Haskell "Heap.writeArray")
   11.65 -code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Haskell infix 4 "==")
   11.66 -code_instance array :: HOL.equal (Haskell -)
   11.67 +code_printing type_constructor array \<rightharpoonup> (Haskell) "Heap.STArray/ Heap.RealWorld/ _"
   11.68 +code_printing constant Array \<rightharpoonup> (Haskell) "error/ \"bare Array\""
   11.69 +code_printing constant Array.new' \<rightharpoonup> (Haskell) "Heap.newArray"
   11.70 +code_printing constant Array.of_list \<rightharpoonup> (Haskell) "Heap.newListArray"
   11.71 +code_printing constant Array.make' \<rightharpoonup> (Haskell) "Heap.newFunArray"
   11.72 +code_printing constant Array.len' \<rightharpoonup> (Haskell) "Heap.lengthArray"
   11.73 +code_printing constant Array.nth' \<rightharpoonup> (Haskell) "Heap.readArray"
   11.74 +code_printing constant Array.upd' \<rightharpoonup> (Haskell) "Heap.writeArray"
   11.75 +code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
   11.76 +code_printing class_instance array :: HOL.equal \<rightharpoonup> (Haskell) -
   11.77  
   11.78  
   11.79  text {* Scala *}
   11.80  
   11.81 -code_type array (Scala "!collection.mutable.ArraySeq[_]")
   11.82 -code_const Array (Scala "!sys.error(\"bare Array\")")
   11.83 -code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
   11.84 -code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
   11.85 -code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
   11.86 -code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
   11.87 -code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
   11.88 -code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
   11.89 -code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Scala infixl 5 "==")
   11.90 +code_printing type_constructor array \<rightharpoonup> (Scala) "!collection.mutable.ArraySeq[_]"
   11.91 +code_printing constant Array \<rightharpoonup> (Scala) "!sys.error(\"bare Array\")"
   11.92 +code_printing constant Array.new' \<rightharpoonup> (Scala) "('_: Unit)/ => / Array.alloc((_))((_))"
   11.93 +code_printing constant Array.make' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.make((_))((_))"
   11.94 +code_printing constant Array.len' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.len((_))"
   11.95 +code_printing constant Array.nth' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.nth((_), (_))"
   11.96 +code_printing constant Array.upd' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.upd((_), (_), (_))"
   11.97 +code_printing constant Array.freeze \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.freeze((_))"
   11.98 +code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
   11.99  
  11.100  end
  11.101  
    12.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Jun 23 21:16:06 2013 +0200
    12.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun Jun 23 21:16:07 2013 +0200
    12.3 @@ -556,15 +556,15 @@
    12.4  
    12.5  subsubsection {* SML and OCaml *}
    12.6  
    12.7 -code_type Heap (SML "(unit/ ->/ _)")
    12.8 -code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
    12.9 -code_const return (SML "!(fn/ ()/ =>/ _)")
   12.10 -code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
   12.11 +code_printing type_constructor Heap \<rightharpoonup> (SML) "(unit/ ->/ _)"
   12.12 +code_printing constant bind \<rightharpoonup> (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())"
   12.13 +code_printing constant return \<rightharpoonup> (SML) "!(fn/ ()/ =>/ _)"
   12.14 +code_printing constant Heap_Monad.raise' \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
   12.15  
   12.16 -code_type Heap (OCaml "(unit/ ->/ _)")
   12.17 -code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
   12.18 -code_const return (OCaml "!(fun/ ()/ ->/ _)")
   12.19 -code_const Heap_Monad.raise' (OCaml "failwith")
   12.20 +code_printing type_constructor Heap \<rightharpoonup> (OCaml) "(unit/ ->/ _)"
   12.21 +code_printing constant bind \<rightharpoonup> (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())"
   12.22 +code_printing constant return \<rightharpoonup> (OCaml) "!(fun/ ()/ ->/ _)"
   12.23 +code_printing constant Heap_Monad.raise' \<rightharpoonup> (OCaml) "failwith"
   12.24  
   12.25  
   12.26  subsubsection {* Haskell *}
   12.27 @@ -608,10 +608,10 @@
   12.28  
   12.29  text {* Monad *}
   12.30  
   12.31 -code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
   12.32 +code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
   12.33  code_monad bind Haskell
   12.34 -code_const return (Haskell "return")
   12.35 -code_const Heap_Monad.raise' (Haskell "error")
   12.36 +code_printing constant return \<rightharpoonup> (Haskell) "return"
   12.37 +code_printing constant Heap_Monad.raise' \<rightharpoonup> (Haskell) "error"
   12.38  
   12.39  
   12.40  subsubsection {* Scala *}
   12.41 @@ -653,10 +653,10 @@
   12.42  
   12.43  code_reserved Scala Heap Ref Array
   12.44  
   12.45 -code_type Heap (Scala "(Unit/ =>/ _)")
   12.46 -code_const bind (Scala "Heap.bind")
   12.47 -code_const return (Scala "('_: Unit)/ =>/ _")
   12.48 -code_const Heap_Monad.raise' (Scala "!sys.error((_))")
   12.49 +code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
   12.50 +code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
   12.51 +code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
   12.52 +code_printing constant Heap_Monad.raise' \<rightharpoonup> (Scala) "!sys.error((_))"
   12.53  
   12.54  
   12.55  subsubsection {* Target variants with less units *}
    13.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Sun Jun 23 21:16:06 2013 +0200
    13.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Sun Jun 23 21:16:07 2013 +0200
    13.3 @@ -275,48 +275,49 @@
    13.4  
    13.5  text {* SML / Eval *}
    13.6  
    13.7 -code_type ref (SML "_/ ref")
    13.8 -code_type ref (Eval "_/ Unsynchronized.ref")
    13.9 -code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
   13.10 -code_const ref' (SML "(fn/ ()/ =>/ ref/ _)")
   13.11 -code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
   13.12 -code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
   13.13 -code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
   13.14 -code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (SML infixl 6 "=")
   13.15 +code_printing type_constructor ref \<rightharpoonup> (SML) "_/ ref"
   13.16 +code_printing type_constructor ref \<rightharpoonup> (Eval) "_/ Unsynchronized.ref"
   13.17 +code_printing constant Ref \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Ref\")"
   13.18 +code_printing constant ref' \<rightharpoonup> (SML) "(fn/ ()/ =>/ ref/ _)"
   13.19 +code_printing constant ref' \<rightharpoonup> (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
   13.20 +code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
   13.21 +code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
   13.22 +code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
   13.23  
   13.24  code_reserved Eval Unsynchronized
   13.25  
   13.26  
   13.27  text {* OCaml *}
   13.28  
   13.29 -code_type ref (OCaml "_/ ref")
   13.30 -code_const Ref (OCaml "failwith/ \"bare Ref\"")
   13.31 -code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
   13.32 -code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
   13.33 -code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
   13.34 -code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (OCaml infixl 4 "=")
   13.35 +code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
   13.36 +code_printing constant Ref \<rightharpoonup> (OCaml) "failwith/ \"bare Ref\""
   13.37 +code_printing constant ref' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ ref/ _)"
   13.38 +code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
   13.39 +code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
   13.40 +code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
   13.41  
   13.42  code_reserved OCaml ref
   13.43  
   13.44  
   13.45  text {* Haskell *}
   13.46  
   13.47 -code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
   13.48 -code_const Ref (Haskell "error/ \"bare Ref\"")
   13.49 -code_const ref' (Haskell "Heap.newSTRef")
   13.50 -code_const Ref.lookup (Haskell "Heap.readSTRef")
   13.51 -code_const Ref.update (Haskell "Heap.writeSTRef")
   13.52 -code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Haskell infix 4 "==")
   13.53 -code_instance ref :: HOL.equal (Haskell -)
   13.54 +code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"
   13.55 +code_printing constant Ref \<rightharpoonup> (Haskell) "error/ \"bare Ref\""
   13.56 +code_printing constant ref' \<rightharpoonup> (Haskell) "Heap.newSTRef"
   13.57 +code_printing constant Ref.lookup \<rightharpoonup> (Haskell) "Heap.readSTRef"
   13.58 +code_printing constant Ref.update \<rightharpoonup> (Haskell) "Heap.writeSTRef"
   13.59 +code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
   13.60 +code_printing class_instance ref :: HOL.equal \<rightharpoonup> (Haskell) -
   13.61  
   13.62  
   13.63  text {* Scala *}
   13.64  
   13.65 -code_type ref (Scala "!Ref[_]")
   13.66 -code_const Ref (Scala "!sys.error(\"bare Ref\")")
   13.67 -code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
   13.68 -code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
   13.69 -code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
   13.70 -code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Scala infixl 5 "==")
   13.71 +code_printing type_constructor ref \<rightharpoonup> (Scala) "!Ref[_]"
   13.72 +code_printing constant Ref \<rightharpoonup> (Scala) "!sys.error(\"bare Ref\")"
   13.73 +code_printing constant ref' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref((_))"
   13.74 +code_printing constant Ref.lookup \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.lookup((_))"
   13.75 +code_printing constant Ref.update \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.update((_), (_))"
   13.76 +code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
   13.77  
   13.78  end
   13.79 +
    14.1 --- a/src/HOL/Int.thy	Sun Jun 23 21:16:06 2013 +0200
    14.2 +++ b/src/HOL/Int.thy	Sun Jun 23 21:16:07 2013 +0200
    14.3 @@ -1614,14 +1614,8 @@
    14.4  
    14.5  text {* Serializer setup *}
    14.6  
    14.7 -code_modulename SML
    14.8 -  Int Arith
    14.9 -
   14.10 -code_modulename OCaml
   14.11 -  Int Arith
   14.12 -
   14.13 -code_modulename Haskell
   14.14 -  Int Arith
   14.15 +code_identifier
   14.16 +  code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   14.17  
   14.18  quickcheck_params [default_type = int]
   14.19  
    15.1 --- a/src/HOL/Library/Code_Binary_Nat.thy	Sun Jun 23 21:16:06 2013 +0200
    15.2 +++ b/src/HOL/Library/Code_Binary_Nat.thy	Sun Jun 23 21:16:07 2013 +0200
    15.3 @@ -142,14 +142,9 @@
    15.4    by (simp_all add: nat_of_num_numeral)
    15.5  
    15.6  
    15.7 -code_modulename SML
    15.8 -  Code_Binary_Nat Arith
    15.9 -
   15.10 -code_modulename OCaml
   15.11 -  Code_Binary_Nat Arith
   15.12 -
   15.13 -code_modulename Haskell
   15.14 -  Code_Binary_Nat Arith
   15.15 +code_identifier
   15.16 +  code_module Code_Binary_Nat \<rightharpoonup>
   15.17 +    (SML) Arith and (OCaml) Arith and (Haskell) Arith
   15.18  
   15.19  hide_const (open) dup sub
   15.20  
    16.1 --- a/src/HOL/Library/Code_Char.thy	Sun Jun 23 21:16:06 2013 +0200
    16.2 +++ b/src/HOL/Library/Code_Char.thy	Sun Jun 23 21:16:07 2013 +0200
    16.3 @@ -8,19 +8,28 @@
    16.4  imports Main Char_ord
    16.5  begin
    16.6  
    16.7 -code_type char
    16.8 -  (SML "char")
    16.9 -  (OCaml "char")
   16.10 -  (Haskell "Prelude.Char")
   16.11 -  (Scala "Char")
   16.12 +code_printing
   16.13 +  type_constructor char \<rightharpoonup>
   16.14 +    (SML) "char"
   16.15 +    and (OCaml) "char"
   16.16 +    and (Haskell) "Prelude.Char"
   16.17 +    and (Scala) "Char"
   16.18  
   16.19  setup {*
   16.20    fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
   16.21    #> String_Code.add_literal_list_string "Haskell"
   16.22  *}
   16.23  
   16.24 -code_instance char :: equal
   16.25 -  (Haskell -)
   16.26 +code_printing
   16.27 +  class_instance char :: equal \<rightharpoonup>
   16.28 +    (Haskell) -
   16.29 +| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
   16.30 +    (SML) "!((_ : char) = _)"
   16.31 +    and (OCaml) "!((_ : char) = _)"
   16.32 +    and (Haskell) infix 4 "=="
   16.33 +    and (Scala) infixl 5 "=="
   16.34 +| constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup>
   16.35 +    (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
   16.36  
   16.37  code_reserved SML
   16.38    char
   16.39 @@ -31,32 +40,22 @@
   16.40  code_reserved Scala
   16.41    char
   16.42  
   16.43 -code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   16.44 -  (SML "!((_ : char) = _)")
   16.45 -  (OCaml "!((_ : char) = _)")
   16.46 -  (Haskell infix 4 "==")
   16.47 -  (Scala infixl 5 "==")
   16.48 -
   16.49 -code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   16.50 -  (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
   16.51 -
   16.52 -
   16.53  definition implode :: "string \<Rightarrow> String.literal" where
   16.54    "implode = STR"
   16.55  
   16.56  code_reserved SML String
   16.57  
   16.58 -code_const implode
   16.59 -  (SML "String.implode")
   16.60 -  (OCaml "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)")
   16.61 -  (Haskell "_")
   16.62 -  (Scala "!(\"\" ++/ _)")
   16.63 -
   16.64 -code_const explode
   16.65 -  (SML "String.explode")
   16.66 -  (OCaml "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])")
   16.67 -  (Haskell "_")
   16.68 -  (Scala "!(_.toList)")
   16.69 +code_printing
   16.70 +  constant implode \<rightharpoonup>
   16.71 +    (SML) "String.implode"
   16.72 +    and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)"
   16.73 +    and (Haskell) "_"
   16.74 +    and (Scala) "!(\"\" ++/ _)"
   16.75 +| constant explode \<rightharpoonup>
   16.76 +    (SML) "String.explode"
   16.77 +    and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])"
   16.78 +    and (Haskell) "_"
   16.79 +    and (Scala) "!(_.toList)"
   16.80  
   16.81  
   16.82  definition integer_of_char :: "char \<Rightarrow> integer"
   16.83 @@ -75,30 +74,29 @@
   16.84    "char_of_nat = char_of_integer o integer_of_nat"
   16.85    by (simp add: char_of_integer_def fun_eq_iff)
   16.86  
   16.87 -code_const integer_of_char and char_of_integer
   16.88 -  (SML "!(IntInf.fromInt o Char.ord)"
   16.89 -    and "!(Char.chr o IntInf.toInt)")
   16.90 -  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
   16.91 -    and "Char.chr (Big'_int.int'_of'_big'_int _)")
   16.92 -  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
   16.93 -    and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
   16.94 -  (Scala "BigInt(_.toInt)"
   16.95 -    and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
   16.96 -
   16.97 -
   16.98 -code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   16.99 -  (SML "!((_ : char) <= _)")
  16.100 -  (OCaml "!((_ : char) <= _)")
  16.101 -  (Haskell infix 4 "<=")
  16.102 -  (Scala infixl 4 "<=")
  16.103 -  (Eval infixl 6 "<=")
  16.104 -
  16.105 -code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
  16.106 -  (SML "!((_ : char) < _)")
  16.107 -  (OCaml "!((_ : char) < _)")
  16.108 -  (Haskell infix 4 "<")
  16.109 -  (Scala infixl 4 "<")
  16.110 -  (Eval infixl 6 "<")
  16.111 +code_printing
  16.112 +  constant integer_of_char \<rightharpoonup>
  16.113 +    (SML) "!(IntInf.fromInt o Char.ord)"
  16.114 +    and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
  16.115 +    and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
  16.116 +    and (Scala) "BigInt(_.toInt)"
  16.117 +| constant char_of_integer \<rightharpoonup>
  16.118 +    (SML) "!(Char.chr o IntInf.toInt)"
  16.119 +    and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
  16.120 +    and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
  16.121 +    and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
  16.122 +| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
  16.123 +    (SML) "!((_ : char) <= _)"
  16.124 +    and (OCaml) "!((_ : char) <= _)"
  16.125 +    and (Haskell) infix 4 "<="
  16.126 +    and (Scala) infixl 4 "<="
  16.127 +    and (Eval) infixl 6 "<="
  16.128 +| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
  16.129 +    (SML) "!((_ : char) < _)"
  16.130 +    and (OCaml) "!((_ : char) < _)"
  16.131 +    and (Haskell) infix 4 "<"
  16.132 +    and (Scala) infixl 4 "<"
  16.133 +    and (Eval) infixl 6 "<"
  16.134  
  16.135  end
  16.136  
    17.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Jun 23 21:16:06 2013 +0200
    17.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Jun 23 21:16:07 2013 +0200
    17.3 @@ -14,61 +14,75 @@
    17.4  The only legitimate use of this theory is as a tool for code generation
    17.5  purposes. *}
    17.6  
    17.7 -code_type real
    17.8 -  (SML   "real")
    17.9 -  (OCaml "float")
   17.10 +code_printing
   17.11 +  type_constructor real \<rightharpoonup>
   17.12 +    (SML) "real"
   17.13 +    and (OCaml) "float"
   17.14  
   17.15 -code_const Ratreal
   17.16 -  (SML "error/ \"Bad constant: Ratreal\"")
   17.17 +code_printing
   17.18 +  constant Ratreal \<rightharpoonup>
   17.19 +    (SML) "error/ \"Bad constant: Ratreal\""
   17.20  
   17.21 -code_const "0 :: real"
   17.22 -  (SML   "0.0")
   17.23 -  (OCaml "0.0")
   17.24 +code_printing
   17.25 +  constant "0 :: real" \<rightharpoonup>
   17.26 +    (SML) "0.0"
   17.27 +    and (OCaml) "0.0"
   17.28  declare zero_real_code[code_unfold del]
   17.29  
   17.30 -code_const "1 :: real"
   17.31 -  (SML   "1.0")
   17.32 -  (OCaml "1.0")
   17.33 +code_printing
   17.34 +  constant "1 :: real" \<rightharpoonup>
   17.35 +    (SML) "1.0"
   17.36 +    and (OCaml) "1.0"
   17.37  declare one_real_code[code_unfold del]
   17.38  
   17.39 -code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
   17.40 -  (SML   "Real.== ((_), (_))")
   17.41 -  (OCaml "Pervasives.(=)")
   17.42 +code_printing
   17.43 +  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
   17.44 +    (SML) "Real.== ((_), (_))"
   17.45 +    and (OCaml) "Pervasives.(=)"
   17.46  
   17.47 -code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
   17.48 -  (SML   "Real.<= ((_), (_))")
   17.49 -  (OCaml "Pervasives.(<=)")
   17.50 +code_printing
   17.51 +  constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
   17.52 +    (SML) "Real.<= ((_), (_))"
   17.53 +    and (OCaml) "Pervasives.(<=)"
   17.54  
   17.55 -code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
   17.56 -  (SML   "Real.< ((_), (_))")
   17.57 -  (OCaml "Pervasives.(<)")
   17.58 +code_printing
   17.59 +  constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
   17.60 +    (SML) "Real.< ((_), (_))"
   17.61 +    and (OCaml) "Pervasives.(<)"
   17.62  
   17.63 -code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
   17.64 -  (SML   "Real.+ ((_), (_))")
   17.65 -  (OCaml "Pervasives.( +. )")
   17.66 +code_printing
   17.67 +  constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
   17.68 +    (SML) "Real.+ ((_), (_))"
   17.69 +    and (OCaml) "Pervasives.( +. )"
   17.70  
   17.71 -code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
   17.72 -  (SML   "Real.* ((_), (_))")
   17.73 -  (OCaml "Pervasives.( *. )")
   17.74 +code_printing
   17.75 +  constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
   17.76 +    (SML) "Real.* ((_), (_))"
   17.77 +    and (OCaml) "Pervasives.( *. )"
   17.78  
   17.79 -code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
   17.80 -  (SML   "Real.- ((_), (_))")
   17.81 -  (OCaml "Pervasives.( -. )")
   17.82 +code_printing
   17.83 +  constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
   17.84 +    (SML) "Real.- ((_), (_))"
   17.85 +    and (OCaml) "Pervasives.( -. )"
   17.86  
   17.87 -code_const "uminus :: real \<Rightarrow> real"
   17.88 -  (SML   "Real.~")
   17.89 -  (OCaml "Pervasives.( ~-. )")
   17.90 +code_printing
   17.91 +  constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
   17.92 +    (SML) "Real.~"
   17.93 +    and (OCaml) "Pervasives.( ~-. )"
   17.94  
   17.95 -code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
   17.96 -  (SML   "Real.'/ ((_), (_))")
   17.97 -  (OCaml "Pervasives.( '/. )")
   17.98 +code_printing
   17.99 +  constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
  17.100 +    (SML) "Real.'/ ((_), (_))"
  17.101 +    and (OCaml) "Pervasives.( '/. )"
  17.102  
  17.103 -code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
  17.104 -  (SML   "Real.== ((_:real), (_))")
  17.105 +code_printing
  17.106 +  constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
  17.107 +    (SML) "Real.== ((_:real), (_))"
  17.108  
  17.109 -code_const "sqrt :: real \<Rightarrow> real"
  17.110 -  (SML   "Math.sqrt")
  17.111 -  (OCaml "Pervasives.sqrt")
  17.112 +code_printing
  17.113 +  constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
  17.114 +    (SML) "Math.sqrt"
  17.115 +    and (OCaml) "Pervasives.sqrt"
  17.116  declare sqrt_def[code del]
  17.117  
  17.118  definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
  17.119 @@ -76,55 +90,64 @@
  17.120  lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
  17.121    unfolding real_exp_def ..
  17.122  
  17.123 -code_const real_exp
  17.124 -  (SML   "Math.exp")
  17.125 -  (OCaml "Pervasives.exp")
  17.126 +code_printing
  17.127 +  constant real_exp \<rightharpoonup>
  17.128 +    (SML) "Math.exp"
  17.129 +    and (OCaml) "Pervasives.exp"
  17.130  declare real_exp_def[code del]
  17.131  declare exp_def[code del]
  17.132  
  17.133  hide_const (open) real_exp
  17.134  
  17.135 -code_const ln
  17.136 -  (SML   "Math.ln")
  17.137 -  (OCaml "Pervasives.ln")
  17.138 +code_printing
  17.139 +  constant ln \<rightharpoonup>
  17.140 +    (SML) "Math.ln"
  17.141 +    and (OCaml) "Pervasives.ln"
  17.142  declare ln_def[code del]
  17.143  
  17.144 -code_const cos
  17.145 -  (SML   "Math.cos")
  17.146 -  (OCaml "Pervasives.cos")
  17.147 +code_printing
  17.148 +  constant cos \<rightharpoonup>
  17.149 +    (SML) "Math.cos"
  17.150 +    and (OCaml) "Pervasives.cos"
  17.151  declare cos_def[code del]
  17.152  
  17.153 -code_const sin
  17.154 -  (SML   "Math.sin")
  17.155 -  (OCaml "Pervasives.sin")
  17.156 +code_printing
  17.157 +  constant sin \<rightharpoonup>
  17.158 +    (SML) "Math.sin"
  17.159 +    and (OCaml) "Pervasives.sin"
  17.160  declare sin_def[code del]
  17.161  
  17.162 -code_const pi
  17.163 -  (SML   "Math.pi")
  17.164 -  (OCaml "Pervasives.pi")
  17.165 +code_printing
  17.166 +  constant pi \<rightharpoonup>
  17.167 +    (SML) "Math.pi"
  17.168 +    and (OCaml) "Pervasives.pi"
  17.169  declare pi_def[code del]
  17.170  
  17.171 -code_const arctan
  17.172 -  (SML   "Math.atan")
  17.173 -  (OCaml "Pervasives.atan")
  17.174 +code_printing
  17.175 +  constant arctan \<rightharpoonup>
  17.176 +    (SML) "Math.atan"
  17.177 +    and (OCaml) "Pervasives.atan"
  17.178  declare arctan_def[code del]
  17.179  
  17.180 -code_const arccos
  17.181 -  (SML   "Math.scos")
  17.182 -  (OCaml "Pervasives.acos")
  17.183 +code_printing
  17.184 +  constant arccos \<rightharpoonup>
  17.185 +    (SML) "Math.scos"
  17.186 +    and (OCaml) "Pervasives.acos"
  17.187  declare arccos_def[code del]
  17.188  
  17.189 -code_const arcsin
  17.190 -  (SML   "Math.asin")
  17.191 -  (OCaml "Pervasives.asin")
  17.192 +code_printing
  17.193 +  constant arcsin \<rightharpoonup>
  17.194 +    (SML) "Math.asin"
  17.195 +    and (OCaml) "Pervasives.asin"
  17.196  declare arcsin_def[code del]
  17.197  
  17.198  definition real_of_integer :: "integer \<Rightarrow> real" where
  17.199    "real_of_integer = of_int \<circ> int_of_integer"
  17.200  
  17.201 -code_const real_of_integer
  17.202 -  (SML "Real.fromInt")
  17.203 -  (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
  17.204 +code_printing
  17.205 +  constant real_of_integer \<rightharpoonup>
  17.206 +    (SML) "Real.fromInt"
  17.207 +    and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
  17.208  
  17.209  definition real_of_int :: "int \<Rightarrow> real" where
  17.210    [code_abbrev]: "real_of_int = of_int"
  17.211 @@ -151,7 +174,8 @@
  17.212  
  17.213  hide_const (open) real_of_int
  17.214  
  17.215 -code_const Ratreal (SML)
  17.216 +code_printing
  17.217 +  constant Ratreal \<rightharpoonup> (SML)
  17.218  
  17.219  definition Realfract :: "int => int => real"
  17.220  where
  17.221 @@ -159,8 +183,8 @@
  17.222  
  17.223  code_datatype Realfract
  17.224  
  17.225 -code_const Realfract
  17.226 -  (SML "Real.fromInt _/ '// Real.fromInt _")
  17.227 +code_printing
  17.228 +  constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
  17.229  
  17.230  lemma [code]:
  17.231    "Ratreal r = split Realfract (quotient_of r)"
    18.1 --- a/src/HOL/Library/Code_Target_Int.thy	Sun Jun 23 21:16:06 2013 +0200
    18.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Sun Jun 23 21:16:07 2013 +0200
    18.3 @@ -109,14 +109,9 @@
    18.4    "nat = nat_of_integer \<circ> of_int"
    18.5    by transfer (simp add: fun_eq_iff)
    18.6  
    18.7 -code_modulename SML
    18.8 -  Code_Target_Int Arith
    18.9 -
   18.10 -code_modulename OCaml
   18.11 -  Code_Target_Int Arith
   18.12 -
   18.13 -code_modulename Haskell
   18.14 -  Code_Target_Int Arith
   18.15 +code_identifier
   18.16 +  code_module Code_Target_Int \<rightharpoonup>
   18.17 +    (SML) Arith and (OCaml) Arith and (Haskell) Arith
   18.18  
   18.19  end
   18.20  
    19.1 --- a/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:06 2013 +0200
    19.2 +++ b/src/HOL/Library/Code_Target_Nat.thy	Sun Jun 23 21:16:07 2013 +0200
    19.3 @@ -123,14 +123,9 @@
    19.4    "integer_of_nat (nat k) = max 0 (integer_of_int k)"
    19.5    by transfer auto
    19.6  
    19.7 -code_modulename SML
    19.8 -  Code_Target_Nat Arith
    19.9 -
   19.10 -code_modulename OCaml
   19.11 -  Code_Target_Nat Arith
   19.12 -
   19.13 -code_modulename Haskell
   19.14 -  Code_Target_Nat Arith
   19.15 +code_identifier
   19.16 +  code_module Code_Target_Nat \<rightharpoonup>
   19.17 +    (SML) Arith and (OCaml) Arith and (Haskell) Arith
   19.18  
   19.19  end
   19.20  
    20.1 --- a/src/HOL/Library/Debug.thy	Sun Jun 23 21:16:06 2013 +0200
    20.2 +++ b/src/HOL/Library/Debug.thy	Sun Jun 23 21:16:07 2013 +0200
    20.3 @@ -29,11 +29,12 @@
    20.4  definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
    20.5    [simp]: "timing s f x = f x"
    20.6  
    20.7 -code_const trace and flush and timing
    20.8 -  (* FIXME proper @{make_string} instead of PolyML.makestring?!?! *)
    20.9 -  (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
   20.10 +code_printing
   20.11 +  constant trace \<rightharpoonup> (Eval) "Output.tracing"
   20.12 +| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *}
   20.13 +| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
   20.14  
   20.15 -code_reserved Eval Output PolyML Timing
   20.16 +code_reserved Eval Output Timing
   20.17  
   20.18  hide_const (open) trace tracing flush flushing timing
   20.19  
    21.1 --- a/src/HOL/Library/IArray.thy	Sun Jun 23 21:16:06 2013 +0200
    21.2 +++ b/src/HOL/Library/IArray.thy	Sun Jun 23 21:16:07 2013 +0200
    21.3 @@ -40,11 +40,9 @@
    21.4  
    21.5  code_reserved SML Vector
    21.6  
    21.7 -code_type iarray
    21.8 -  (SML "_ Vector.vector")
    21.9 -
   21.10 -code_const IArray
   21.11 -  (SML "Vector.fromList")
   21.12 +code_printing
   21.13 +  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
   21.14 +| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
   21.15  
   21.16  lemma [code]:
   21.17  "size (as :: 'a iarray) = 0"
   21.18 @@ -74,8 +72,8 @@
   21.19  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
   21.20  by simp 
   21.21  
   21.22 -code_const IArray.tabulate
   21.23 -  (SML "Vector.tabulate")
   21.24 +code_printing
   21.25 +  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
   21.26  
   21.27  primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
   21.28  "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
   21.29 @@ -85,8 +83,8 @@
   21.30  "as !! n = IArray.sub' (as, integer_of_nat n)"
   21.31  by simp
   21.32  
   21.33 -code_const IArray.sub'
   21.34 -  (SML "Vector.sub")
   21.35 +code_printing
   21.36 +  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
   21.37  
   21.38  definition length' :: "'a iarray \<Rightarrow> integer" where
   21.39  [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
   21.40 @@ -96,8 +94,8 @@
   21.41  "IArray.length as = nat_of_integer (IArray.length' as)"
   21.42  by simp
   21.43  
   21.44 -code_const IArray.length'
   21.45 -  (SML "Vector.length")
   21.46 +code_printing
   21.47 +  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
   21.48  
   21.49  end
   21.50  
    22.1 --- a/src/HOL/Library/Parallel.thy	Sun Jun 23 21:16:06 2013 +0200
    22.2 +++ b/src/HOL/Library/Parallel.thy	Sun Jun 23 21:16:07 2013 +0200
    22.3 @@ -18,14 +18,10 @@
    22.4    shows "f = g"
    22.5    using assms by (cases f, cases g) (simp add: ext)
    22.6  
    22.7 -code_type future
    22.8 -  (Eval "_ future")
    22.9 -
   22.10 -code_const fork
   22.11 -  (Eval "Future.fork")
   22.12 -
   22.13 -code_const join
   22.14 -  (Eval "Future.join")
   22.15 +code_printing
   22.16 +  type_constructor future \<rightharpoonup> (Eval) "_ future"
   22.17 +| constant fork \<rightharpoonup> (Eval) "Future.fork"
   22.18 +| constant join \<rightharpoonup> (Eval) "Future.join"
   22.19  
   22.20  code_reserved Eval Future future
   22.21  
   22.22 @@ -49,14 +45,10 @@
   22.23    "exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
   22.24    by (simp add: exists_def list_ex_iff)
   22.25  
   22.26 -code_const map
   22.27 -  (Eval "Par'_List.map")
   22.28 -
   22.29 -code_const forall
   22.30 -  (Eval "Par'_List.forall")
   22.31 -
   22.32 -code_const exists
   22.33 -  (Eval "Par'_List.exists")
   22.34 +code_printing
   22.35 +  constant map \<rightharpoonup> (Eval) "Par'_List.map"
   22.36 +| constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
   22.37 +| constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
   22.38  
   22.39  code_reserved Eval Par_List
   22.40  
    23.1 --- a/src/HOL/List.thy	Sun Jun 23 21:16:06 2013 +0200
    23.2 +++ b/src/HOL/List.thy	Sun Jun 23 21:16:07 2013 +0200
    23.3 @@ -6042,30 +6042,31 @@
    23.4              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    23.5          | NONE =>
    23.6              default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    23.7 -  in Code_Target.add_const_syntax target @{const_name Cons}
    23.8 -    (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
    23.9 +  in
   23.10 +    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
   23.11 +      [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
   23.12    end
   23.13  
   23.14  end;
   23.15  *}
   23.16  
   23.17 -code_type list
   23.18 -  (SML "_ list")
   23.19 -  (OCaml "_ list")
   23.20 -  (Haskell "![(_)]")
   23.21 -  (Scala "List[(_)]")
   23.22 -
   23.23 -code_const Nil
   23.24 -  (SML "[]")
   23.25 -  (OCaml "[]")
   23.26 -  (Haskell "[]")
   23.27 -  (Scala "!Nil")
   23.28 -
   23.29 -code_instance list :: equal
   23.30 -  (Haskell -)
   23.31 -
   23.32 -code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   23.33 -  (Haskell infix 4 "==")
   23.34 +code_printing
   23.35 +  type_constructor list \<rightharpoonup>
   23.36 +    (SML) "_ list"
   23.37 +    and (OCaml) "_ list"
   23.38 +    and (Haskell) "![(_)]"
   23.39 +    and (Scala) "List[(_)]"
   23.40 +| constant Nil \<rightharpoonup>
   23.41 +    (SML) "[]"
   23.42 +    and (OCaml) "[]"
   23.43 +    and (Haskell) "[]"
   23.44 +    and (Scala) "!Nil"
   23.45 +| class_instance list :: equal \<rightharpoonup>
   23.46 +    (Haskell) -
   23.47 +| constant "HOL.equal :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" \<rightharpoonup>
   23.48 +    (Haskell) infix 4 "=="
   23.49 +
   23.50 +setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
   23.51  
   23.52  code_reserved SML
   23.53    list
   23.54 @@ -6073,49 +6074,37 @@
   23.55  code_reserved OCaml
   23.56    list
   23.57  
   23.58 -setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
   23.59 -
   23.60  
   23.61  subsubsection {* Use convenient predefined operations *}
   23.62  
   23.63 -code_const "op @"
   23.64 -  (SML infixr 7 "@")
   23.65 -  (OCaml infixr 6 "@")
   23.66 -  (Haskell infixr 5 "++")
   23.67 -  (Scala infixl 7 "++")
   23.68 -
   23.69 -code_const map
   23.70 -  (Haskell "map")
   23.71 -
   23.72 -code_const filter
   23.73 -  (Haskell "filter")
   23.74 -
   23.75 -code_const concat
   23.76 -  (Haskell "concat")
   23.77 -
   23.78 -code_const List.maps
   23.79 -  (Haskell "concatMap")
   23.80 -
   23.81 -code_const rev
   23.82 -  (Haskell "reverse")
   23.83 -
   23.84 -code_const zip
   23.85 -  (Haskell "zip")
   23.86 -
   23.87 -code_const List.null
   23.88 -  (Haskell "null")
   23.89 -
   23.90 -code_const takeWhile
   23.91 -  (Haskell "takeWhile")
   23.92 -
   23.93 -code_const dropWhile
   23.94 -  (Haskell "dropWhile")
   23.95 -
   23.96 -code_const list_all
   23.97 -  (Haskell "all")
   23.98 -
   23.99 -code_const list_ex
  23.100 -  (Haskell "any")
  23.101 +code_printing
  23.102 +  constant "op @" \<rightharpoonup>
  23.103 +    (SML) infixr 7 "@"
  23.104 +    and (OCaml) infixr 6 "@"
  23.105 +    and (Haskell) infixr 5 "++"
  23.106 +    and (Scala) infixl 7 "++"
  23.107 +| constant map \<rightharpoonup>
  23.108 +    (Haskell) "map"
  23.109 +| constant filter \<rightharpoonup>
  23.110 +    (Haskell) "filter"
  23.111 +| constant concat \<rightharpoonup>
  23.112 +    (Haskell) "concat"
  23.113 +| constant List.maps \<rightharpoonup>
  23.114 +    (Haskell) "concatMap"
  23.115 +| constant rev \<rightharpoonup>
  23.116 +    (Haskell) "reverse"
  23.117 +| constant zip \<rightharpoonup>
  23.118 +    (Haskell) "zip"
  23.119 +| constant List.null \<rightharpoonup>
  23.120 +    (Haskell) "null"
  23.121 +| constant takeWhile \<rightharpoonup>
  23.122 +    (Haskell) "takeWhile"
  23.123 +| constant dropWhile \<rightharpoonup>
  23.124 +    (Haskell) "dropWhile"
  23.125 +| constant list_all \<rightharpoonup>
  23.126 +    (Haskell) "all"
  23.127 +| constant list_ex \<rightharpoonup>
  23.128 +    (Haskell) "any"
  23.129  
  23.130  
  23.131  subsubsection {* Implementation of sets by lists *}
    24.1 --- a/src/HOL/MicroJava/BV/BVExample.thy	Sun Jun 23 21:16:06 2013 +0200
    24.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Jun 23 21:16:07 2013 +0200
    24.3 @@ -434,8 +434,8 @@
    24.4  
    24.5  definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
    24.6    "some_elem = (%S. SOME x. x : S)"
    24.7 -code_const some_elem
    24.8 -  (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
    24.9 +code_printing
   24.10 +  constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
   24.11  
   24.12  text {* This code setup is just a demonstration and \emph{not} sound! *}
   24.13  
    25.1 --- a/src/HOL/Nat.thy	Sun Jun 23 21:16:06 2013 +0200
    25.2 +++ b/src/HOL/Nat.thy	Sun Jun 23 21:16:07 2013 +0200
    25.3 @@ -1911,14 +1911,8 @@
    25.4  
    25.5  subsection {* code module namespace *}
    25.6  
    25.7 -code_modulename SML
    25.8 -  Nat Arith
    25.9 -
   25.10 -code_modulename OCaml
   25.11 -  Nat Arith
   25.12 -
   25.13 -code_modulename Haskell
   25.14 -  Nat Arith
   25.15 +code_identifier
   25.16 +  code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   25.17  
   25.18  hide_const (open) of_nat_aux
   25.19  
    26.1 --- a/src/HOL/Num.thy	Sun Jun 23 21:16:06 2013 +0200
    26.2 +++ b/src/HOL/Num.thy	Sun Jun 23 21:16:07 2013 +0200
    26.3 @@ -1114,14 +1114,8 @@
    26.4  
    26.5  subsection {* code module namespace *}
    26.6  
    26.7 -code_modulename SML
    26.8 -  Num Arith
    26.9 -
   26.10 -code_modulename OCaml
   26.11 -  Num Arith
   26.12 -
   26.13 -code_modulename Haskell
   26.14 -  Num Arith
   26.15 +code_identifier
   26.16 +  code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   26.17  
   26.18  end
   26.19  
    27.1 --- a/src/HOL/Option.thy	Sun Jun 23 21:16:06 2013 +0200
    27.2 +++ b/src/HOL/Option.thy	Sun Jun 23 21:16:07 2013 +0200
    27.3 @@ -186,23 +186,26 @@
    27.4  
    27.5  hide_const (open) is_none
    27.6  
    27.7 -code_type option
    27.8 -  (SML "_ option")
    27.9 -  (OCaml "_ option")
   27.10 -  (Haskell "Maybe _")
   27.11 -  (Scala "!Option[(_)]")
   27.12 -
   27.13 -code_const None and Some
   27.14 -  (SML "NONE" and "SOME")
   27.15 -  (OCaml "None" and "Some _")
   27.16 -  (Haskell "Nothing" and "Just")
   27.17 -  (Scala "!None" and "Some")
   27.18 -
   27.19 -code_instance option :: equal
   27.20 -  (Haskell -)
   27.21 -
   27.22 -code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   27.23 -  (Haskell infix 4 "==")
   27.24 +code_printing
   27.25 +  type_constructor option \<rightharpoonup>
   27.26 +    (SML) "_ option"
   27.27 +    and (OCaml) "_ option"
   27.28 +    and (Haskell) "Maybe _"
   27.29 +    and (Scala) "!Option[(_)]"
   27.30 +| constant None \<rightharpoonup>
   27.31 +    (SML) "NONE"
   27.32 +    and (OCaml) "None"
   27.33 +    and (Haskell) "Nothing"
   27.34 +    and (Scala) "!None"
   27.35 +| constant Some \<rightharpoonup>
   27.36 +    (SML) "SOME"
   27.37 +    and (OCaml) "Some _"
   27.38 +    and (Haskell) "Just"
   27.39 +    and (Scala) "Some"
   27.40 +| class_instance option :: equal \<rightharpoonup>
   27.41 +    (Haskell) -
   27.42 +| constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
   27.43 +    (Haskell) infix 4 "=="
   27.44  
   27.45  code_reserved SML
   27.46    option NONE SOME
    28.1 --- a/src/HOL/Power.thy	Sun Jun 23 21:16:06 2013 +0200
    28.2 +++ b/src/HOL/Power.thy	Sun Jun 23 21:16:07 2013 +0200
    28.3 @@ -742,14 +742,8 @@
    28.4  
    28.5  declare power.power.simps [code]
    28.6  
    28.7 -code_modulename SML
    28.8 -  Power Arith
    28.9 -
   28.10 -code_modulename OCaml
   28.11 -  Power Arith
   28.12 -
   28.13 -code_modulename Haskell
   28.14 -  Power Arith
   28.15 +code_identifier
   28.16 +  code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   28.17  
   28.18  end
   28.19  
    29.1 --- a/src/HOL/Product_Type.thy	Sun Jun 23 21:16:06 2013 +0200
    29.2 +++ b/src/HOL/Product_Type.thy	Sun Jun 23 21:16:07 2013 +0200
    29.3 @@ -34,11 +34,9 @@
    29.4    Code.add_case @{thm If_case_cert}
    29.5  *}
    29.6  
    29.7 -code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    29.8 -  (Haskell infix 4 "==")
    29.9 -
   29.10 -code_instance bool :: equal
   29.11 -  (Haskell -)
   29.12 +code_printing
   29.13 +  constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
   29.14 +| class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) -
   29.15  
   29.16  
   29.17  subsection {* The @{text unit} type *}
   29.18 @@ -95,23 +93,21 @@
   29.19  lemma [code]:
   29.20    "HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
   29.21  
   29.22 -code_type unit
   29.23 -  (SML "unit")
   29.24 -  (OCaml "unit")
   29.25 -  (Haskell "()")
   29.26 -  (Scala "Unit")
   29.27 -
   29.28 -code_const Unity
   29.29 -  (SML "()")
   29.30 -  (OCaml "()")
   29.31 -  (Haskell "()")
   29.32 -  (Scala "()")
   29.33 -
   29.34 -code_instance unit :: equal
   29.35 -  (Haskell -)
   29.36 -
   29.37 -code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
   29.38 -  (Haskell infix 4 "==")
   29.39 +code_printing
   29.40 +  type_constructor unit \<rightharpoonup>
   29.41 +    (SML) "unit"
   29.42 +    and (OCaml) "unit"
   29.43 +    and (Haskell) "()"
   29.44 +    and (Scala) "Unit"
   29.45 +| constant Unity \<rightharpoonup>
   29.46 +    (SML) "()"
   29.47 +    and (OCaml) "()"
   29.48 +    and (Haskell) "()"
   29.49 +    and (Scala) "()"
   29.50 +| class_instance unit :: equal \<rightharpoonup>
   29.51 +    (Haskell) -
   29.52 +| constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup>
   29.53 +    (Haskell) infix 4 "=="
   29.54  
   29.55  code_reserved SML
   29.56    unit
   29.57 @@ -288,23 +284,21 @@
   29.58  
   29.59  subsubsection {* Code generator setup *}
   29.60  
   29.61 -code_type prod
   29.62 -  (SML infix 2 "*")
   29.63 -  (OCaml infix 2 "*")
   29.64 -  (Haskell "!((_),/ (_))")
   29.65 -  (Scala "((_),/ (_))")
   29.66 -
   29.67 -code_const Pair
   29.68 -  (SML "!((_),/ (_))")
   29.69 -  (OCaml "!((_),/ (_))")
   29.70 -  (Haskell "!((_),/ (_))")
   29.71 -  (Scala "!((_),/ (_))")
   29.72 -
   29.73 -code_instance prod :: equal
   29.74 -  (Haskell -)
   29.75 -
   29.76 -code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
   29.77 -  (Haskell infix 4 "==")
   29.78 +code_printing
   29.79 +  type_constructor prod \<rightharpoonup>
   29.80 +    (SML) infix 2 "*"
   29.81 +    and (OCaml) infix 2 "*"
   29.82 +    and (Haskell) "!((_),/ (_))"
   29.83 +    and (Scala) "((_),/ (_))"
   29.84 +| constant Pair \<rightharpoonup>
   29.85 +    (SML) "!((_),/ (_))"
   29.86 +    and (OCaml) "!((_),/ (_))"
   29.87 +    and (Haskell) "!((_),/ (_))"
   29.88 +    and (Scala) "!((_),/ (_))"
   29.89 +| class_instance  prod :: equal \<rightharpoonup>
   29.90 +    (Haskell) -
   29.91 +| constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup>
   29.92 +    (Haskell) infix 4 "=="
   29.93  
   29.94  
   29.95  subsubsection {* Fundamental operations and properties *}
   29.96 @@ -330,8 +324,9 @@
   29.97  lemma snd_conv [simp, code]: "snd (a, b) = b"
   29.98    unfolding snd_def by simp
   29.99  
  29.100 -code_const fst and snd
  29.101 -  (Haskell "fst" and "snd")
  29.102 +code_printing
  29.103 +  constant fst \<rightharpoonup> (Haskell) "fst"
  29.104 +| constant snd \<rightharpoonup> (Haskell) "snd"
  29.105  
  29.106  lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
  29.107    by (simp add: fun_eq_iff split: prod.split)
  29.108 @@ -764,8 +759,8 @@
  29.109  lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
  29.110    by (simp add: fun_eq_iff scomp_unfold)
  29.111  
  29.112 -code_const scomp
  29.113 -  (Eval infixl 3 "#->")
  29.114 +code_printing
  29.115 +  constant scomp \<rightharpoonup> (Eval) infixl 3 "#->"
  29.116  
  29.117  no_notation fcomp (infixl "\<circ>>" 60)
  29.118  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    30.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Jun 23 21:16:06 2013 +0200
    30.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Jun 23 21:16:07 2013 +0200
    30.3 @@ -518,10 +518,11 @@
    30.4  axiomatization throw_Counterexample :: "term list => unit"
    30.5  axiomatization catch_Counterexample :: "unit => term list option"
    30.6  
    30.7 -code_const throw_Counterexample
    30.8 -  (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
    30.9 -code_const catch_Counterexample
   30.10 -  (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
   30.11 +code_printing
   30.12 +  constant throw_Counterexample \<rightharpoonup>
   30.13 +    (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
   30.14 +| constant catch_Counterexample \<rightharpoonup>
   30.15 +    (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
   30.16  
   30.17  subsection {* Continuation passing style functions as plus monad *}
   30.18    
    31.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:06 2013 +0200
    31.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Sun Jun 23 21:16:07 2013 +0200
    31.3 @@ -13,14 +13,10 @@
    31.4  
    31.5  setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
    31.6  
    31.7 -code_type typerep
    31.8 -  (Haskell_Quickcheck "Typerep")
    31.9 -
   31.10 -code_const Typerep.Typerep
   31.11 -  (Haskell_Quickcheck "Typerep")
   31.12 -
   31.13 -code_type integer
   31.14 -  (Haskell_Quickcheck "Prelude.Int")
   31.15 +code_printing
   31.16 +  type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
   31.17 +| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
   31.18 +| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
   31.19  
   31.20  code_reserved Haskell_Quickcheck Typerep
   31.21  
   31.22 @@ -47,19 +43,19 @@
   31.23  
   31.24  consts nth :: "'a list => integer => 'a"
   31.25  
   31.26 -code_const nth (Haskell_Quickcheck infixl 9  "!!")
   31.27 +code_printing constant nth \<rightharpoonup> (Haskell_Quickcheck) infixl 9 "!!"
   31.28  
   31.29  consts error :: "char list => 'a"
   31.30  
   31.31 -code_const error (Haskell_Quickcheck "error")
   31.32 +code_printing constant error \<rightharpoonup> (Haskell_Quickcheck) "error"
   31.33  
   31.34  consts toEnum :: "integer => char"
   31.35  
   31.36 -code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
   31.37 +code_printing constant toEnum \<rightharpoonup> (Haskell_Quickcheck) "Prelude.toEnum"
   31.38  
   31.39  consts marker :: "char"
   31.40  
   31.41 -code_const marker (Haskell_Quickcheck "''\\0'")
   31.42 +code_printing constant marker \<rightharpoonup> (Haskell_Quickcheck) "''\\0'"
   31.43  
   31.44  subsubsection {* Narrowing's basic operations *}
   31.45  
    32.1 --- a/src/HOL/Quickcheck_Random.thy	Sun Jun 23 21:16:06 2013 +0200
    32.2 +++ b/src/HOL/Quickcheck_Random.thy	Sun Jun 23 21:16:07 2013 +0200
    32.3 @@ -15,8 +15,8 @@
    32.4  
    32.5  axiomatization catch_match :: "'a => 'a => 'a"
    32.6  
    32.7 -code_const catch_match 
    32.8 -  (Quickcheck "((_) handle Match => _)")
    32.9 +code_printing
   32.10 +  constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
   32.11  
   32.12  subsection {* The @{text random} class *}
   32.13  
   32.14 @@ -212,7 +212,8 @@
   32.15  
   32.16  subsection {* Code setup *}
   32.17  
   32.18 -code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
   32.19 +code_printing
   32.20 +  constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
   32.21    -- {* With enough criminal energy this can be abused to derive @{prop False};
   32.22    for this reason we use a distinguished target @{text Quickcheck}
   32.23    not spoiling the regular trusted code generation *}
    33.1 --- a/src/HOL/Rings.thy	Sun Jun 23 21:16:06 2013 +0200
    33.2 +++ b/src/HOL/Rings.thy	Sun Jun 23 21:16:07 2013 +0200
    33.3 @@ -1149,13 +1149,8 @@
    33.4  
    33.5  end
    33.6  
    33.7 -code_modulename SML
    33.8 -  Rings Arith
    33.9 -
   33.10 -code_modulename OCaml
   33.11 -  Rings Arith
   33.12 -
   33.13 -code_modulename Haskell
   33.14 -  Rings Arith
   33.15 +code_identifier
   33.16 +  code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   33.17  
   33.18  end
   33.19 +
    34.1 --- a/src/HOL/Semiring_Normalization.thy	Sun Jun 23 21:16:06 2013 +0200
    34.2 +++ b/src/HOL/Semiring_Normalization.thy	Sun Jun 23 21:16:07 2013 +0200
    34.3 @@ -219,13 +219,7 @@
    34.4  
    34.5  hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
    34.6  
    34.7 -code_modulename SML
    34.8 -  Semiring_Normalization Arith
    34.9 -
   34.10 -code_modulename OCaml
   34.11 -  Semiring_Normalization Arith
   34.12 -
   34.13 -code_modulename Haskell
   34.14 -  Semiring_Normalization Arith
   34.15 +code_identifier
   34.16 +  code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
   34.17  
   34.18  end
    35.1 --- a/src/HOL/String.thy	Sun Jun 23 21:16:06 2013 +0200
    35.2 +++ b/src/HOL/String.thy	Sun Jun 23 21:16:07 2013 +0200
    35.3 @@ -400,24 +400,25 @@
    35.4  code_reserved OCaml string
    35.5  code_reserved Scala string
    35.6  
    35.7 -code_type literal
    35.8 -  (SML "string")
    35.9 -  (OCaml "string")
   35.10 -  (Haskell "String")
   35.11 -  (Scala "String")
   35.12 +code_printing
   35.13 +  type_constructor literal \<rightharpoonup>
   35.14 +    (SML) "string"
   35.15 +    and (OCaml) "string"
   35.16 +    and (Haskell) "String"
   35.17 +    and (Scala) "String"
   35.18  
   35.19  setup {*
   35.20    fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
   35.21  *}
   35.22  
   35.23 -code_instance literal :: equal
   35.24 -  (Haskell -)
   35.25 -
   35.26 -code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   35.27 -  (SML "!((_ : string) = _)")
   35.28 -  (OCaml "!((_ : string) = _)")
   35.29 -  (Haskell infix 4 "==")
   35.30 -  (Scala infixl 5 "==")
   35.31 +code_printing
   35.32 +  class_instance literal :: equal \<rightharpoonup>
   35.33 +    (Haskell) -
   35.34 +| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
   35.35 +    (SML) "!((_ : string) = _)"
   35.36 +    and (OCaml) "!((_ : string) = _)"
   35.37 +    and (Haskell) infix 4 "=="
   35.38 +    and (Scala) infixl 5 "=="
   35.39  
   35.40  hide_type (open) literal
   35.41  
    36.1 --- a/src/HOL/Tools/numeral.ML	Sun Jun 23 21:16:06 2013 +0200
    36.2 +++ b/src/HOL/Tools/numeral.ML	Sun Jun 23 21:16:07 2013 +0200
    36.3 @@ -81,9 +81,9 @@
    36.4      fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
    36.5        (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
    36.6    in
    36.7 -    thy |> Code_Target.add_const_syntax target number_of
    36.8 -      (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Num.One},
    36.9 -        @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))
   36.10 +    thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
   36.11 +      [(target, SOME (Code_Printer.complex_const_syntax
   36.12 +        (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
   36.13    end;
   36.14  
   36.15  end; (*local*)
    37.1 --- a/src/HOL/Tools/string_code.ML	Sun Jun 23 21:16:06 2013 +0200
    37.2 +++ b/src/HOL/Tools/string_code.ML	Sun Jun 23 21:16:07 2013 +0200
    37.3 @@ -58,8 +58,9 @@
    37.4                    Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
    37.5          | NONE =>
    37.6              List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    37.7 -  in Code_Target.add_const_syntax target
    37.8 -    @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
    37.9 +  in
   37.10 +    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
   37.11 +      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
   37.12    end;
   37.13  
   37.14  fun add_literal_char target =
   37.15 @@ -68,8 +69,9 @@
   37.16        case decode_char nibbles' (t1, t2)
   37.17         of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
   37.18          | NONE => Code_Printer.eqn_error thm "Illegal character expression";
   37.19 -  in Code_Target.add_const_syntax target
   37.20 -    @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
   37.21 +  in
   37.22 +    Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
   37.23 +      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
   37.24    end;
   37.25  
   37.26  fun add_literal_string target =
   37.27 @@ -80,8 +82,9 @@
   37.28               of SOME p => p
   37.29                | NONE => Code_Printer.eqn_error thm "Illegal message expression")
   37.30          | NONE => Code_Printer.eqn_error thm "Illegal message expression";
   37.31 -  in Code_Target.add_const_syntax target 
   37.32 -    @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
   37.33 +  in
   37.34 +    Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
   37.35 +      [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
   37.36    end;
   37.37  
   37.38  end;
    38.1 --- a/src/HOL/Typerep.thy	Sun Jun 23 21:16:06 2013 +0200
    38.2 +++ b/src/HOL/Typerep.thy	Sun Jun 23 21:16:07 2013 +0200
    38.3 @@ -87,11 +87,9 @@
    38.4    "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
    38.5    by (fact equal_refl)
    38.6  
    38.7 -code_type typerep
    38.8 -  (Eval "Term.typ")
    38.9 -
   38.10 -code_const Typerep
   38.11 -  (Eval "Term.Type/ (_, _)")
   38.12 +code_printing
   38.13 +  type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
   38.14 +| constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
   38.15  
   38.16  code_reserved Eval Term
   38.17  
    39.1 --- a/src/Tools/Code/code_haskell.ML	Sun Jun 23 21:16:06 2013 +0200
    39.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Jun 23 21:16:07 2013 +0200
    39.3 @@ -465,8 +465,8 @@
    39.4      val c_bind = Code.read_const thy raw_c_bind;
    39.5    in if target = target' then
    39.6      thy
    39.7 -    |> Code_Target.add_const_syntax target c_bind
    39.8 -        (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
    39.9 +    |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
   39.10 +      SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
   39.11    else error "Only Haskell target allows for monad syntax" end;
   39.12  
   39.13  
   39.14 @@ -484,12 +484,13 @@
   39.15          make_command = fn module_name =>
   39.16            "\"$ISABELLE_GHC\" " ^ language_params  ^ " -odir build -hidir build -stubdir build -e \"\" " ^
   39.17              module_name ^ ".hs" } })
   39.18 -  #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   39.19 +  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   39.20 +    [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   39.21        brackify_infix (1, R) fxy (
   39.22          print_typ (INFX (1, X)) ty1,
   39.23          str "->",
   39.24          print_typ (INFX (1, R)) ty2
   39.25 -      )))
   39.26 +      )))]))
   39.27    #> fold (Code_Target.add_reserved target) [
   39.28        "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
   39.29        "import", "default", "forall", "let", "in", "class", "qualified", "data",
    40.1 --- a/src/Tools/Code/code_ml.ML	Sun Jun 23 21:16:06 2013 +0200
    40.2 +++ b/src/Tools/Code/code_ml.ML	Sun Jun 23 21:16:07 2013 +0200
    40.3 @@ -823,6 +823,13 @@
    40.4  
    40.5  (** Isar setup **)
    40.6  
    40.7 +fun fun_syntax print_typ fxy [ty1, ty2] =
    40.8 +  brackify_infix (1, R) fxy (
    40.9 +    print_typ (INFX (1, X)) ty1,
   40.10 +    str "->",
   40.11 +    print_typ (INFX (1, R)) ty2
   40.12 +  );
   40.13 +
   40.14  val setup =
   40.15    Code_Target.add_target
   40.16      (target_SML, { serializer = serializer_sml, literals = literals_sml,
   40.17 @@ -835,18 +842,8 @@
   40.18        check = { env_var = "ISABELLE_OCAML",
   40.19          make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
   40.20          make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
   40.21 -  #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   40.22 -      brackify_infix (1, R) fxy (
   40.23 -        print_typ (INFX (1, X)) ty1,
   40.24 -        str "->",
   40.25 -        print_typ (INFX (1, R)) ty2
   40.26 -      )))
   40.27 -  #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   40.28 -      brackify_infix (1, R) fxy (
   40.29 -        print_typ (INFX (1, X)) ty1,
   40.30 -        str "->",
   40.31 -        print_typ (INFX (1, R)) ty2
   40.32 -      )))
   40.33 +  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   40.34 +    [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
   40.35    #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
   40.36    #> fold (Code_Target.add_reserved target_SML)
   40.37        ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
    41.1 --- a/src/Tools/Code/code_runtime.ML	Sun Jun 23 21:16:06 2013 +0200
    41.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Jun 23 21:16:07 2013 +0200
    41.3 @@ -53,10 +53,10 @@
    41.4  
    41.5  val _ = Context.>> (Context.map_theory
    41.6    (Code_Target.extend_target (target, (Code_ML.target_SML, K I))
    41.7 -  #> Code_Target.add_tyco_syntax target @{type_name prop}
    41.8 -       (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
    41.9 -  #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds}
   41.10 -       (SOME (Code_Printer.plain_const_syntax s_Holds))
   41.11 +  #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
   41.12 +    [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
   41.13 +  #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
   41.14 +    [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
   41.15    #> Code_Target.add_reserved target this
   41.16    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
   41.17         (*avoid further pervasive infix names*)
   41.18 @@ -287,7 +287,7 @@
   41.19            Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   41.20    in
   41.21      thy
   41.22 -    |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
   41.23 +    |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
   41.24    end;
   41.25  
   41.26  fun add_eval_constr (const, const') thy =
   41.27 @@ -297,11 +297,12 @@
   41.28        (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
   41.29    in
   41.30      thy
   41.31 -    |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
   41.32 +    |> Code_Target.set_printings (Code_Symbol.Constant (const,
   41.33 +      [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
   41.34    end;
   41.35  
   41.36 -fun add_eval_const (const, const') = Code_Target.add_const_syntax target
   41.37 -  const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
   41.38 +fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
   41.39 +  (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
   41.40  
   41.41  fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
   41.42        thy
   41.43 @@ -431,8 +432,8 @@
   41.44    |> Code_Target.add_reserved target ml_name
   41.45    |> Specification.axiomatization [(b, SOME T, NoSyn)] []
   41.46    |-> (fn ([Const (const, _)], _) =>
   41.47 -     Code_Target.add_const_syntax target const
   41.48 -       (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
   41.49 +    Code_Target.set_printings (Code_Symbol.Constant (const,
   41.50 +      [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   41.51    #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
   41.52  
   41.53  fun process_file filepath (definienda, thy) =
    42.1 --- a/src/Tools/Code/code_scala.ML	Sun Jun 23 21:16:06 2013 +0200
    42.2 +++ b/src/Tools/Code/code_scala.ML	Sun Jun 23 21:16:07 2013 +0200
    42.3 @@ -413,13 +413,13 @@
    42.4          make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
    42.5          make_command = fn _ =>
    42.6            "env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
    42.7 -  #> Code_Target.add_tyco_syntax target "fun"
    42.8 -     (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    42.9 -        brackify_infix (1, R) fxy (
   42.10 -          print_typ BR ty1 (*product type vs. tupled arguments!*),
   42.11 -          str "=>",
   42.12 -          print_typ (INFX (1, R)) ty2
   42.13 -        )))
   42.14 +  #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
   42.15 +    [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   42.16 +      brackify_infix (1, R) fxy (
   42.17 +        print_typ BR ty1 (*product type vs. tupled arguments!*),
   42.18 +        str "=>",
   42.19 +        print_typ (INFX (1, R)) ty2
   42.20 +      )))]))
   42.21    #> fold (Code_Target.add_reserved target) [
   42.22        "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   42.23        "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
    43.1 --- a/src/Tools/Code/code_target.ML	Sun Jun 23 21:16:06 2013 +0200
    43.2 +++ b/src/Tools/Code/code_target.ML	Sun Jun 23 21:16:07 2013 +0200
    43.3 @@ -515,7 +515,7 @@
    43.4    in union (op =) cs3 cs1 end;
    43.5  
    43.6  fun prep_destination "" = NONE
    43.7 -  | prep_destination "-" = NONE
    43.8 +  | prep_destination "-" = (legacy_feature "drop \"file\" argument entirely instead of \"-\""; NONE)
    43.9    | prep_destination s = SOME (Path.explode s);
   43.10  
   43.11  fun export_code thy cs seris =
   43.12 @@ -638,8 +638,13 @@
   43.13  val set_identifiers = gen_set_identifiers cert_name_decls;
   43.14  val set_identifiers_cmd = gen_set_identifiers read_name_decls;
   43.15  
   43.16 -fun add_module_alias_cmd target = fold (fn (sym, name) =>
   43.17 -  set_identifier (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))));
   43.18 +fun add_module_alias_cmd target aliasses =
   43.19 +  let
   43.20 +    val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
   43.21 +  in
   43.22 +    fold (fn (sym, name) => set_identifier
   43.23 +      (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses
   43.24 +  end;
   43.25  
   43.26  
   43.27  (* custom printings *)
   43.28 @@ -670,6 +675,7 @@
   43.29  
   43.30  fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
   43.31    let
   43.32 +    val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
   43.33      val x = prep_x thy raw_x;
   43.34    in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end;
   43.35