migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
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 +code_printing
4.51 + constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
4.52 + (SML) "IntInf.+ ((_), (_))"
4.53 + and (OCaml) "Big'_int.add'_big'_int"
4.54 + and (Haskell) infixl 6 "+"
4.55 + and (Scala) infixl 7 "+"
4.56 + and (Eval) infixl 8 "+"
4.57 +| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
4.58 + (SML) "IntInf.~"
4.59 + and (OCaml) "Big'_int.minus'_big'_int"
4.60 + and (Haskell) "negate"
4.61 + and (Scala) "!(- _)"
4.62 + and (Eval) "~/ _"
4.63 +| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
4.64 + (SML) "IntInf.- ((_), (_))"
4.65 + and (OCaml) "Big'_int.sub'_big'_int"
4.66 + and (Haskell) infixl 6 "-"
4.67 + and (Scala) infixl 7 "-"
4.68 + and (Eval) infixl 8 "-"
4.69 +| constant Code_Numeral.dup \<rightharpoonup>
4.70 + (SML) "IntInf.*/ (2,/ (_))"
4.71 + and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
4.72 + and (Haskell) "!(2 * _)"
4.73 + and (Scala) "!(2 * _)"
4.74 + and (Eval) "!(2 * _)"
4.75 +| constant Code_Numeral.sub \<rightharpoonup>
4.76 + (SML) "!(raise/ Fail/ \"sub\")"
4.77 + and (OCaml) "failwith/ \"sub\""
4.78 + and (Haskell) "error/ \"sub\""
4.79 + and (Scala) "!sys.error(\"sub\")"
4.80 +| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
4.81 + (SML) "IntInf.* ((_), (_))"
4.82 + and (OCaml) "Big'_int.mult'_big'_int"
4.83 + and (Haskell) infixl 7 "*"
4.84 + and (Scala) infixl 8 "*"
4.85 + and (Eval) infixl 9 "*"
4.86 +| constant Code_Numeral.divmod_abs \<rightharpoonup>
4.87 + (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
4.88 + and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
4.89 + and (Haskell) "divMod/ (abs _)/ (abs _)"
4.90 + and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
4.91 + and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
4.92 +| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
4.93 + (SML) "!((_ : IntInf.int) = _)"
4.94 + and (OCaml) "Big'_int.eq'_big'_int"
4.95 + and (Haskell) infix 4 "=="
4.96 + and (Scala) infixl 5 "=="
4.97 + and (Eval) infixl 6 "="
4.98 +| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
4.99 + (SML) "IntInf.<= ((_), (_))"
4.100 + and (OCaml) "Big'_int.le'_big'_int"
4.101 + and (Haskell) infix 4 "<="
4.102 + and (Scala) infixl 4 "<="
4.103 + and (Eval) infixl 6 "<="
4.104 +| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
4.105 + (SML) "IntInf.< ((_), (_))"
4.106 + and (OCaml) "Big'_int.lt'_big'_int"
4.107 + and (Haskell) infix 4 "<"
4.108 + and (Scala) infixl 4 "<"
4.109 + and (Eval) infixl 6 "<"
4.110
4.111 -code_const "uminus :: integer \<Rightarrow> _"
4.112 - (SML "IntInf.~")
4.113 - (OCaml "Big'_int.minus'_big'_int")
4.114 - (Haskell "negate")
4.115 - (Scala "!(- _)")
4.116 - (Eval "~/ _")
4.117 -
4.118 -code_const "minus :: integer \<Rightarrow> _"
4.119 - (SML "IntInf.- ((_), (_))")
4.120 - (OCaml "Big'_int.sub'_big'_int")
4.121 - (Haskell infixl 6 "-")
4.122 - (Scala infixl 7 "-")
4.123 - (Eval infixl 8 "-")
4.124 -
4.125 -code_const Code_Numeral.dup
4.126 - (SML "IntInf.*/ (2,/ (_))")
4.127 - (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
4.128 - (Haskell "!(2 * _)")
4.129 - (Scala "!(2 * _)")
4.130 - (Eval "!(2 * _)")
4.131 -
4.132 -code_const Code_Numeral.sub
4.133 - (SML "!(raise/ Fail/ \"sub\")")
4.134 - (OCaml "failwith/ \"sub\"")
4.135 - (Haskell "error/ \"sub\"")
4.136 - (Scala "!sys.error(\"sub\")")
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