# HG changeset patch # User haftmann # Date 1372014967 -7200 # Node ID 6646bb548c6b8dfc65730bc66154d8af343baaad # Parent cbb94074682b8bbce06a410eff341ea4e286c9c9 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier diff -r cbb94074682b -r 6646bb548c6b NEWS --- 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. diff -r cbb94074682b -r 6646bb548c6b src/Doc/IsarRef/HOL_Specific.thy --- 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} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Code_Evaluation.thy --- 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 \ integer \ term" - (Eval "HOLogic.mk'_number/ HOLogic.code'_integerT") - -code_const "term_of \ String.literal \ term" - (Eval "HOLogic.mk'_literal") +code_printing + type_constructor "term" \ (Eval) "Term.term" +| constant Const \ (Eval) "Term.Const/ ((_), (_))" +| constant App \ (Eval) "Term.$/ ((_), (_))" +| constant Abs \ (Eval) "Term.Abs/ ((_), (_), (_))" +| constant Free \ (Eval) "Term.Free/ ((_), (_))" +| constant "term_of \ integer \ term" \ (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT" +| constant "term_of \ String.literal \ term" \ (Eval) "HOLogic.mk'_literal" code_reserved Eval HOLogic @@ -161,8 +157,8 @@ definition tracing :: "String.literal \ 'a \ '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" \ (Eval) "Code'_Evaluation.tracing" subsection {* Generic reification *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Code_Numeral.thy --- 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 \ + (SML) "IntInf.int" + and (OCaml) "Big'_int.big'_int" + and (Haskell) "Integer" + and (Scala) "BigInt" + and (Eval) "int" +| class_instance integer :: equal \ + (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" \ + (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 \ _ \ _" - (SML "IntInf.+ ((_), (_))") - (OCaml "Big'_int.add'_big'_int") - (Haskell infixl 6 "+") - (Scala infixl 7 "+") - (Eval infixl 8 "+") - -code_const "uminus :: integer \ _" - (SML "IntInf.~") - (OCaml "Big'_int.minus'_big'_int") - (Haskell "negate") - (Scala "!(- _)") - (Eval "~/ _") - -code_const "minus :: integer \ _" - (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 \ _ \ _" \ + (SML) "IntInf.+ ((_), (_))" + and (OCaml) "Big'_int.add'_big'_int" + and (Haskell) infixl 6 "+" + and (Scala) infixl 7 "+" + and (Eval) infixl 8 "+" +| constant "uminus :: integer \ _" \ + (SML) "IntInf.~" + and (OCaml) "Big'_int.minus'_big'_int" + and (Haskell) "negate" + and (Scala) "!(- _)" + and (Eval) "~/ _" +| constant "minus :: integer \ _" \ + (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 \ + (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 \ + (SML) "!(raise/ Fail/ \"sub\")" + and (OCaml) "failwith/ \"sub\"" + and (Haskell) "error/ \"sub\"" + and (Scala) "!sys.error(\"sub\")" +| constant "times :: integer \ _ \ _" \ + (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 \ + (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 \ _ \ bool" \ + (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 \ _ \ bool" \ + (SML) "IntInf.<= ((_), (_))" + and (OCaml) "Big'_int.le'_big'_int" + and (Haskell) infix 4 "<=" + and (Scala) infixl 4 "<=" + and (Eval) infixl 6 "<=" +| constant "less :: integer \ _ \ bool" \ + (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 \ _ \ _" - (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 \ _ \ bool" - (SML "!((_ : IntInf.int) = _)") - (OCaml "Big'_int.eq'_big'_int") - (Haskell infix 4 "==") - (Scala infixl 5 "==") - (Eval infixl 6 "=") - -code_const "less_eq :: integer \ _ \ bool" - (SML "IntInf.<= ((_), (_))") - (OCaml "Big'_int.le'_big'_int") - (Haskell infix 4 "<=") - (Scala infixl 4 "<=") - (Eval infixl 6 "<=") - -code_const "less :: integer \ _ \ 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith subsection {* Type of target language naturals *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Divides.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end + diff -r cbb94074682b -r 6646bb548c6b src/HOL/Enum.thy --- 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 \ (Eval) "(fn '_ => raise Match)" subsubsection {* Equality and order on functions *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Fields.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Fun.thy --- 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 \ (Haskell) "id" + subsection {* The Composition Operator @{text "f \ g"} *} @@ -77,6 +80,9 @@ "SUPR A (g \ f) = SUPR (f ` A) g" by (simp add: SUP_def image_comp) +code_printing + constant comp \ (SML) infixl 5 "o" and (Haskell) infixr 9 "." + subsection {* The Forward Composition Operator @{text fcomp} *} @@ -95,8 +101,8 @@ lemma fcomp_id [simp]: "f \> id = f" by (simp add: fcomp_def) -code_const fcomp - (Eval infixl 1 "#>") +code_printing + constant fcomp \ (Eval) infixl 1 "#>" no_notation fcomp (infixl "\>" 60) @@ -814,16 +820,6 @@ *} -subsubsection {* Code generator *} - -code_const "op \" - (SML infixl 5 "o") - (Haskell infixr 9 ".") - -code_const "id" - (Haskell "id") - - subsubsection {* Functorial structure of types *} ML_file "Tools/enriched_type.ML" diff -r cbb94074682b -r 6646bb548c6b src/HOL/Groups.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith text {* Legacy *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/HOL.thy --- 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 \ + (SML) "bool" and (OCaml) "bool" and (Haskell) "Bool" and (Scala) "Boolean" +| constant True \ + (SML) "true" and (OCaml) "true" and (Haskell) "True" and (Scala) "true" +| constant False \ + (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 \ + (SML) "not" and (OCaml) "not" and (Haskell) "not" and (Scala) "'! _" +| constant HOL.conj \ + (SML) infixl 1 "andalso" and (OCaml) infixl 3 "&&" and (Haskell) infixr 3 "&&" and (Scala) infixl 3 "&&" +| constant HOL.disj \ + (SML) infixl 0 "orelse" and (OCaml) infixl 2 "||" and (Haskell) infixl 2 "||" and (Scala) infixl 1 "||" +| constant HOL.implies \ + (SML) "!(if (_)/ then (_)/ else true)" + and (OCaml) "!(if (_)/ then (_)/ else true)" + and (Haskell) "!(if (_)/ then (_)/ else True)" + and (Scala) "!(if ((_))/ (_)/ else true)" +| constant If \ + (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 \ + (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 \ (Haskell) "Eq" +| constant HOL.equal \ (Haskell) infix 4 "==" +| constant HOL.eq \ (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 \ + (SML) "!(raise/ Fail/ \"undefined\")" + and (OCaml) "failwith/ \"undefined\"" + and (Haskell) "error/ \"undefined\"" + and (Scala) "!sys.error(\"undefined\")" + subsubsection {* Evaluation and normalization by evaluation *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Imperative_HOL/Array.thy --- 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 \ 'a array \ bool" (SML infixl 6 "=") +code_printing type_constructor array \ (SML) "_/ array" +code_printing constant Array \ (SML) "raise/ (Fail/ \"bare Array\")" +code_printing constant Array.new' \ (SML) "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))" +code_printing constant Array.of_list \ (SML) "(fn/ ()/ =>/ Array.fromList/ _)" +code_printing constant Array.make' \ (SML) "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))" +code_printing constant Array.len' \ (SML) "(fn/ ()/ =>/ Array.length/ _)" +code_printing constant Array.nth' \ (SML) "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))" +code_printing constant Array.upd' \ (SML) "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))" +code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (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 \ 'a array \ bool" (OCaml infixl 4 "=") +code_printing type_constructor array \ (OCaml) "_/ array" +code_printing constant Array \ (OCaml) "failwith/ \"bare Array\"" +code_printing constant Array.new' \ (OCaml) "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)" +code_printing constant Array.of_list \ (OCaml) "(fun/ ()/ ->/ Array.of'_list/ _)" +code_printing constant Array.make' \ (OCaml) + "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/ (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))" +code_printing constant Array.len' \ (OCaml) "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))" +code_printing constant Array.nth' \ (OCaml) "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))" +code_printing constant Array.upd' \ (OCaml) "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)" +code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (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 \ 'a array \ bool" (Haskell infix 4 "==") -code_instance array :: HOL.equal (Haskell -) +code_printing type_constructor array \ (Haskell) "Heap.STArray/ Heap.RealWorld/ _" +code_printing constant Array \ (Haskell) "error/ \"bare Array\"" +code_printing constant Array.new' \ (Haskell) "Heap.newArray" +code_printing constant Array.of_list \ (Haskell) "Heap.newListArray" +code_printing constant Array.make' \ (Haskell) "Heap.newFunArray" +code_printing constant Array.len' \ (Haskell) "Heap.lengthArray" +code_printing constant Array.nth' \ (Haskell) "Heap.readArray" +code_printing constant Array.upd' \ (Haskell) "Heap.writeArray" +code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (Haskell) infix 4 "==" +code_printing class_instance array :: HOL.equal \ (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 \ 'a array \ bool" (Scala infixl 5 "==") +code_printing type_constructor array \ (Scala) "!collection.mutable.ArraySeq[_]" +code_printing constant Array \ (Scala) "!sys.error(\"bare Array\")" +code_printing constant Array.new' \ (Scala) "('_: Unit)/ => / Array.alloc((_))((_))" +code_printing constant Array.make' \ (Scala) "('_: Unit)/ =>/ Array.make((_))((_))" +code_printing constant Array.len' \ (Scala) "('_: Unit)/ =>/ Array.len((_))" +code_printing constant Array.nth' \ (Scala) "('_: Unit)/ =>/ Array.nth((_), (_))" +code_printing constant Array.upd' \ (Scala) "('_: Unit)/ =>/ Array.upd((_), (_), (_))" +code_printing constant Array.freeze \ (Scala) "('_: Unit)/ =>/ Array.freeze((_))" +code_printing constant "HOL.equal :: 'a array \ 'a array \ bool" \ (Scala) infixl 5 "==" end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Imperative_HOL/Heap_Monad.thy --- 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 \ (SML) "(unit/ ->/ _)" +code_printing constant bind \ (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())" +code_printing constant return \ (SML) "!(fn/ ()/ =>/ _)" +code_printing constant Heap_Monad.raise' \ (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 \ (OCaml) "(unit/ ->/ _)" +code_printing constant bind \ (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())" +code_printing constant return \ (OCaml) "!(fun/ ()/ ->/ _)" +code_printing constant Heap_Monad.raise' \ (OCaml) "failwith" subsubsection {* Haskell *} @@ -608,10 +608,10 @@ text {* Monad *} -code_type Heap (Haskell "Heap.ST/ Heap.RealWorld/ _") +code_printing type_constructor Heap \ (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 \ (Haskell) "return" +code_printing constant Heap_Monad.raise' \ (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 \ (Scala) "(Unit/ =>/ _)" +code_printing constant bind \ (Scala) "Heap.bind" +code_printing constant return \ (Scala) "('_: Unit)/ =>/ _" +code_printing constant Heap_Monad.raise' \ (Scala) "!sys.error((_))" subsubsection {* Target variants with less units *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Imperative_HOL/Ref.thy --- 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 \ 'a ref \ bool" (SML infixl 6 "=") +code_printing type_constructor ref \ (SML) "_/ ref" +code_printing type_constructor ref \ (Eval) "_/ Unsynchronized.ref" +code_printing constant Ref \ (SML) "raise/ (Fail/ \"bare Ref\")" +code_printing constant ref' \ (SML) "(fn/ ()/ =>/ ref/ _)" +code_printing constant ref' \ (Eval) "(fn/ ()/ =>/ Unsynchronized.ref/ _)" +code_printing constant Ref.lookup \ (SML) "(fn/ ()/ =>/ !/ _)" +code_printing constant Ref.update \ (SML) "(fn/ ()/ =>/ _/ :=/ _)" +code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (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 \ 'a ref \ bool" (OCaml infixl 4 "=") +code_printing type_constructor ref \ (OCaml) "_/ ref" +code_printing constant Ref \ (OCaml) "failwith/ \"bare Ref\"" +code_printing constant ref' \ (OCaml) "(fun/ ()/ ->/ ref/ _)" +code_printing constant Ref.lookup \ (OCaml) "(fun/ ()/ ->/ !/ _)" +code_printing constant Ref.update \ (OCaml) "(fun/ ()/ ->/ _/ :=/ _)" +code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (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 \ 'a ref \ bool" (Haskell infix 4 "==") -code_instance ref :: HOL.equal (Haskell -) +code_printing type_constructor ref \ (Haskell) "Heap.STRef/ Heap.RealWorld/ _" +code_printing constant Ref \ (Haskell) "error/ \"bare Ref\"" +code_printing constant ref' \ (Haskell) "Heap.newSTRef" +code_printing constant Ref.lookup \ (Haskell) "Heap.readSTRef" +code_printing constant Ref.update \ (Haskell) "Heap.writeSTRef" +code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (Haskell) infix 4 "==" +code_printing class_instance ref :: HOL.equal \ (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 \ 'a ref \ bool" (Scala infixl 5 "==") +code_printing type_constructor ref \ (Scala) "!Ref[_]" +code_printing constant Ref \ (Scala) "!sys.error(\"bare Ref\")" +code_printing constant ref' \ (Scala) "('_: Unit)/ =>/ Ref((_))" +code_printing constant Ref.lookup \ (Scala) "('_: Unit)/ =>/ Ref.lookup((_))" +code_printing constant Ref.update \ (Scala) "('_: Unit)/ =>/ Ref.update((_), (_))" +code_printing constant "HOL.equal :: 'a ref \ 'a ref \ bool" \ (Scala) infixl 5 "==" end + diff -r cbb94074682b -r 6646bb548c6b src/HOL/Int.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith quickcheck_params [default_type = int] diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Code_Binary_Nat.thy --- 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 \ + (SML) Arith and (OCaml) Arith and (Haskell) Arith hide_const (open) dup sub diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Code_Char.thy --- 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 \ + (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 \ + (Haskell) - +| constant "HOL.equal :: char \ char \ bool" \ + (SML) "!((_ : char) = _)" + and (OCaml) "!((_ : char) = _)" + and (Haskell) infix 4 "==" + and (Scala) infixl 5 "==" +| constant "Code_Evaluation.term_of \ char \ term" \ + (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))" code_reserved SML char @@ -31,32 +40,22 @@ code_reserved Scala char -code_const "HOL.equal \ char \ char \ bool" - (SML "!((_ : char) = _)") - (OCaml "!((_ : char) = _)") - (Haskell infix 4 "==") - (Scala infixl 5 "==") - -code_const "Code_Evaluation.term_of \ char \ term" - (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") - - definition implode :: "string \ 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 \ + (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 \ + (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 \ 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 \ char \ char \ bool" - (SML "!((_ : char) <= _)") - (OCaml "!((_ : char) <= _)") - (Haskell infix 4 "<=") - (Scala infixl 4 "<=") - (Eval infixl 6 "<=") - -code_const "Orderings.less \ char \ char \ bool" - (SML "!((_ : char) < _)") - (OCaml "!((_ : char) < _)") - (Haskell infix 4 "<") - (Scala infixl 4 "<") - (Eval infixl 6 "<") +code_printing + constant integer_of_char \ + (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 \ + (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 \ char \ bool" \ + (SML) "!((_ : char) <= _)" + and (OCaml) "!((_ : char) <= _)" + and (Haskell) infix 4 "<=" + and (Scala) infixl 4 "<=" + and (Eval) infixl 6 "<=" +| constant "Orderings.less :: char \ char \ bool" \ + (SML) "!((_ : char) < _)" + and (OCaml) "!((_ : char) < _)" + and (Haskell) infix 4 "<" + and (Scala) infixl 4 "<" + and (Eval) infixl 6 "<" end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Code_Real_Approx_By_Float.thy --- 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 \ + (SML) "real" + and (OCaml) "float" -code_const Ratreal - (SML "error/ \"Bad constant: Ratreal\"") +code_printing + constant Ratreal \ + (SML) "error/ \"Bad constant: Ratreal\"" -code_const "0 :: real" - (SML "0.0") - (OCaml "0.0") +code_printing + constant "0 :: real" \ + (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" \ + (SML) "1.0" + and (OCaml) "1.0" declare one_real_code[code_unfold del] -code_const "HOL.equal :: real \ real \ bool" - (SML "Real.== ((_), (_))") - (OCaml "Pervasives.(=)") +code_printing + constant "HOL.equal :: real \ real \ bool" \ + (SML) "Real.== ((_), (_))" + and (OCaml) "Pervasives.(=)" -code_const "Orderings.less_eq :: real \ real \ bool" - (SML "Real.<= ((_), (_))") - (OCaml "Pervasives.(<=)") +code_printing + constant "Orderings.less_eq :: real \ real \ bool" \ + (SML) "Real.<= ((_), (_))" + and (OCaml) "Pervasives.(<=)" -code_const "Orderings.less :: real \ real \ bool" - (SML "Real.< ((_), (_))") - (OCaml "Pervasives.(<)") +code_printing + constant "Orderings.less :: real \ real \ bool" \ + (SML) "Real.< ((_), (_))" + and (OCaml) "Pervasives.(<)" -code_const "op + :: real \ real \ real" - (SML "Real.+ ((_), (_))") - (OCaml "Pervasives.( +. )") +code_printing + constant "op + :: real \ real \ real" \ + (SML) "Real.+ ((_), (_))" + and (OCaml) "Pervasives.( +. )" -code_const "op * :: real \ real \ real" - (SML "Real.* ((_), (_))") - (OCaml "Pervasives.( *. )") +code_printing + constant "op * :: real \ real \ real" \ + (SML) "Real.* ((_), (_))" + and (OCaml) "Pervasives.( *. )" -code_const "op - :: real \ real \ real" - (SML "Real.- ((_), (_))") - (OCaml "Pervasives.( -. )") +code_printing + constant "op - :: real \ real \ real" \ + (SML) "Real.- ((_), (_))" + and (OCaml) "Pervasives.( -. )" -code_const "uminus :: real \ real" - (SML "Real.~") - (OCaml "Pervasives.( ~-. )") +code_printing + constant "uminus :: real \ real" \ + (SML) "Real.~" + and (OCaml) "Pervasives.( ~-. )" -code_const "op / :: real \ real \ real" - (SML "Real.'/ ((_), (_))") - (OCaml "Pervasives.( '/. )") +code_printing + constant "op / :: real \ real \ real" \ + (SML) "Real.'/ ((_), (_))" + and (OCaml) "Pervasives.( '/. )" -code_const "HOL.equal :: real \ real \ bool" - (SML "Real.== ((_:real), (_))") +code_printing + constant "HOL.equal :: real \ real \ bool" \ + (SML) "Real.== ((_:real), (_))" -code_const "sqrt :: real \ real" - (SML "Math.sqrt") - (OCaml "Pervasives.sqrt") +code_printing + constant "sqrt :: real \ real" \ + (SML) "Math.sqrt" + and (OCaml) "Pervasives.sqrt" declare sqrt_def[code del] definition real_exp :: "real \ 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 \ + (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 \ + (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 \ + (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 \ + (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 \ + (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 \ + (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 \ + (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 \ + (SML) "Math.asin" + and (OCaml) "Pervasives.asin" declare arcsin_def[code del] definition real_of_integer :: "integer \ real" where "real_of_integer = of_int \ 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 \ + (SML) "Real.fromInt" + and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))" definition real_of_int :: "int \ 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 \ (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 \ (SML) "Real.fromInt _/ '// Real.fromInt _" lemma [code]: "Ratreal r = split Realfract (quotient_of r)" diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Code_Target_Int.thy --- 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 \ 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 \ + (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Code_Target_Nat.thy --- 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 \ + (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Debug.thy --- 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 \ ('a \ 'b) \ 'a \ '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 \ (Eval) "Output.tracing" +| constant flush \ (Eval) "Output.tracing/ (@{make'_string} _)" -- {* note indirection via antiquotation *} +| constant timing \ (Eval) "Timing.timeap'_msg" -code_reserved Eval Output PolyML Timing +code_reserved Eval Output Timing hide_const (open) trace tracing flush flushing timing diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/IArray.thy --- 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 \ (SML) "_ Vector.vector" +| constant IArray \ (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 \ nat_of_integer)" by simp -code_const IArray.tabulate - (SML "Vector.tabulate") +code_printing + constant IArray.tabulate \ (SML) "Vector.tabulate" primrec sub' :: "'a iarray \ integer \ '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' \ (SML) "Vector.sub" definition length' :: "'a iarray \ 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' \ (SML) "Vector.length" end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Library/Parallel.thy --- 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 \ (Eval) "_ future" +| constant fork \ (Eval) "Future.fork" +| constant join \ (Eval) "Future.join" code_reserved Eval Future future @@ -49,14 +45,10 @@ "exists P xs \ (\x\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 \ (Eval) "Par'_List.map" +| constant forall \ (Eval) "Par'_List.forall" +| constant exists \ (Eval) "Par'_List.exists" code_reserved Eval Par_List diff -r cbb94074682b -r 6646bb548c6b src/HOL/List.thy --- 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 \ 'a list \ 'a list \ bool" - (Haskell infix 4 "==") +code_printing + type_constructor list \ + (SML) "_ list" + and (OCaml) "_ list" + and (Haskell) "![(_)]" + and (Scala) "List[(_)]" +| constant Nil \ + (SML) "[]" + and (OCaml) "[]" + and (Haskell) "[]" + and (Scala) "!Nil" +| class_instance list :: equal \ + (Haskell) - +| constant "HOL.equal :: 'a list \ 'a list \ bool" \ + (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 @" \ + (SML) infixr 7 "@" + and (OCaml) infixr 6 "@" + and (Haskell) infixr 5 "++" + and (Scala) infixl 7 "++" +| constant map \ + (Haskell) "map" +| constant filter \ + (Haskell) "filter" +| constant concat \ + (Haskell) "concat" +| constant List.maps \ + (Haskell) "concatMap" +| constant rev \ + (Haskell) "reverse" +| constant zip \ + (Haskell) "zip" +| constant List.null \ + (Haskell) "null" +| constant takeWhile \ + (Haskell) "takeWhile" +| constant dropWhile \ + (Haskell) "dropWhile" +| constant list_all \ + (Haskell) "all" +| constant list_ex \ + (Haskell) "any" subsubsection {* Implementation of sets by lists *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/MicroJava/BV/BVExample.thy --- 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 \ '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 \ (SML) "(case/ _ of/ Set/ xs/ =>/ hd/ xs)" text {* This code setup is just a demonstration and \emph{not} sound! *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Nat.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith hide_const (open) of_nat_aux diff -r cbb94074682b -r 6646bb548c6b src/HOL/Num.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Option.thy --- 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 \ 'a option \ 'a option \ bool" - (Haskell infix 4 "==") +code_printing + type_constructor option \ + (SML) "_ option" + and (OCaml) "_ option" + and (Haskell) "Maybe _" + and (Scala) "!Option[(_)]" +| constant None \ + (SML) "NONE" + and (OCaml) "None" + and (Haskell) "Nothing" + and (Scala) "!None" +| constant Some \ + (SML) "SOME" + and (OCaml) "Some _" + and (Haskell) "Just" + and (Scala) "Some" +| class_instance option :: equal \ + (Haskell) - +| constant "HOL.equal :: 'a option \ 'a option \ bool" \ + (Haskell) infix 4 "==" code_reserved SML option NONE SOME diff -r cbb94074682b -r 6646bb548c6b src/HOL/Power.thy --- 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 \ (SML) Arith and (OCaml) Arith and (Haskell) Arith end diff -r cbb94074682b -r 6646bb548c6b src/HOL/Product_Type.thy --- 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 \ bool \ bool \ bool" - (Haskell infix 4 "==") - -code_instance bool :: equal - (Haskell -) +code_printing + constant "HOL.equal :: bool \ bool \ bool" \ (Haskell) infix 4 "==" +| class_instance "bool" :: "equal" \ (Haskell) - subsection {* The @{text unit} type *} @@ -95,23 +93,21 @@ lemma [code]: "HOL.equal (u\unit) v \ 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 \ unit \ unit \ bool" - (Haskell infix 4 "==") +code_printing + type_constructor unit \ + (SML) "unit" + and (OCaml) "unit" + and (Haskell) "()" + and (Scala) "Unit" +| constant Unity \ + (SML) "()" + and (OCaml) "()" + and (Haskell) "()" + and (Scala) "()" +| class_instance unit :: equal \ + (Haskell) - +| constant "HOL.equal :: unit \ unit \ bool" \ + (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 \ 'a \ 'b \ 'a \ 'b \ bool" - (Haskell infix 4 "==") +code_printing + type_constructor prod \ + (SML) infix 2 "*" + and (OCaml) infix 2 "*" + and (Haskell) "!((_),/ (_))" + and (Scala) "((_),/ (_))" +| constant Pair \ + (SML) "!((_),/ (_))" + and (OCaml) "!((_),/ (_))" + and (Haskell) "!((_),/ (_))" + and (Scala) "!((_),/ (_))" +| class_instance prod :: equal \ + (Haskell) - +| constant "HOL.equal :: 'a \ 'b \ 'a \ 'b \ bool" \ + (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 \ (Haskell) "fst" +| constant snd \ (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 \> g) \\ h = f \> (g \\ h)" by (simp add: fun_eq_iff scomp_unfold) -code_const scomp - (Eval infixl 3 "#->") +code_printing + constant scomp \ (Eval) infixl 3 "#->" no_notation fcomp (infixl "\>" 60) no_notation scomp (infixl "\\" 60) diff -r cbb94074682b -r 6646bb548c6b src/HOL/Quickcheck_Exhaustive.thy --- 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 \ + (Quickcheck) "raise (Exhaustive'_Generators.Counterexample _)" +| constant catch_Counterexample \ + (Quickcheck) "(((_); NONE) handle Exhaustive'_Generators.Counterexample ts => SOME ts)" subsection {* Continuation passing style functions as plus monad *} diff -r cbb94074682b -r 6646bb548c6b src/HOL/Quickcheck_Narrowing.thy --- 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 \ (Haskell_Quickcheck) "Typerep" +| constant Typerep.Typerep \