# HG changeset patch
# User haftmann
# Date 1263369385 -3600
# Node ID dcaf6ec84e2886ef9e720f1b97623641e65221e5
# Parent  6587c24ef6d889d0935775a2861ad2225b22bf03# Parent  460ec1a99aa218e491f7a49a02fd5e8eec37680a
merged

diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/Code_Numeral.thy
--- 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
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/HOL.thy
--- 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 *}
 
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/List.thy
--- 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
 *}
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/Option.thy
--- 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
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/Product_Type.thy
--- 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")
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/String.thy
--- 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")
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/HOL/ex/Codegenerator_Pretty_Test.thy
--- 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
diff -r 6587c24ef6d8 -r dcaf6ec84e28 src/Tools/Code/code_scala.ML
--- 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*)