| author | haftmann |
| Tue, 01 Jun 2010 10:30:53 +0200 | |
| changeset 37221 | 4d984bc33c66 |
| parent 32061 | 6d28bbd33e2c |
| child 39428 | f967a16dfcdd |
| 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" |
| haftmann@24999 | 16 |
unfolding int_of_char_def by (simp add: expand_fun_eq) |
| 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" |
| haftmann@24999 | 23 |
unfolding char_of_int_def by (simp add: expand_fun_eq) |
| 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@37221 | 28 |
(Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . 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 |