added Scala code setup
authorhaftmann
Tue Jun 01 10:30:53 2010 +0200 (2010-06-01)
changeset 372224d984bc33c66
parent 37221 9d9205e31767
child 37223 5226259b6fa2
added Scala code setup
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Char_chr.thy
     1.1 --- a/src/HOL/Library/Code_Char.thy	Tue Jun 01 10:30:53 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Tue Jun 01 10:30:53 2010 +0200
     1.3 @@ -12,9 +12,10 @@
     1.4    (SML "char")
     1.5    (OCaml "char")
     1.6    (Haskell "Char")
     1.7 +  (Scala "Char")
     1.8  
     1.9  setup {*
    1.10 -  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
    1.11 +  fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    1.12    #> String_Code.add_literal_list_string "Haskell"
    1.13  *}
    1.14  
    1.15 @@ -27,10 +28,14 @@
    1.16  code_reserved OCaml
    1.17    char
    1.18  
    1.19 +code_reserved Scala
    1.20 +  char
    1.21 +
    1.22  code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.23    (SML "!((_ : char) = _)")
    1.24    (OCaml "!((_ : char) = _)")
    1.25    (Haskell infixl 4 "==")
    1.26 +  (Scala infixl 5 "==")
    1.27  
    1.28  code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    1.29    (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    1.30 @@ -53,10 +58,12 @@
    1.31    (SML "String.implode")
    1.32    (OCaml "failwith/ \"implode\"")
    1.33    (Haskell "_")
    1.34 +  (Scala "List.toString((_))")
    1.35  
    1.36  code_const explode
    1.37    (SML "String.explode")
    1.38    (OCaml "failwith/ \"explode\"")
    1.39    (Haskell "_")
    1.40 +  (Scala "List.fromString((_))")
    1.41  
    1.42  end
     2.1 --- a/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 10:30:53 2010 +0200
     2.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jun 01 10:30:53 2010 +0200
     2.3 @@ -22,23 +22,10 @@
     2.4    "char_of_nat = char_of_int o int"
     2.5    unfolding char_of_int_def by (simp add: expand_fun_eq)
     2.6  
     2.7 -lemmas [code del] = char.recs char.cases char.size
     2.8 -
     2.9 -lemma [code, code_unfold]:
    2.10 -  "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
    2.11 -  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    2.12 -
    2.13 -lemma [code, code_unfold]:
    2.14 -  "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
    2.15 -  by (cases c) (auto simp add: nibble_pair_of_nat_char)
    2.16 -
    2.17 -lemma [code]:
    2.18 -  "size (c\<Colon>char) = 0"
    2.19 -  by (cases c) auto
    2.20 -
    2.21  code_const int_of_char and char_of_int
    2.22    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
    2.23    (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
    2.24 -  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
    2.25 +  (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)")
    2.26 +  (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    2.27  
    2.28 -end
    2.29 \ No newline at end of file
    2.30 +end