# HG changeset patch
# User wenzelm
# Date 1275385061 -7200
# Node ID 7c59ab0a419b20c5597e1daf930a3a1c94c91d24
# Parent  32c5251f78cdd5a2c42ae9dac9309d2032f5cdcb# Parent  d416e49b3926a13c5a4b09e5802a74e605bbdf7a
merged

diff -r d416e49b3926 -r 7c59ab0a419b src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Tue Jun 01 11:37:24 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy	Tue Jun 01 11:37:41 2010 +0200
@@ -75,7 +75,7 @@
   unfolding nibble_of_nat_def by auto
 
 lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
-  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
+  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
 
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
   by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
@@ -193,12 +193,12 @@
 text {* Code generator setup *}
 
 code_modulename SML
-  Char_nat List
+  Char_nat String
 
 code_modulename OCaml
-  Char_nat List
+  Char_nat String
 
 code_modulename Haskell
-  Char_nat List
+  Char_nat String
 
 end
\ No newline at end of file
diff -r d416e49b3926 -r 7c59ab0a419b src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Tue Jun 01 11:37:24 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Tue Jun 01 11:37:41 2010 +0200
@@ -12,9 +12,10 @@
   (SML "char")
   (OCaml "char")
   (Haskell "Char")
+  (Scala "Char")
 
 setup {*
-  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
+  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
   #> String_Code.add_literal_list_string "Haskell"
 *}
 
@@ -27,10 +28,14 @@
 code_reserved OCaml
   char
 
+code_reserved Scala
+  char
+
 code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")
+  (Scala infixl 5 "==")
 
 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
@@ -53,10 +58,12 @@
   (SML "String.implode")
   (OCaml "failwith/ \"implode\"")
   (Haskell "_")
+  (Scala "List.toString((_))")
 
 code_const explode
   (SML "String.explode")
   (OCaml "failwith/ \"explode\"")
   (Haskell "_")
+  (Scala "List.fromString((_))")
 
 end
diff -r d416e49b3926 -r 7c59ab0a419b src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 11:37:24 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 11:37:41 2010 +0200
@@ -22,23 +22,10 @@
   "char_of_nat = char_of_int o int"
   unfolding char_of_int_def by (simp add: expand_fun_eq)
 
-lemmas [code del] = char.recs char.cases char.size
-
-lemma [code, code_unfold]:
-  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code, code_unfold]:
-  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
-  by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code]:
-  "size (c\<Colon>char) = 0"
-  by (cases c) auto
-
 code_const int_of_char and char_of_int
   (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 "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
+  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
+  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
 
-end
\ No newline at end of file
+end
diff -r d416e49b3926 -r 7c59ab0a419b src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 11:37:24 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jun 01 11:37:41 2010 +0200
@@ -317,7 +317,7 @@
     else error("Int value too big:" + this.value.toString)
 
   def +(that: Nat): Nat = new Nat(this.value + that.value)
-  def -(that: Nat): Nat = Nat(this.value + that.value)
+  def -(that: Nat): Nat = Nat(this.value - that.value)
   def *(that: Nat): Nat = new Nat(this.value * that.value)
 
   def /%(that: Nat): (Nat, Nat) = if (that.value == 0) (new Nat(0), this)
diff -r d416e49b3926 -r 7c59ab0a419b src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Jun 01 11:37:24 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Tue Jun 01 11:37:41 2010 +0200
@@ -400,10 +400,11 @@
   end;
 
 val literals = let
-  fun char_scala c =
-    let
-      val s = ML_Syntax.print_char c;
-    in if s = "'" then "\\'" else s end;
+  fun char_scala c = if c = "'" then "\\'"
+    else if c = "\"" then "\\\""
+    else if c = "\\" then "\\\\"
+    else let val k = ord c
+    in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   fun numeral_scala k = if k < 0
     then if k <= 2147483647 then "- " ^ string_of_int (~ k)
       else quote ("- " ^ string_of_int (~ k))