1 (* Title: HOL/Library/Code_Char_chr.thy
3 Author: Florian Haftmann
6 header {* Code generation of pretty characters with character codes *}
9 imports Char_nat Code_Char Code_Integer
13 "int_of_char = int o nat_of_char"
16 "nat_of_char = nat o int_of_char"
17 unfolding int_of_char_def by (simp add: expand_fun_eq)
20 "char_of_int = char_of_nat o nat"
23 "char_of_nat = char_of_int o int"
24 unfolding char_of_int_def by (simp add: expand_fun_eq)
26 lemmas [code func del] = char.recs char.cases char.size
28 lemma [code func, code inline]:
29 "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
30 by (cases c) (auto simp add: nibble_pair_of_nat_char)
32 lemma [code func, code inline]:
33 "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
34 by (cases c) (auto simp add: nibble_pair_of_nat_char)
37 "size (c\<Colon>char) = 0"
40 code_const int_of_char and char_of_int
41 (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
42 (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
43 (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")