--- a/src/HOL/Library/Code_Char.thy Tue Jun 01 10:30:53 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy Tue Jun 01 10:30:53 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
--- a/src/HOL/Library/Code_Char_chr.thy Tue Jun 01 10:30:53 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Tue Jun 01 10:30:53 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