| author | haftmann |
| Mon, 23 Jul 2012 09:28:03 +0200 | |
| changeset 49446 | 6efff142bb54 |
| parent 39535 | d7728f65b353 |
| child 52280 | 0a2371e7ced3 |
| permissions | -rw-r--r-- |
| haftmann@24999 | 1 |
(* Title: HOL/Library/Code_Char_chr.thy |
| haftmann@24999 | 2 |
Author: Florian Haftmann |
| haftmann@24999 | 3 |
*) |
| haftmann@24999 | 4 |
|
| haftmann@24999 | 5 |
header {* Code generation of pretty characters with character codes *}
|
| haftmann@24999 | 6 |
|
| haftmann@24999 | 7 |
theory Code_Char_chr |
| haftmann@30663 | 8 |
imports Char_nat Code_Char Code_Integer Main |
| haftmann@24999 | 9 |
begin |
| haftmann@24999 | 10 |
|
| haftmann@24999 | 11 |
definition |
| haftmann@24999 | 12 |
"int_of_char = int o nat_of_char" |
| haftmann@24999 | 13 |
|
| haftmann@28562 | 14 |
lemma [code]: |
| haftmann@24999 | 15 |
"nat_of_char = nat o int_of_char" |
| nipkow@39535 | 16 |
unfolding int_of_char_def by (simp add: fun_eq_iff) |
| haftmann@24999 | 17 |
|
| haftmann@24999 | 18 |
definition |
| haftmann@24999 | 19 |
"char_of_int = char_of_nat o nat" |
| haftmann@24999 | 20 |
|
| haftmann@28562 | 21 |
lemma [code]: |
| haftmann@24999 | 22 |
"char_of_nat = char_of_int o int" |
| nipkow@39535 | 23 |
unfolding char_of_int_def by (simp add: fun_eq_iff) |
| haftmann@24999 | 24 |
|
| haftmann@24999 | 25 |
code_const int_of_char and char_of_int |
| haftmann@24999 | 26 |
(SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
| haftmann@24999 | 27 |
(OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
| haftmann@49446 | 28 |
(Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))" and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)") |
| haftmann@37221 | 29 |
(Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
| haftmann@24999 | 30 |
|
| haftmann@37221 | 31 |
end |