--- a/src/HOL/Code_Numeral.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Jan 13 08:56:25 2010 +0100
@@ -289,33 +289,38 @@
(SML "int")
(OCaml "Big'_int.big'_int")
(Haskell "Int")
+ (Scala "Int")
code_instance code_numeral :: eq
(Haskell -)
setup {*
fold (Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral}
- false false) ["SML", "Haskell"]
+ false false) ["SML", "Haskell", "Scala"]
#> Numeral.add_code @{const_name number_code_numeral_inst.number_of_code_numeral} false true "OCaml"
*}
code_reserved SML Int int
code_reserved OCaml Big_int
+code_reserved Scala Int
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.+/ ((_),/ (_))")
(OCaml "Big'_int.add'_big'_int")
(Haskell infixl 6 "+")
+ (Scala infixl 7 "+")
code_const "subtract_code_numeral \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.max/ (_/ -/ _,/ 0 : int)")
(OCaml "Big'_int.max'_big'_int/ (Big'_int.sub'_big'_int/ _/ _)/ Big'_int.zero'_big'_int")
(Haskell "max/ (_/ -/ _)/ (0 :: Int)")
+ (Scala "!(_/ -/ _).max(0)")
code_const "op * \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
(SML "Int.*/ ((_),/ (_))")
(OCaml "Big'_int.mult'_big'_int")
(Haskell infixl 7 "*")
+ (Scala infixl 8 "*")
code_const div_mod_code_numeral
(SML "(fn n => fn m =>/ if m = 0/ then (0, n) else/ (n div m, n mod m))")
@@ -326,15 +331,18 @@
(SML "!((_ : Int.int) = _)")
(OCaml "Big'_int.eq'_big'_int")
(Haskell infixl 4 "==")
+ (Scala infixl 5 "==")
code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "Int.<=/ ((_),/ (_))")
(OCaml "Big'_int.le'_big'_int")
(Haskell infix 4 "<=")
+ (Scala infix 4 "<=")
code_const "op < \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(SML "Int.</ ((_),/ (_))")
(OCaml "Big'_int.lt'_big'_int")
(Haskell infix 4 "<")
+ (Scala infix 4 "<")
end
--- a/src/HOL/HOL.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/HOL.thy Wed Jan 13 08:56:25 2010 +0100
@@ -1954,6 +1954,7 @@
(SML "!(raise/ Fail/ \"undefined\")")
(OCaml "failwith/ \"undefined\"")
(Haskell "error/ \"undefined\"")
+ (Scala "!error(\"undefined\")")
subsubsection {* Evaluation and normalization by evaluation *}
--- a/src/HOL/List.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/List.thy Wed Jan 13 08:56:25 2010 +0100
@@ -3890,12 +3890,14 @@
code_type list
(SML "_ list")
(OCaml "_ list")
- (Haskell "![_]")
+ (Haskell "![(_)]")
+ (Scala "List[(_)]")
code_const Nil
(SML "[]")
(OCaml "[]")
(Haskell "[]")
+ (Scala "Nil")
code_instance list :: eq
(Haskell -)
@@ -3938,7 +3940,7 @@
(Codegen.invoke_codegen thy defs dep thyname false) ts gr'
in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
in
- fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
+ fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
#> Codegen.add_codegen "list_codegen" list_codegen
end
*}
--- a/src/HOL/Option.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/Option.thy Wed Jan 13 08:56:25 2010 +0100
@@ -115,11 +115,13 @@
(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 :: eq
(Haskell -)
@@ -133,4 +135,7 @@
code_reserved OCaml
option None Some
+code_reserved Scala
+ Option None Some
+
end
--- a/src/HOL/Product_Type.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/Product_Type.thy Wed Jan 13 08:56:25 2010 +0100
@@ -99,6 +99,7 @@
(SML "unit")
(OCaml "unit")
(Haskell "()")
+ (Scala "Unit")
code_instance unit :: eq
(Haskell -)
@@ -110,6 +111,7 @@
(SML "()")
(OCaml "()")
(Haskell "()")
+ (Scala "()")
code_reserved SML
unit
@@ -117,6 +119,9 @@
code_reserved OCaml
unit
+code_reserved Scala
+ Unit
+
subsection {* Pairs *}
@@ -995,6 +1000,7 @@
(SML infix 2 "*")
(OCaml infix 2 "*")
(Haskell "!((_),/ (_))")
+ (Scala "!((_),/ (_))")
code_instance * :: eq
(Haskell -)
@@ -1006,6 +1012,7 @@
(SML "!((_),/ (_))")
(OCaml "!((_),/ (_))")
(Haskell "!((_),/ (_))")
+ (Scala "!((_),/ (_))")
code_const fst and snd
(Haskell "fst" and "snd")
--- a/src/HOL/String.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/String.thy Wed Jan 13 08:56:25 2010 +0100
@@ -170,14 +170,16 @@
code_reserved SML string
code_reserved OCaml string
+code_reserved Scala string
code_type literal
(SML "string")
(OCaml "string")
(Haskell "String")
+ (Scala "String")
setup {*
- fold String_Code.add_literal_string ["SML", "OCaml", "Haskell"]
+ fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
*}
code_instance literal :: eq
@@ -187,7 +189,7 @@
(SML "!((_ : string) = _)")
(OCaml "!((_ : string) = _)")
(Haskell infixl 4 "==")
-
+ (Scala infixl 5 "==")
types_code
"char" ("string")
--- a/src/HOL/ex/Codegenerator_Pretty_Test.thy Wed Jan 13 00:08:56 2010 +0100
+++ b/src/HOL/ex/Codegenerator_Pretty_Test.thy Wed Jan 13 08:56:25 2010 +0100
@@ -10,6 +10,6 @@
export_code * in SML module_name CodegenTest
in OCaml module_name CodegenTest file -
in Haskell file -
- in Scala file -
+(*in Scala file -*)
end
--- a/src/Tools/Code/code_scala.ML Wed Jan 13 00:08:56 2010 +0100
+++ b/src/Tools/Code/code_scala.ML Wed Jan 13 08:56:25 2010 +0100
@@ -409,7 +409,7 @@
literal_string = quote o translate_string char_scala,
literal_numeral = fn unbounded => fn k => if k >= 0 then string_of_int k
else Library.enclose "(" ")" (signed_string_of_int k),
- literal_list = fn ps => Pretty.block [str "List", enum "," "(" ")" ps],
+ literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
infix_cons = (6, "::")
} end;
@@ -436,7 +436,7 @@
"true", "type", "val", "var", "while", "with"
]
#> fold (Code_Target.add_reserved target) [
- "error", "apply", "List"
+ "error", "apply", "List", "Nil"
];
end; (*struct*)