wneuper/isa: src/HOL/Library/Code_Char

     1 (*  Title:      HOL/Library/Code_Char_chr.thy

     2     Author:     Florian Haftmann

     3 *)

     5 header {* Code generation of pretty characters with character codes *}

     7 theory Code_Char_chr

     8 imports Char_nat Code_Char Code_Integer Main

     9 begin

    11 definition

    12   "int_of_char = int o nat_of_char"

    14 lemma [code]:

    15   "nat_of_char = nat o int_of_char"

    16   unfolding int_of_char_def by (simp add: fun_eq_iff)

    18 definition

    19   "char_of_int = char_of_nat o nat"

    21 lemma [code]:

    22   "char_of_nat = char_of_int o int"

    23   unfolding char_of_int_def by (simp add: fun_eq_iff)

    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 _)")

    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)")

    29   (Scala "BigInt(_.toInt)" and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")

    31 end

author	haftmann
	Mon, 23 Jul 2012 09:28:03 +0200
changeset 49446	6efff142bb54
parent 39535	d7728f65b353
child 52280	0a2371e7ced3
permissions	-rw-r--r--