migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
--- a/NEWS Sun Jun 23 21:16:06 2013 +0200
+++ b/NEWS Sun Jun 23 21:16:07 2013 +0200
@@ -68,6 +68,12 @@
*** HOL ***
+* Code generator:
+ * 'code_printing' unifies 'code_const' / 'code_type' / 'code_class' / 'code_instance'.
+ * 'code_identifier' declares name hints for arbitrary identifiers in generated code,
+ subsuming 'code_modulename'.
+ See the Isar reference manual for syntax diagrams, and the HOL theories for examples.
+
* Library/Polynomial.thy:
* Use lifting for primitive definitions.
* Explicit conversions from and to lists of coefficients, used for generated code.
--- a/src/Doc/IsarRef/HOL_Specific.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Sun Jun 23 21:16:07 2013 +0200
@@ -2224,7 +2224,7 @@
@{rail "
@@{command (HOL) export_code} ( constexpr + ) \\
( ( @'in' target ( @'module_name' @{syntax string} ) ? \\
- ( @'file' ( @{syntax string} | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
+ ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
;
const: @{syntax term}
--- a/src/HOL/Code_Evaluation.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Code_Evaluation.thy Sun Jun 23 21:16:07 2013 +0200
@@ -125,18 +125,14 @@
(Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
by (subst term_of_anything) rule
-code_type "term"
- (Eval "Term.term")
-
-code_const Const and App and Abs and Free
- (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))"
- and "Term.Free/ ((_), (_))")
-
-code_const "term_of \<Colon> integer \<Rightarrow> term"
- (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT")
-
-code_const "term_of \<Colon> String.literal \<Rightarrow> term"
- (Eval "HOLogic.mk'_literal")
+code_printing
+ type_constructor "term" \<rightharpoonup> (Eval) "Term.term"
+| constant Const \<rightharpoonup> (Eval) "Term.Const/ ((_), (_))"
+| constant App \<rightharpoonup> (Eval) "Term.$/ ((_), (_))"
+| constant Abs \<rightharpoonup> (Eval) "Term.Abs/ ((_), (_), (_))"
+| constant Free \<rightharpoonup> (Eval) "Term.Free/ ((_), (_))"
+| constant "term_of \<Colon> integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
+| constant "term_of \<Colon> String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
code_reserved Eval HOLogic
@@ -161,8 +157,8 @@
definition tracing :: "String.literal \<Rightarrow> 'a \<Rightarrow> 'a" where
[code del]: "tracing s x = x"
-code_const "tracing :: String.literal => 'a => 'a"
- (Eval "Code'_Evaluation.tracing")
+code_printing
+ constant "tracing :: String.literal => 'a => 'a" \<rightharpoonup> (Eval) "Code'_Evaluation.tracing"
subsection {* Generic reification *}
--- a/src/HOL/Code_Numeral.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Code_Numeral.thy Sun Jun 23 21:16:07 2013 +0200
@@ -519,21 +519,22 @@
code_reserved Eval int Integer abs
-code_type integer
- (SML "IntInf.int")
- (OCaml "Big'_int.big'_int")
- (Haskell "Integer")
- (Scala "BigInt")
- (Eval "int")
+code_printing
+ type_constructor integer \<rightharpoonup>
+ (SML) "IntInf.int"
+ and (OCaml) "Big'_int.big'_int"
+ and (Haskell) "Integer"
+ and (Scala) "BigInt"
+ and (Eval) "int"
+| class_instance integer :: equal \<rightharpoonup>
+ (Haskell) -
-code_instance integer :: equal
- (Haskell -)
-
-code_const "0::integer"
- (SML "0")
- (OCaml "Big'_int.zero'_big'_int")
- (Haskell "0")
- (Scala "BigInt(0)")
+code_printing
+ constant "0::integer" \<rightharpoonup>
+ (SML) "0"
+ and (OCaml) "Big'_int.zero'_big'_int"
+ and (Haskell) "0"
+ and (Scala) "BigInt(0)"
setup {*
fold (Numeral.add_code @{const_name Code_Numeral.Pos}
@@ -545,83 +546,69 @@
true Code_Printer.literal_numeral) ["SML", "OCaml", "Haskell", "Scala"]
*}
-code_const "plus :: integer \<Rightarrow> _ \<Rightarrow> _"
- (SML "IntInf.+ ((_), (_))")
- (OCaml "Big'_int.add'_big'_int")
- (Haskell infixl 6 "+")
- (Scala infixl 7 "+")
- (Eval infixl 8 "+")
-
-code_const "uminus :: integer \<Rightarrow> _"
- (SML "IntInf.~")
- (OCaml "Big'_int.minus'_big'_int")
- (Haskell "negate")
- (Scala "!(- _)")
- (Eval "~/ _")
-
-code_const "minus :: integer \<Rightarrow> _"
- (SML "IntInf.- ((_), (_))")
- (OCaml "Big'_int.sub'_big'_int")
- (Haskell infixl 6 "-")
- (Scala infixl 7 "-")
- (Eval infixl 8 "-")
-
-code_const Code_Numeral.dup
- (SML "IntInf.*/ (2,/ (_))")
- (OCaml "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)")
- (Haskell "!(2 * _)")
- (Scala "!(2 * _)")
- (Eval "!(2 * _)")
-
-code_const Code_Numeral.sub
- (SML "!(raise/ Fail/ \"sub\")")
- (OCaml "failwith/ \"sub\"")
- (Haskell "error/ \"sub\"")
- (Scala "!sys.error(\"sub\")")
+code_printing
+ constant "plus :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
+ (SML) "IntInf.+ ((_), (_))"
+ and (OCaml) "Big'_int.add'_big'_int"
+ and (Haskell) infixl 6 "+"
+ and (Scala) infixl 7 "+"
+ and (Eval) infixl 8 "+"
+| constant "uminus :: integer \<Rightarrow> _" \<rightharpoonup>
+ (SML) "IntInf.~"
+ and (OCaml) "Big'_int.minus'_big'_int"
+ and (Haskell) "negate"
+ and (Scala) "!(- _)"
+ and (Eval) "~/ _"
+| constant "minus :: integer \<Rightarrow> _" \<rightharpoonup>
+ (SML) "IntInf.- ((_), (_))"
+ and (OCaml) "Big'_int.sub'_big'_int"
+ and (Haskell) infixl 6 "-"
+ and (Scala) infixl 7 "-"
+ and (Eval) infixl 8 "-"
+| constant Code_Numeral.dup \<rightharpoonup>
+ (SML) "IntInf.*/ (2,/ (_))"
+ and (OCaml) "Big'_int.mult'_big'_int/ (Big'_int.big'_int'_of'_int/ 2)"
+ and (Haskell) "!(2 * _)"
+ and (Scala) "!(2 * _)"
+ and (Eval) "!(2 * _)"
+| constant Code_Numeral.sub \<rightharpoonup>
+ (SML) "!(raise/ Fail/ \"sub\")"
+ and (OCaml) "failwith/ \"sub\""
+ and (Haskell) "error/ \"sub\""
+ and (Scala) "!sys.error(\"sub\")"
+| constant "times :: integer \<Rightarrow> _ \<Rightarrow> _" \<rightharpoonup>
+ (SML) "IntInf.* ((_), (_))"
+ and (OCaml) "Big'_int.mult'_big'_int"
+ and (Haskell) infixl 7 "*"
+ and (Scala) infixl 8 "*"
+ and (Eval) infixl 9 "*"
+| constant Code_Numeral.divmod_abs \<rightharpoonup>
+ (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)"
+ and (OCaml) "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)"
+ and (Haskell) "divMod/ (abs _)/ (abs _)"
+ and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))"
+ and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)"
+| constant "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : IntInf.int) = _)"
+ and (OCaml) "Big'_int.eq'_big'_int"
+ and (Haskell) infix 4 "=="
+ and (Scala) infixl 5 "=="
+ and (Eval) infixl 6 "="
+| constant "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "IntInf.<= ((_), (_))"
+ and (OCaml) "Big'_int.le'_big'_int"
+ and (Haskell) infix 4 "<="
+ and (Scala) infixl 4 "<="
+ and (Eval) infixl 6 "<="
+| constant "less :: integer \<Rightarrow> _ \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "IntInf.< ((_), (_))"
+ and (OCaml) "Big'_int.lt'_big'_int"
+ and (Haskell) infix 4 "<"
+ and (Scala) infixl 4 "<"
+ and (Eval) infixl 6 "<"
-code_const "times :: integer \<Rightarrow> _ \<Rightarrow> _"
- (SML "IntInf.* ((_), (_))")
- (OCaml "Big'_int.mult'_big'_int")
- (Haskell infixl 7 "*")
- (Scala infixl 8 "*")
- (Eval infixl 9 "*")
-
-code_const Code_Numeral.divmod_abs
- (SML "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)")
- (OCaml "Big'_int.quomod'_big'_int/ (Big'_int.abs'_big'_int _)/ (Big'_int.abs'_big'_int _)")
- (Haskell "divMod/ (abs _)/ (abs _)")
- (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
- (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
-
-code_const "HOL.equal :: integer \<Rightarrow> _ \<Rightarrow> bool"
- (SML "!((_ : IntInf.int) = _)")
- (OCaml "Big'_int.eq'_big'_int")
- (Haskell infix 4 "==")
- (Scala infixl 5 "==")
- (Eval infixl 6 "=")
-
-code_const "less_eq :: integer \<Rightarrow> _ \<Rightarrow> bool"
- (SML "IntInf.<= ((_), (_))")
- (OCaml "Big'_int.le'_big'_int")
- (Haskell infix 4 "<=")
- (Scala infixl 4 "<=")
- (Eval infixl 6 "<=")
-
-code_const "less :: integer \<Rightarrow> _ \<Rightarrow> bool"
- (SML "IntInf.< ((_), (_))")
- (OCaml "Big'_int.lt'_big'_int")
- (Haskell infix 4 "<")
- (Scala infixl 4 "<")
- (Eval infixl 6 "<")
-
-code_modulename SML
- Code_Numeral Arith
-
-code_modulename OCaml
- Code_Numeral Arith
-
-code_modulename Haskell
- Code_Numeral Arith
+code_identifier
+ code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
subsection {* Type of target language naturals *}
--- a/src/HOL/Divides.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Divides.thy Sun Jun 23 21:16:07 2013 +0200
@@ -2381,13 +2381,8 @@
then show ?thesis by (simp add: divmod_int_pdivmod)
qed
-code_modulename SML
- Divides Arith
-
-code_modulename OCaml
- Divides Arith
-
-code_modulename Haskell
- Divides Arith
+code_identifier
+ code_module Divides \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
+
--- a/src/HOL/Enum.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Enum.thy Sun Jun 23 21:16:07 2013 +0200
@@ -117,7 +117,9 @@
qed
code_abort enum_the
-code_const enum_the (Eval "(fn p => raise Match)")
+
+code_printing
+ constant enum_the \<rightharpoonup> (Eval) "(fn '_ => raise Match)"
subsubsection {* Equality and order on functions *}
--- a/src/HOL/Fields.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Fields.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1176,13 +1176,7 @@
end
-code_modulename SML
- Fields Arith
-
-code_modulename OCaml
- Fields Arith
-
-code_modulename Haskell
- Fields Arith
+code_identifier
+ code_module Fields \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/Fun.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Fun.thy Sun Jun 23 21:16:07 2013 +0200
@@ -29,6 +29,9 @@
lemma vimage_id [simp]: "vimage id = id"
by (simp add: id_def fun_eq_iff)
+code_printing
+ constant id \<rightharpoonup> (Haskell) "id"
+
subsection {* The Composition Operator @{text "f \<circ> g"} *}
@@ -77,6 +80,9 @@
"SUPR A (g \<circ> f) = SUPR (f ` A) g"
by (simp add: SUP_def image_comp)
+code_printing
+ constant comp \<rightharpoonup> (SML) infixl 5 "o" and (Haskell) infixr 9 "."
+
subsection {* The Forward Composition Operator @{text fcomp} *}
@@ -95,8 +101,8 @@
lemma fcomp_id [simp]: "f \<circ>> id = f"
by (simp add: fcomp_def)
-code_const fcomp
- (Eval infixl 1 "#>")
+code_printing
+ constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
no_notation fcomp (infixl "\<circ>>" 60)
@@ -814,16 +820,6 @@
*}
-subsubsection {* Code generator *}
-
-code_const "op \<circ>"
- (SML infixl 5 "o")
- (Haskell infixr 9 ".")
-
-code_const "id"
- (Haskell "id")
-
-
subsubsection {* Functorial structure of types *}
ML_file "Tools/enriched_type.ML"
--- a/src/HOL/Groups.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Groups.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1359,14 +1359,8 @@
by (auto intro: add_strict_right_mono add_strict_left_mono
add_less_le_mono add_le_less_mono add_strict_mono)
-code_modulename SML
- Groups Arith
-
-code_modulename OCaml
- Groups Arith
-
-code_modulename Haskell
- Groups Arith
+code_identifier
+ code_module Groups \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
text {* Legacy *}
--- a/src/HOL/HOL.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/HOL.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1830,61 +1830,67 @@
text {* type @{typ bool} *}
-code_type bool
- (SML "bool")
- (OCaml "bool")
- (Haskell "Bool")
- (Scala "Boolean")
-
-code_const True and False and Not and HOL.conj and HOL.disj and HOL.implies and If
- (SML "true" and "false" and "not"
- and infixl 1 "andalso" and infixl 0 "orelse"
- and "!(if (_)/ then (_)/ else true)"
- and "!(if (_)/ then (_)/ else (_))")
- (OCaml "true" and "false" and "not"
- and infixl 3 "&&" and infixl 2 "||"
- and "!(if (_)/ then (_)/ else true)"
- and "!(if (_)/ then (_)/ else (_))")
- (Haskell "True" and "False" and "not"
- and infixr 3 "&&" and infixr 2 "||"
- and "!(if (_)/ then (_)/ else True)"
- and "!(if (_)/ then (_)/ else (_))")
- (Scala "true" and "false" and "'! _"
- and infixl 3 "&&" and infixl 1 "||"
- and "!(if ((_))/ (_)/ else true)"
- and "!(if ((_))/ (_)/ else (_))")
+code_printing
+ type_constructor bool \<rightharpoonup>
+ (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean"
+| constant True \<rightharpoonup>
+ (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true"
+| constant False \<rightharpoonup>
+ (SML) "false" and (OCaml) "false" and (Haskell) "False" and (Scala) "false"
code_reserved SML
- bool true false not
+ bool true false
code_reserved OCaml
- bool not
+ bool
code_reserved Scala
Boolean
-code_modulename SML Pure HOL
-code_modulename OCaml Pure HOL
-code_modulename Haskell Pure HOL
+code_printing
+ constant Not \<rightharpoonup>
+ (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _"
+| constant HOL.conj \<rightharpoonup>
+ (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&"
+| constant HOL.disj \<rightharpoonup>
+ (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||"
+| constant HOL.implies \<rightharpoonup>
+ (SML) "!(if (_)/ then (_)/ else true)"
+ and (OCaml) "!(if (_)/ then (_)/ else true)"
+ and (Haskell) "!(if (_)/ then (_)/ else True)"
+ and (Scala) "!(if ((_))/ (_)/ else true)"
+| constant If \<rightharpoonup>
+ (SML) "!(if (_)/ then (_)/ else (_))"
+ and (OCaml) "!(if (_)/ then (_)/ else (_))"
+ and (Haskell) "!(if (_)/ then (_)/ else (_))"
+ and (Scala) "!(if ((_))/ (_)/ else (_))"
+
+code_reserved SML
+ not
+
+code_reserved OCaml
+ not
+
+code_identifier
+ code_module Pure \<rightharpoonup>
+ (SML) HOL and (OCaml) HOL and (Haskell) HOL and (Scala) HOL
text {* using built-in Haskell equality *}
-code_class equal
- (Haskell "Eq")
-
-code_const "HOL.equal"
- (Haskell infix 4 "==")
-
-code_const HOL.eq
- (Haskell infix 4 "==")
+code_printing
+ type_class equal \<rightharpoonup> (Haskell) "Eq"
+| constant HOL.equal \<rightharpoonup> (Haskell) infix 4 "=="
+| constant HOL.eq \<rightharpoonup> (Haskell) infix 4 "=="
text {* undefined *}
-code_const undefined
- (SML "!(raise/ Fail/ \"undefined\")")
- (OCaml "failwith/ \"undefined\"")
- (Haskell "error/ \"undefined\"")
- (Scala "!sys.error(\"undefined\")")
+code_printing
+ constant undefined \<rightharpoonup>
+ (SML) "!(raise/ Fail/ \"undefined\")"
+ and (OCaml) "failwith/ \"undefined\""
+ and (Haskell) "error/ \"undefined\""
+ and (Scala) "!sys.error(\"undefined\")"
+
subsubsection {* Evaluation and normalization by evaluation *}
--- a/src/HOL/Imperative_HOL/Array.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy Sun Jun 23 21:16:07 2013 +0200
@@ -445,60 +445,60 @@
text {* SML *}
-code_type array (SML "_/ array")
-code_const Array (SML "raise/ (Fail/ \"bare Array\")")
-code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
-code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
-code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
-code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
-code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
-code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
-code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (SML infixl 6 "=")
+code_printing type_constructor array \<rightharpoonup> (SML) "_/ array"
+code_printing constant Array \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Array\")"
+code_printing constant Array.new' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))"
+code_printing constant Array.of_list \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.fromList/ _)"
+code_printing constant Array.make' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))"
+code_printing constant Array.len' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.length/ _)"
+code_printing constant Array.nth' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))"
+code_printing constant Array.upd' \<rightharpoonup> (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))"
+code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
code_reserved SML Array
text {* OCaml *}
-code_type array (OCaml "_/ array")
-code_const Array (OCaml "failwith/ \"bare Array\"")
-code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
-code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
-code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/
- (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))")
-code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
-code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
-code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
-code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (OCaml infixl 4 "=")
+code_printing type_constructor array \<rightharpoonup> (OCaml) "_/ array"
+code_printing constant Array \<rightharpoonup> (OCaml) "failwith/ \"bare Array\""
+code_printing constant Array.new' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)"
+code_printing constant Array.of_list \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)"
+code_printing constant Array.make' \<rightharpoonup> (OCaml)
+ "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))"
+code_printing constant Array.len' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))"
+code_printing constant Array.nth' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))"
+code_printing constant Array.upd' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)"
+code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
code_reserved OCaml Array
text {* Haskell *}
-code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
-code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "Heap.newArray")
-code_const Array.of_list (Haskell "Heap.newListArray")
-code_const Array.make' (Haskell "Heap.newFunArray")
-code_const Array.len' (Haskell "Heap.lengthArray")
-code_const Array.nth' (Haskell "Heap.readArray")
-code_const Array.upd' (Haskell "Heap.writeArray")
-code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Haskell infix 4 "==")
-code_instance array :: HOL.equal (Haskell -)
+code_printing type_constructor array \<rightharpoonup> (Haskell) "Heap.STArray/ Heap.RealWorld/ _"
+code_printing constant Array \<rightharpoonup> (Haskell) "error/ \"bare Array\""
+code_printing constant Array.new' \<rightharpoonup> (Haskell) "Heap.newArray"
+code_printing constant Array.of_list \<rightharpoonup> (Haskell) "Heap.newListArray"
+code_printing constant Array.make' \<rightharpoonup> (Haskell) "Heap.newFunArray"
+code_printing constant Array.len' \<rightharpoonup> (Haskell) "Heap.lengthArray"
+code_printing constant Array.nth' \<rightharpoonup> (Haskell) "Heap.readArray"
+code_printing constant Array.upd' \<rightharpoonup> (Haskell) "Heap.writeArray"
+code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
+code_printing class_instance array :: HOL.equal \<rightharpoonup> (Haskell) -
text {* Scala *}
-code_type array (Scala "!collection.mutable.ArraySeq[_]")
-code_const Array (Scala "!sys.error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.alloc((_))((_))")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.make((_))((_))")
-code_const Array.len' (Scala "('_: Unit)/ =>/ Array.len((_))")
-code_const Array.nth' (Scala "('_: Unit)/ =>/ Array.nth((_), (_))")
-code_const Array.upd' (Scala "('_: Unit)/ =>/ Array.upd((_), (_), (_))")
-code_const Array.freeze (Scala "('_: Unit)/ =>/ Array.freeze((_))")
-code_const "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" (Scala infixl 5 "==")
+code_printing type_constructor array \<rightharpoonup> (Scala) "!collection.mutable.ArraySeq[_]"
+code_printing constant Array \<rightharpoonup> (Scala) "!sys.error(\"bare Array\")"
+code_printing constant Array.new' \<rightharpoonup> (Scala) "('_: Unit)/ => / Array.alloc((_))((_))"
+code_printing constant Array.make' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.make((_))((_))"
+code_printing constant Array.len' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.len((_))"
+code_printing constant Array.nth' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.nth((_), (_))"
+code_printing constant Array.upd' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.upd((_), (_), (_))"
+code_printing constant Array.freeze \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.freeze((_))"
+code_printing constant "HOL.equal :: 'a array \<Rightarrow> 'a array \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Jun 23 21:16:07 2013 +0200
@@ -556,15 +556,15 @@
subsubsection {* SML and OCaml *}
-code_type Heap (SML "(unit/ ->/ _)")
-code_const bind (SML "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())")
-code_const return (SML "!(fn/ ()/ =>/ _)")
-code_const Heap_Monad.raise' (SML "!(raise/ Fail/ _)")
+code_printing type_constructor Heap \<rightharpoonup> (SML) "(unit/ ->/ _)"
+code_printing constant bind \<rightharpoonup> (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())"
+code_printing constant return \<rightharpoonup> (SML) "!(fn/ ()/ =>/ _)"
+code_printing constant Heap_Monad.raise' \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
-code_type Heap (OCaml "(unit/ ->/ _)")
-code_const bind (OCaml "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())")
-code_const return (OCaml "!(fun/ ()/ ->/ _)")
-code_const Heap_Monad.raise' (OCaml "failwith")
+code_printing type_constructor Heap \<rightharpoonup> (OCaml) "(unit/ ->/ _)"
+code_printing constant bind \<rightharpoonup> (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())"
+code_printing constant return \<rightharpoonup> (OCaml) "!(fun/ ()/ ->/ _)"
+code_printing constant Heap_Monad.raise' \<rightharpoonup> (OCaml) "failwith"
subsubsection {* Haskell *}
@@ -608,10 +608,10 @@
text {* Monad *}
-code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _")
+code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
code_monad bind Haskell
-code_const return (Haskell "return")
-code_const Heap_Monad.raise' (Haskell "error")
+code_printing constant return \<rightharpoonup> (Haskell) "return"
+code_printing constant Heap_Monad.raise' \<rightharpoonup> (Haskell) "error"
subsubsection {* Scala *}
@@ -653,10 +653,10 @@
code_reserved Scala Heap Ref Array
-code_type Heap (Scala "(Unit/ =>/ _)")
-code_const bind (Scala "Heap.bind")
-code_const return (Scala "('_: Unit)/ =>/ _")
-code_const Heap_Monad.raise' (Scala "!sys.error((_))")
+code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
+code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
+code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
+code_printing constant Heap_Monad.raise' \<rightharpoonup> (Scala) "!sys.error((_))"
subsubsection {* Target variants with less units *}
--- a/src/HOL/Imperative_HOL/Ref.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Sun Jun 23 21:16:07 2013 +0200
@@ -275,48 +275,49 @@
text {* SML / Eval *}
-code_type ref (SML "_/ ref")
-code_type ref (Eval "_/ Unsynchronized.ref")
-code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const ref' (SML "(fn/ ()/ =>/ ref/ _)")
-code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
-code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
-code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
-code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (SML infixl 6 "=")
+code_printing type_constructor ref \<rightharpoonup> (SML) "_/ ref"
+code_printing type_constructor ref \<rightharpoonup> (Eval) "_/ Unsynchronized.ref"
+code_printing constant Ref \<rightharpoonup> (SML) "raise/ (Fail/ \"bare Ref\")"
+code_printing constant ref' \<rightharpoonup> (SML) "(fn/ ()/ =>/ ref/ _)"
+code_printing constant ref' \<rightharpoonup> (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)"
+code_printing constant Ref.lookup \<rightharpoonup> (SML) "(fn/ ()/ =>/ !/ _)"
+code_printing constant Ref.update \<rightharpoonup> (SML) "(fn/ ()/ =>/ _/ :=/ _)"
+code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (SML) infixl 6 "="
code_reserved Eval Unsynchronized
text {* OCaml *}
-code_type ref (OCaml "_/ ref")
-code_const Ref (OCaml "failwith/ \"bare Ref\"")
-code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
-code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
-code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
-code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (OCaml infixl 4 "=")
+code_printing type_constructor ref \<rightharpoonup> (OCaml) "_/ ref"
+code_printing constant Ref \<rightharpoonup> (OCaml) "failwith/ \"bare Ref\""
+code_printing constant ref' \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ ref/ _)"
+code_printing constant Ref.lookup \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ !/ _)"
+code_printing constant Ref.update \<rightharpoonup> (OCaml) "(fun/ ()/ ->/ _/ :=/ _)"
+code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (OCaml) infixl 4 "="
code_reserved OCaml ref
text {* Haskell *}
-code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
-code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const ref' (Haskell "Heap.newSTRef")
-code_const Ref.lookup (Haskell "Heap.readSTRef")
-code_const Ref.update (Haskell "Heap.writeSTRef")
-code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Haskell infix 4 "==")
-code_instance ref :: HOL.equal (Haskell -)
+code_printing type_constructor ref \<rightharpoonup> (Haskell) "Heap.STRef/ Heap.RealWorld/ _"
+code_printing constant Ref \<rightharpoonup> (Haskell) "error/ \"bare Ref\""
+code_printing constant ref' \<rightharpoonup> (Haskell) "Heap.newSTRef"
+code_printing constant Ref.lookup \<rightharpoonup> (Haskell) "Heap.readSTRef"
+code_printing constant Ref.update \<rightharpoonup> (Haskell) "Heap.writeSTRef"
+code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
+code_printing class_instance ref :: HOL.equal \<rightharpoonup> (Haskell) -
text {* Scala *}
-code_type ref (Scala "!Ref[_]")
-code_const Ref (Scala "!sys.error(\"bare Ref\")")
-code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
-code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
-code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
-code_const "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" (Scala infixl 5 "==")
+code_printing type_constructor ref \<rightharpoonup> (Scala) "!Ref[_]"
+code_printing constant Ref \<rightharpoonup> (Scala) "!sys.error(\"bare Ref\")"
+code_printing constant ref' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref((_))"
+code_printing constant Ref.lookup \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.lookup((_))"
+code_printing constant Ref.update \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Ref.update((_), (_))"
+code_printing constant "HOL.equal :: 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" \<rightharpoonup> (Scala) infixl 5 "=="
end
+
--- a/src/HOL/Int.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Int.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1614,14 +1614,8 @@
text {* Serializer setup *}
-code_modulename SML
- Int Arith
-
-code_modulename OCaml
- Int Arith
-
-code_modulename Haskell
- Int Arith
+code_identifier
+ code_module Int \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
quickcheck_params [default_type = int]
--- a/src/HOL/Library/Code_Binary_Nat.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Binary_Nat.thy Sun Jun 23 21:16:07 2013 +0200
@@ -142,14 +142,9 @@
by (simp_all add: nat_of_num_numeral)
-code_modulename SML
- Code_Binary_Nat Arith
-
-code_modulename OCaml
- Code_Binary_Nat Arith
-
-code_modulename Haskell
- Code_Binary_Nat Arith
+code_identifier
+ code_module Code_Binary_Nat \<rightharpoonup>
+ (SML) Arith and (OCaml) Arith and (Haskell) Arith
hide_const (open) dup sub
--- a/src/HOL/Library/Code_Char.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Char.thy Sun Jun 23 21:16:07 2013 +0200
@@ -8,19 +8,28 @@
imports Main Char_ord
begin
-code_type char
- (SML "char")
- (OCaml "char")
- (Haskell "Prelude.Char")
- (Scala "Char")
+code_printing
+ type_constructor char \<rightharpoonup>
+ (SML) "char"
+ and (OCaml) "char"
+ and (Haskell) "Prelude.Char"
+ and (Scala) "Char"
setup {*
fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
#> String_Code.add_literal_list_string "Haskell"
*}
-code_instance char :: equal
- (Haskell -)
+code_printing
+ class_instance char :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : char) = _)"
+ and (OCaml) "!((_ : char) = _)"
+ and (Haskell) infix 4 "=="
+ and (Scala) infixl 5 "=="
+| constant "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term" \<rightharpoonup>
+ (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
code_reserved SML
char
@@ -31,32 +40,22 @@
code_reserved Scala
char
-code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) = _)")
- (OCaml "!((_ : char) = _)")
- (Haskell infix 4 "==")
- (Scala infixl 5 "==")
-
-code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
- (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
-
-
definition implode :: "string \<Rightarrow> String.literal" where
"implode = STR"
code_reserved SML String
-code_const implode
- (SML "String.implode")
- (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)")
- (Haskell "_")
- (Scala "!(\"\" ++/ _)")
-
-code_const explode
- (SML "String.explode")
- (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) [])")
- (Haskell "_")
- (Scala "!(_.toList)")
+code_printing
+ constant implode \<rightharpoonup>
+ (SML) "String.implode"
+ 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)"
+ and (Haskell) "_"
+ and (Scala) "!(\"\" ++/ _)"
+| constant explode \<rightharpoonup>
+ (SML) "String.explode"
+ 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) [])"
+ and (Haskell) "_"
+ and (Scala) "!(_.toList)"
definition integer_of_char :: "char \<Rightarrow> integer"
@@ -75,30 +74,29 @@
"char_of_nat = char_of_integer o integer_of_nat"
by (simp add: char_of_integer_def fun_eq_iff)
-code_const integer_of_char and char_of_integer
- (SML "!(IntInf.fromInt o Char.ord)"
- and "!(Char.chr o IntInf.toInt)")
- (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
- and "Char.chr (Big'_int.int'_of'_big'_int _)")
- (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
- and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
- (Scala "BigInt(_.toInt)"
- and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
-
-
-code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) <= _)")
- (OCaml "!((_ : char) <= _)")
- (Haskell infix 4 "<=")
- (Scala infixl 4 "<=")
- (Eval infixl 6 "<=")
-
-code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) < _)")
- (OCaml "!((_ : char) < _)")
- (Haskell infix 4 "<")
- (Scala infixl 4 "<")
- (Eval infixl 6 "<")
+code_printing
+ constant integer_of_char \<rightharpoonup>
+ (SML) "!(IntInf.fromInt o Char.ord)"
+ and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
+ and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
+ and (Scala) "BigInt(_.toInt)"
+| constant char_of_integer \<rightharpoonup>
+ (SML) "!(Char.chr o IntInf.toInt)"
+ and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
+ and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
+ and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))"
+| constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : char) <= _)"
+ and (OCaml) "!((_ : char) <= _)"
+ and (Haskell) infix 4 "<="
+ and (Scala) infixl 4 "<="
+ and (Eval) infixl 6 "<="
+| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : char) < _)"
+ and (OCaml) "!((_ : char) < _)"
+ and (Haskell) infix 4 "<"
+ and (Scala) infixl 4 "<"
+ and (Eval) infixl 6 "<"
end
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Jun 23 21:16:07 2013 +0200
@@ -14,61 +14,75 @@
The only legitimate use of this theory is as a tool for code generation
purposes. *}
-code_type real
- (SML "real")
- (OCaml "float")
+code_printing
+ type_constructor real \<rightharpoonup>
+ (SML) "real"
+ and (OCaml) "float"
-code_const Ratreal
- (SML "error/ \"Bad constant: Ratreal\"")
+code_printing
+ constant Ratreal \<rightharpoonup>
+ (SML) "error/ \"Bad constant: Ratreal\""
-code_const "0 :: real"
- (SML "0.0")
- (OCaml "0.0")
+code_printing
+ constant "0 :: real" \<rightharpoonup>
+ (SML) "0.0"
+ and (OCaml) "0.0"
declare zero_real_code[code_unfold del]
-code_const "1 :: real"
- (SML "1.0")
- (OCaml "1.0")
+code_printing
+ constant "1 :: real" \<rightharpoonup>
+ (SML) "1.0"
+ and (OCaml) "1.0"
declare one_real_code[code_unfold del]
-code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.== ((_), (_))")
- (OCaml "Pervasives.(=)")
+code_printing
+ constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.== ((_), (_))"
+ and (OCaml) "Pervasives.(=)"
-code_const "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.<= ((_), (_))")
- (OCaml "Pervasives.(<=)")
+code_printing
+ constant "Orderings.less_eq :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.<= ((_), (_))"
+ and (OCaml) "Pervasives.(<=)"
-code_const "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.< ((_), (_))")
- (OCaml "Pervasives.(<)")
+code_printing
+ constant "Orderings.less :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.< ((_), (_))"
+ and (OCaml) "Pervasives.(<)"
-code_const "op + :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.+ ((_), (_))")
- (OCaml "Pervasives.( +. )")
+code_printing
+ constant "op + :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.+ ((_), (_))"
+ and (OCaml) "Pervasives.( +. )"
-code_const "op * :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.* ((_), (_))")
- (OCaml "Pervasives.( *. )")
+code_printing
+ constant "op * :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.* ((_), (_))"
+ and (OCaml) "Pervasives.( *. )"
-code_const "op - :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.- ((_), (_))")
- (OCaml "Pervasives.( -. )")
+code_printing
+ constant "op - :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.- ((_), (_))"
+ and (OCaml) "Pervasives.( -. )"
-code_const "uminus :: real \<Rightarrow> real"
- (SML "Real.~")
- (OCaml "Pervasives.( ~-. )")
+code_printing
+ constant "uminus :: real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.~"
+ and (OCaml) "Pervasives.( ~-. )"
-code_const "op / :: real \<Rightarrow> real \<Rightarrow> real"
- (SML "Real.'/ ((_), (_))")
- (OCaml "Pervasives.( '/. )")
+code_printing
+ constant "op / :: real \<Rightarrow> real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Real.'/ ((_), (_))"
+ and (OCaml) "Pervasives.( '/. )"
-code_const "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool"
- (SML "Real.== ((_:real), (_))")
+code_printing
+ constant "HOL.equal :: real \<Rightarrow> real \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "Real.== ((_:real), (_))"
-code_const "sqrt :: real \<Rightarrow> real"
- (SML "Math.sqrt")
- (OCaml "Pervasives.sqrt")
+code_printing
+ constant "sqrt :: real \<Rightarrow> real" \<rightharpoonup>
+ (SML) "Math.sqrt"
+ and (OCaml) "Pervasives.sqrt"
declare sqrt_def[code del]
definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
@@ -76,55 +90,64 @@
lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
unfolding real_exp_def ..
-code_const real_exp
- (SML "Math.exp")
- (OCaml "Pervasives.exp")
+code_printing
+ constant real_exp \<rightharpoonup>
+ (SML) "Math.exp"
+ and (OCaml) "Pervasives.exp"
declare real_exp_def[code del]
declare exp_def[code del]
hide_const (open) real_exp
-code_const ln
- (SML "Math.ln")
- (OCaml "Pervasives.ln")
+code_printing
+ constant ln \<rightharpoonup>
+ (SML) "Math.ln"
+ and (OCaml) "Pervasives.ln"
declare ln_def[code del]
-code_const cos
- (SML "Math.cos")
- (OCaml "Pervasives.cos")
+code_printing
+ constant cos \<rightharpoonup>
+ (SML) "Math.cos"
+ and (OCaml) "Pervasives.cos"
declare cos_def[code del]
-code_const sin
- (SML "Math.sin")
- (OCaml "Pervasives.sin")
+code_printing
+ constant sin \<rightharpoonup>
+ (SML) "Math.sin"
+ and (OCaml) "Pervasives.sin"
declare sin_def[code del]
-code_const pi
- (SML "Math.pi")
- (OCaml "Pervasives.pi")
+code_printing
+ constant pi \<rightharpoonup>
+ (SML) "Math.pi"
+ and (OCaml) "Pervasives.pi"
declare pi_def[code del]
-code_const arctan
- (SML "Math.atan")
- (OCaml "Pervasives.atan")
+code_printing
+ constant arctan \<rightharpoonup>
+ (SML) "Math.atan"
+ and (OCaml) "Pervasives.atan"
declare arctan_def[code del]
-code_const arccos
- (SML "Math.scos")
- (OCaml "Pervasives.acos")
+code_printing
+ constant arccos \<rightharpoonup>
+ (SML) "Math.scos"
+ and (OCaml) "Pervasives.acos"
declare arccos_def[code del]
-code_const arcsin
- (SML "Math.asin")
- (OCaml "Pervasives.asin")
+code_printing
+ constant arcsin \<rightharpoonup>
+ (SML) "Math.asin"
+ and (OCaml) "Pervasives.asin"
declare arcsin_def[code del]
definition real_of_integer :: "integer \<Rightarrow> real" where
"real_of_integer = of_int \<circ> int_of_integer"
-code_const real_of_integer
- (SML "Real.fromInt")
- (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
+code_printing
+ constant real_of_integer \<rightharpoonup>
+ (SML) "Real.fromInt"
+ and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
definition real_of_int :: "int \<Rightarrow> real" where
[code_abbrev]: "real_of_int = of_int"
@@ -151,7 +174,8 @@
hide_const (open) real_of_int
-code_const Ratreal (SML)
+code_printing
+ constant Ratreal \<rightharpoonup> (SML)
definition Realfract :: "int => int => real"
where
@@ -159,8 +183,8 @@
code_datatype Realfract
-code_const Realfract
- (SML "Real.fromInt _/ '// Real.fromInt _")
+code_printing
+ constant Realfract \<rightharpoonup> (SML) "Real.fromInt _/ '// Real.fromInt _"
lemma [code]:
"Ratreal r = split Realfract (quotient_of r)"
--- a/src/HOL/Library/Code_Target_Int.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy Sun Jun 23 21:16:07 2013 +0200
@@ -109,14 +109,9 @@
"nat = nat_of_integer \<circ> of_int"
by transfer (simp add: fun_eq_iff)
-code_modulename SML
- Code_Target_Int Arith
-
-code_modulename OCaml
- Code_Target_Int Arith
-
-code_modulename Haskell
- Code_Target_Int Arith
+code_identifier
+ code_module Code_Target_Int \<rightharpoonup>
+ (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/Library/Code_Target_Nat.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy Sun Jun 23 21:16:07 2013 +0200
@@ -123,14 +123,9 @@
"integer_of_nat (nat k) = max 0 (integer_of_int k)"
by transfer auto
-code_modulename SML
- Code_Target_Nat Arith
-
-code_modulename OCaml
- Code_Target_Nat Arith
-
-code_modulename Haskell
- Code_Target_Nat Arith
+code_identifier
+ code_module Code_Target_Nat \<rightharpoonup>
+ (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/Library/Debug.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Debug.thy Sun Jun 23 21:16:07 2013 +0200
@@ -29,11 +29,12 @@
definition timing :: "String.literal \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where
[simp]: "timing s f x = f x"
-code_const trace and flush and timing
- (* FIXME proper @{make_string} instead of PolyML.makestring?!?! *)
- (Eval "Output.tracing" and "Output.tracing/ (PolyML.makestring _)" and "Timing.timeap'_msg")
+code_printing
+ constant trace \<rightharpoonup> (Eval) "Output.tracing"
+| constant flush \<rightharpoonup> (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *}
+| constant timing \<rightharpoonup> (Eval) "Timing.timeap'_msg"
-code_reserved Eval Output PolyML Timing
+code_reserved Eval Output Timing
hide_const (open) trace tracing flush flushing timing
--- a/src/HOL/Library/IArray.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/IArray.thy Sun Jun 23 21:16:07 2013 +0200
@@ -40,11 +40,9 @@
code_reserved SML Vector
-code_type iarray
- (SML "_ Vector.vector")
-
-code_const IArray
- (SML "Vector.fromList")
+code_printing
+ type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
+| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
lemma [code]:
"size (as :: 'a iarray) = 0"
@@ -74,8 +72,8 @@
"IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
by simp
-code_const IArray.tabulate
- (SML "Vector.tabulate")
+code_printing
+ constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
"sub' (as, n) = IArray.list_of as ! nat_of_integer n"
@@ -85,8 +83,8 @@
"as !! n = IArray.sub' (as, integer_of_nat n)"
by simp
-code_const IArray.sub'
- (SML "Vector.sub")
+code_printing
+ constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
definition length' :: "'a iarray \<Rightarrow> integer" where
[simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
@@ -96,8 +94,8 @@
"IArray.length as = nat_of_integer (IArray.length' as)"
by simp
-code_const IArray.length'
- (SML "Vector.length")
+code_printing
+ constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
end
--- a/src/HOL/Library/Parallel.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Library/Parallel.thy Sun Jun 23 21:16:07 2013 +0200
@@ -18,14 +18,10 @@
shows "f = g"
using assms by (cases f, cases g) (simp add: ext)
-code_type future
- (Eval "_ future")
-
-code_const fork
- (Eval "Future.fork")
-
-code_const join
- (Eval "Future.join")
+code_printing
+ type_constructor future \<rightharpoonup> (Eval) "_ future"
+| constant fork \<rightharpoonup> (Eval) "Future.fork"
+| constant join \<rightharpoonup> (Eval) "Future.join"
code_reserved Eval Future future
@@ -49,14 +45,10 @@
"exists P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
by (simp add: exists_def list_ex_iff)
-code_const map
- (Eval "Par'_List.map")
-
-code_const forall
- (Eval "Par'_List.forall")
-
-code_const exists
- (Eval "Par'_List.exists")
+code_printing
+ constant map \<rightharpoonup> (Eval) "Par'_List.map"
+| constant forall \<rightharpoonup> (Eval) "Par'_List.forall"
+| constant exists \<rightharpoonup> (Eval) "Par'_List.exists"
code_reserved Eval Par_List
--- a/src/HOL/List.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/List.thy Sun Jun 23 21:16:07 2013 +0200
@@ -6042,30 +6042,31 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_const_syntax target @{const_name Cons}
- (SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))
+ in
+ Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
+ [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
end
end;
*}
-code_type list
- (SML "_ list")
- (OCaml "_ list")
- (Haskell "![(_)]")
- (Scala "List[(_)]")
-
-code_const Nil
- (SML "[]")
- (OCaml "[]")
- (Haskell "[]")
- (Scala "!Nil")
-
-code_instance list :: equal
- (Haskell -)
-
-code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
- (Haskell infix 4 "==")
+code_printing
+ type_constructor list \<rightharpoonup>
+ (SML) "_ list"
+ and (OCaml) "_ list"
+ and (Haskell) "![(_)]"
+ and (Scala) "List[(_)]"
+| constant Nil \<rightharpoonup>
+ (SML) "[]"
+ and (OCaml) "[]"
+ and (Haskell) "[]"
+ and (Scala) "!Nil"
+| class_instance list :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool" \<rightharpoonup>
+ (Haskell) infix 4 "=="
+
+setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
code_reserved SML
list
@@ -6073,49 +6074,37 @@
code_reserved OCaml
list
-setup {* fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"] *}
-
subsubsection {* Use convenient predefined operations *}
-code_const "op @"
- (SML infixr 7 "@")
- (OCaml infixr 6 "@")
- (Haskell infixr 5 "++")
- (Scala infixl 7 "++")
-
-code_const map
- (Haskell "map")
-
-code_const filter
- (Haskell "filter")
-
-code_const concat
- (Haskell "concat")
-
-code_const List.maps
- (Haskell "concatMap")
-
-code_const rev
- (Haskell "reverse")
-
-code_const zip
- (Haskell "zip")
-
-code_const List.null
- (Haskell "null")
-
-code_const takeWhile
- (Haskell "takeWhile")
-
-code_const dropWhile
- (Haskell "dropWhile")
-
-code_const list_all
- (Haskell "all")
-
-code_const list_ex
- (Haskell "any")
+code_printing
+ constant "op @" \<rightharpoonup>
+ (SML) infixr 7 "@"
+ and (OCaml) infixr 6 "@"
+ and (Haskell) infixr 5 "++"
+ and (Scala) infixl 7 "++"
+| constant map \<rightharpoonup>
+ (Haskell) "map"
+| constant filter \<rightharpoonup>
+ (Haskell) "filter"
+| constant concat \<rightharpoonup>
+ (Haskell) "concat"
+| constant List.maps \<rightharpoonup>
+ (Haskell) "concatMap"
+| constant rev \<rightharpoonup>
+ (Haskell) "reverse"
+| constant zip \<rightharpoonup>
+ (Haskell) "zip"
+| constant List.null \<rightharpoonup>
+ (Haskell) "null"
+| constant takeWhile \<rightharpoonup>
+ (Haskell) "takeWhile"
+| constant dropWhile \<rightharpoonup>
+ (Haskell) "dropWhile"
+| constant list_all \<rightharpoonup>
+ (Haskell) "all"
+| constant list_ex \<rightharpoonup>
+ (Haskell) "any"
subsubsection {* Implementation of sets by lists *}
--- a/src/HOL/MicroJava/BV/BVExample.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy Sun Jun 23 21:16:07 2013 +0200
@@ -434,8 +434,8 @@
definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]:
"some_elem = (%S. SOME x. x : S)"
-code_const some_elem
- (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)")
+code_printing
+ constant some_elem \<rightharpoonup> (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)"
text {* This code setup is just a demonstration and \emph{not} sound! *}
--- a/src/HOL/Nat.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Nat.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1911,14 +1911,8 @@
subsection {* code module namespace *}
-code_modulename SML
- Nat Arith
-
-code_modulename OCaml
- Nat Arith
-
-code_modulename Haskell
- Nat Arith
+code_identifier
+ code_module Nat \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
hide_const (open) of_nat_aux
--- a/src/HOL/Num.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Num.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1114,14 +1114,8 @@
subsection {* code module namespace *}
-code_modulename SML
- Num Arith
-
-code_modulename OCaml
- Num Arith
-
-code_modulename Haskell
- Num Arith
+code_identifier
+ code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/Option.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Option.thy Sun Jun 23 21:16:07 2013 +0200
@@ -186,23 +186,26 @@
hide_const (open) is_none
-code_type option
- (SML "_ option")
- (OCaml "_ option")
- (Haskell "Maybe _")
- (Scala "!Option[(_)]")
-
-code_const None and Some
- (SML "NONE" and "SOME")
- (OCaml "None" and "Some _")
- (Haskell "Nothing" and "Just")
- (Scala "!None" and "Some")
-
-code_instance option :: equal
- (Haskell -)
-
-code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
- (Haskell infix 4 "==")
+code_printing
+ type_constructor option \<rightharpoonup>
+ (SML) "_ option"
+ and (OCaml) "_ option"
+ and (Haskell) "Maybe _"
+ and (Scala) "!Option[(_)]"
+| constant None \<rightharpoonup>
+ (SML) "NONE"
+ and (OCaml) "None"
+ and (Haskell) "Nothing"
+ and (Scala) "!None"
+| constant Some \<rightharpoonup>
+ (SML) "SOME"
+ and (OCaml) "Some _"
+ and (Haskell) "Just"
+ and (Scala) "Some"
+| class_instance option :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool" \<rightharpoonup>
+ (Haskell) infix 4 "=="
code_reserved SML
option NONE SOME
--- a/src/HOL/Power.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Power.thy Sun Jun 23 21:16:07 2013 +0200
@@ -742,14 +742,8 @@
declare power.power.simps [code]
-code_modulename SML
- Power Arith
-
-code_modulename OCaml
- Power Arith
-
-code_modulename Haskell
- Power Arith
+code_identifier
+ code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/Product_Type.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Product_Type.thy Sun Jun 23 21:16:07 2013 +0200
@@ -34,11 +34,9 @@
Code.add_case @{thm If_case_cert}
*}
-code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
- (Haskell infix 4 "==")
-
-code_instance bool :: equal
- (Haskell -)
+code_printing
+ constant "HOL.equal :: bool \<Rightarrow> bool \<Rightarrow> bool" \<rightharpoonup> (Haskell) infix 4 "=="
+| class_instance "bool" :: "equal" \<rightharpoonup> (Haskell) -
subsection {* The @{text unit} type *}
@@ -95,23 +93,21 @@
lemma [code]:
"HOL.equal (u\<Colon>unit) v \<longleftrightarrow> True" unfolding equal unit_eq [of u] unit_eq [of v] by rule+
-code_type unit
- (SML "unit")
- (OCaml "unit")
- (Haskell "()")
- (Scala "Unit")
-
-code_const Unity
- (SML "()")
- (OCaml "()")
- (Haskell "()")
- (Scala "()")
-
-code_instance unit :: equal
- (Haskell -)
-
-code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
- (Haskell infix 4 "==")
+code_printing
+ type_constructor unit \<rightharpoonup>
+ (SML) "unit"
+ and (OCaml) "unit"
+ and (Haskell) "()"
+ and (Scala) "Unit"
+| constant Unity \<rightharpoonup>
+ (SML) "()"
+ and (OCaml) "()"
+ and (Haskell) "()"
+ and (Scala) "()"
+| class_instance unit :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: unit \<Rightarrow> unit \<Rightarrow> bool" \<rightharpoonup>
+ (Haskell) infix 4 "=="
code_reserved SML
unit
@@ -288,23 +284,21 @@
subsubsection {* Code generator setup *}
-code_type prod
- (SML infix 2 "*")
- (OCaml infix 2 "*")
- (Haskell "!((_),/ (_))")
- (Scala "((_),/ (_))")
-
-code_const Pair
- (SML "!((_),/ (_))")
- (OCaml "!((_),/ (_))")
- (Haskell "!((_),/ (_))")
- (Scala "!((_),/ (_))")
-
-code_instance prod :: equal
- (Haskell -)
-
-code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- (Haskell infix 4 "==")
+code_printing
+ type_constructor prod \<rightharpoonup>
+ (SML) infix 2 "*"
+ and (OCaml) infix 2 "*"
+ and (Haskell) "!((_),/ (_))"
+ and (Scala) "((_),/ (_))"
+| constant Pair \<rightharpoonup>
+ (SML) "!((_),/ (_))"
+ and (OCaml) "!((_),/ (_))"
+ and (Haskell) "!((_),/ (_))"
+ and (Scala) "!((_),/ (_))"
+| class_instance prod :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool" \<rightharpoonup>
+ (Haskell) infix 4 "=="
subsubsection {* Fundamental operations and properties *}
@@ -330,8 +324,9 @@
lemma snd_conv [simp, code]: "snd (a, b) = b"
unfolding snd_def by simp
-code_const fst and snd
- (Haskell "fst" and "snd")
+code_printing
+ constant fst \<rightharpoonup> (Haskell) "fst"
+| constant snd \<rightharpoonup> (Haskell) "snd"
lemma prod_case_unfold [nitpick_unfold]: "prod_case = (%c p. c (fst p) (snd p))"
by (simp add: fun_eq_iff split: prod.split)
@@ -764,8 +759,8 @@
lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
by (simp add: fun_eq_iff scomp_unfold)
-code_const scomp
- (Eval infixl 3 "#->")
+code_printing
+ constant scomp \<rightharpoonup> (Eval) infixl 3 "#->"
no_notation fcomp (infixl "\<circ>>" 60)
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
--- a/src/HOL/Quickcheck_Exhaustive.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Sun Jun 23 21:16:07 2013 +0200
@@ -518,10 +518,11 @@
axiomatization throw_Counterexample :: "term list => unit"
axiomatization catch_Counterexample :: "unit => term list option"
-code_const throw_Counterexample
- (Quickcheck "raise (Exhaustive'_Generators.Counterexample _)")
-code_const catch_Counterexample
- (Quickcheck "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)")
+code_printing
+ constant throw_Counterexample \<rightharpoonup>
+ (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)"
+| constant catch_Counterexample \<rightharpoonup>
+ (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)"
subsection {* Continuation passing style functions as plus monad *}
--- a/src/HOL/Quickcheck_Narrowing.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Sun Jun 23 21:16:07 2013 +0200
@@ -13,14 +13,10 @@
setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
-code_type typerep
- (Haskell_Quickcheck "Typerep")
-
-code_const Typerep.Typerep
- (Haskell_Quickcheck "Typerep")
-
-code_type integer
- (Haskell_Quickcheck "Prelude.Int")
+code_printing
+ type_constructor typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
+| constant Typerep.Typerep \<rightharpoonup> (Haskell_Quickcheck) "Typerep"
+| type_constructor integer \<rightharpoonup> (Haskell_Quickcheck) "Prelude.Int"
code_reserved Haskell_Quickcheck Typerep
@@ -47,19 +43,19 @@
consts nth :: "'a list => integer => 'a"
-code_const nth (Haskell_Quickcheck infixl 9 "!!")
+code_printing constant nth \<rightharpoonup> (Haskell_Quickcheck) infixl 9 "!!"
consts error :: "char list => 'a"
-code_const error (Haskell_Quickcheck "error")
+code_printing constant error \<rightharpoonup> (Haskell_Quickcheck) "error"
consts toEnum :: "integer => char"
-code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
+code_printing constant toEnum \<rightharpoonup> (Haskell_Quickcheck) "Prelude.toEnum"
consts marker :: "char"
-code_const marker (Haskell_Quickcheck "''\\0'")
+code_printing constant marker \<rightharpoonup> (Haskell_Quickcheck) "''\\0'"
subsubsection {* Narrowing's basic operations *}
--- a/src/HOL/Quickcheck_Random.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Quickcheck_Random.thy Sun Jun 23 21:16:07 2013 +0200
@@ -15,8 +15,8 @@
axiomatization catch_match :: "'a => 'a => 'a"
-code_const catch_match
- (Quickcheck "((_) handle Match => _)")
+code_printing
+ constant catch_match \<rightharpoonup> (Quickcheck) "((_) handle Match => _)"
subsection {* The @{text random} class *}
@@ -212,7 +212,8 @@
subsection {* Code setup *}
-code_const random_fun_aux (Quickcheck "Random'_Generators.random'_fun")
+code_printing
+ constant random_fun_aux \<rightharpoonup> (Quickcheck) "Random'_Generators.random'_fun"
-- {* With enough criminal energy this can be abused to derive @{prop False};
for this reason we use a distinguished target @{text Quickcheck}
not spoiling the regular trusted code generation *}
--- a/src/HOL/Rings.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Rings.thy Sun Jun 23 21:16:07 2013 +0200
@@ -1149,13 +1149,8 @@
end
-code_modulename SML
- Rings Arith
-
-code_modulename OCaml
- Rings Arith
-
-code_modulename Haskell
- Rings Arith
+code_identifier
+ code_module Rings \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
+
--- a/src/HOL/Semiring_Normalization.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Semiring_Normalization.thy Sun Jun 23 21:16:07 2013 +0200
@@ -219,13 +219,7 @@
hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
-code_modulename SML
- Semiring_Normalization Arith
-
-code_modulename OCaml
- Semiring_Normalization Arith
-
-code_modulename Haskell
- Semiring_Normalization Arith
+code_identifier
+ code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
--- a/src/HOL/String.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/String.thy Sun Jun 23 21:16:07 2013 +0200
@@ -400,24 +400,25 @@
code_reserved OCaml string
code_reserved Scala string
-code_type literal
- (SML "string")
- (OCaml "string")
- (Haskell "String")
- (Scala "String")
+code_printing
+ type_constructor literal \<rightharpoonup>
+ (SML) "string"
+ and (OCaml) "string"
+ and (Haskell) "String"
+ and (Scala) "String"
setup {*
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
*}
-code_instance literal :: equal
- (Haskell -)
-
-code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
- (SML "!((_ : string) = _)")
- (OCaml "!((_ : string) = _)")
- (Haskell infix 4 "==")
- (Scala infixl 5 "==")
+code_printing
+ class_instance literal :: equal \<rightharpoonup>
+ (Haskell) -
+| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : string) = _)"
+ and (OCaml) "!((_ : string) = _)"
+ and (Haskell) infix 4 "=="
+ and (Scala) infixl 5 "=="
hide_type (open) literal
--- a/src/HOL/Tools/numeral.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Tools/numeral.ML Sun Jun 23 21:16:07 2013 +0200
@@ -81,9 +81,9 @@
fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
(Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
in
- thy |> Code_Target.add_const_syntax target number_of
- (SOME (Code_Printer.complex_const_syntax (1, ([@{const_name Num.One},
- @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))
+ thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
+ [(target, SOME (Code_Printer.complex_const_syntax
+ (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
end;
end; (*local*)
--- a/src/HOL/Tools/string_code.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Tools/string_code.ML Sun Jun 23 21:16:07 2013 +0200
@@ -58,8 +58,9 @@
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
| NONE =>
List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in Code_Target.add_const_syntax target
- @{const_name Cons} (SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))
+ in
+ Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
+ [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
end;
fun add_literal_char target =
@@ -68,8 +69,9 @@
case decode_char nibbles' (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
- in Code_Target.add_const_syntax target
- @{const_name Char} (SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))
+ in
+ Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
+ [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
end;
fun add_literal_string target =
@@ -80,8 +82,9 @@
of SOME p => p
| NONE => Code_Printer.eqn_error thm "Illegal message expression")
| NONE => Code_Printer.eqn_error thm "Illegal message expression";
- in Code_Target.add_const_syntax target
- @{const_name STR} (SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))
+ in
+ Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
+ [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
end;
end;
--- a/src/HOL/Typerep.thy Sun Jun 23 21:16:06 2013 +0200
+++ b/src/HOL/Typerep.thy Sun Jun 23 21:16:07 2013 +0200
@@ -87,11 +87,9 @@
"HOL.equal (x :: typerep) x \<longleftrightarrow> True"
by (fact equal_refl)
-code_type typerep
- (Eval "Term.typ")
-
-code_const Typerep
- (Eval "Term.Type/ (_, _)")
+code_printing
+ type_constructor typerep \<rightharpoonup> (Eval) "Term.typ"
+| constant Typerep \<rightharpoonup> (Eval) "Term.Type/ (_, _)"
code_reserved Eval Term
--- a/src/Tools/Code/code_haskell.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_haskell.ML Sun Jun 23 21:16:07 2013 +0200
@@ -465,8 +465,8 @@
val c_bind = Code.read_const thy raw_c_bind;
in if target = target' then
thy
- |> Code_Target.add_const_syntax target c_bind
- (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))
+ |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+ SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
else error "Only Haskell target allows for monad syntax" end;
@@ -484,12 +484,13 @@
make_command = fn module_name =>
"\"$ISABELLE_GHC\" " ^ language_params ^ " -odir build -hidir build -stubdir build -e \"\" " ^
module_name ^ ".hs" } })
- #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
str "->",
print_typ (INFX (1, R)) ty2
- )))
+ )))]))
#> fold (Code_Target.add_reserved target) [
"hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
"import", "default", "forall", "let", "in", "class", "qualified", "data",
--- a/src/Tools/Code/code_ml.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_ml.ML Sun Jun 23 21:16:07 2013 +0200
@@ -823,6 +823,13 @@
(** Isar setup **)
+fun fun_syntax print_typ fxy [ty1, ty2] =
+ brackify_infix (1, R) fxy (
+ print_typ (INFX (1, X)) ty1,
+ str "->",
+ print_typ (INFX (1, R)) ty2
+ );
+
val setup =
Code_Target.add_target
(target_SML, { serializer = serializer_sml, literals = literals_sml,
@@ -835,18 +842,8 @@
check = { env_var = "ISABELLE_OCAML",
make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
make_command = fn _ => "\"$ISABELLE_OCAML\" -w pu nums.cma ROOT.ocaml" } })
- #> Code_Target.add_tyco_syntax target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy (
- print_typ (INFX (1, X)) ty1,
- str "->",
- print_typ (INFX (1, R)) ty2
- )))
- #> Code_Target.add_tyco_syntax target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy (
- print_typ (INFX (1, X)) ty1,
- str "->",
- print_typ (INFX (1, R)) ty2
- )))
+ #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
--- a/src/Tools/Code/code_runtime.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_runtime.ML Sun Jun 23 21:16:07 2013 +0200
@@ -53,10 +53,10 @@
val _ = Context.>> (Context.map_theory
(Code_Target.extend_target (target, (Code_ML.target_SML, K I))
- #> Code_Target.add_tyco_syntax target @{type_name prop}
- (SOME (0, (K o K o K) (Code_Printer.str s_truth)))
- #> Code_Target.add_const_syntax target @{const_name Code_Generator.holds}
- (SOME (Code_Printer.plain_const_syntax s_Holds))
+ #> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop},
+ [(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))]))
+ #> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds},
+ [(target, SOME (Code_Printer.plain_const_syntax s_Holds))]))
#> Code_Target.add_reserved target this
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
(*avoid further pervasive infix names*)
@@ -287,7 +287,7 @@
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
- |> Code_Target.add_tyco_syntax target tyco (SOME (k, pr))
+ |> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))]))
end;
fun add_eval_constr (const, const') thy =
@@ -297,11 +297,12 @@
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
in
thy
- |> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr)))
+ |> Code_Target.set_printings (Code_Symbol.Constant (const,
+ [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
end;
-fun add_eval_const (const, const') = Code_Target.add_const_syntax target
- const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
+fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant
+ (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
thy
@@ -431,8 +432,8 @@
|> Code_Target.add_reserved target ml_name
|> Specification.axiomatization [(b, SOME T, NoSyn)] []
|-> (fn ([Const (const, _)], _) =>
- Code_Target.add_const_syntax target const
- (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
+ Code_Target.set_printings (Code_Symbol.Constant (const,
+ [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
fun process_file filepath (definienda, thy) =
--- a/src/Tools/Code/code_scala.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_scala.ML Sun Jun 23 21:16:07 2013 +0200
@@ -413,13 +413,13 @@
make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn _ =>
"env JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' \"$SCALA_HOME/bin/scalac\" ROOT.scala" } })
- #> Code_Target.add_tyco_syntax target "fun"
- (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy (
- print_typ BR ty1 (*product type vs. tupled arguments!*),
- str "=>",
- print_typ (INFX (1, R)) ty2
- )))
+ #> Code_Target.set_printings (Code_Symbol.Type_Constructor ("fun",
+ [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
+ brackify_infix (1, R) fxy (
+ print_typ BR ty1 (*product type vs. tupled arguments!*),
+ str "=>",
+ print_typ (INFX (1, R)) ty2
+ )))]))
#> fold (Code_Target.add_reserved target) [
"abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
"final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
--- a/src/Tools/Code/code_target.ML Sun Jun 23 21:16:06 2013 +0200
+++ b/src/Tools/Code/code_target.ML Sun Jun 23 21:16:07 2013 +0200
@@ -515,7 +515,7 @@
in union (op =) cs3 cs1 end;
fun prep_destination "" = NONE
- | prep_destination "-" = NONE
+ | prep_destination "-" = (legacy_feature "drop \"file\" argument entirely instead of \"-\""; NONE)
| prep_destination s = SOME (Path.explode s);
fun export_code thy cs seris =
@@ -638,8 +638,13 @@
val set_identifiers = gen_set_identifiers cert_name_decls;
val set_identifiers_cmd = gen_set_identifiers read_name_decls;
-fun add_module_alias_cmd target = fold (fn (sym, name) =>
- set_identifier (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))));
+fun add_module_alias_cmd target aliasses =
+ let
+ val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
+ in
+ fold (fn (sym, name) => set_identifier
+ (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses
+ end;
(* custom printings *)
@@ -670,6 +675,7 @@
fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
let
+ val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
val x = prep_x thy raw_x;
in set_printing (target, Symbol (x, Option.map (prep_syn thy x) some_raw_syn)) thy end;