author | haftmann |
Fri, 20 Aug 2010 17:48:30 +0200 | |
changeset 38622 | 86fc906dcd86 |
parent 37222 | 4d984bc33c66 |
child 39198 | f967a16dfcdd |
permissions | -rw-r--r-- |
24999 | 1 |
(* Title: HOL/Library/Code_Char_chr.thy |
2 |
Author: Florian Haftmann |
|
3 |
*) |
|
4 |
||
5 |
header {* Code generation of pretty characters with character codes *} |
|
6 |
||
7 |
theory Code_Char_chr |
|
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
28562
diff
changeset
|
8 |
imports Char_nat Code_Char Code_Integer Main |
24999 | 9 |
begin |
10 |
||
11 |
definition |
|
12 |
"int_of_char = int o nat_of_char" |
|
13 |
||
28562 | 14 |
lemma [code]: |
24999 | 15 |
"nat_of_char = nat o int_of_char" |
16 |
unfolding int_of_char_def by (simp add: expand_fun_eq) |
|
17 |
||
18 |
definition |
|
19 |
"char_of_int = char_of_nat o nat" |
|
20 |
||
28562 | 21 |
lemma [code]: |
24999 | 22 |
"char_of_nat = char_of_int o int" |
23 |
unfolding char_of_int_def by (simp add: expand_fun_eq) |
|
24 |
||
25 |
code_const int_of_char and char_of_int |
|
26 |
(SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)") |
|
27 |
(OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)") |
|
37222 | 28 |
(Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | (0 <= k && k < 256) = toEnum k :: Char in chr . fromInteger)") |
29 |
(Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))") |
|
24999 | 30 |
|
37222 | 31 |
end |