src/HOL/Library/Code_Char.thy
changeset 51160 599ff65b85e2
parent 48431 6efff142bb54
child 51542 738598beeb26
     1.1 --- a/src/HOL/Library/Code_Char.thy	Fri Feb 15 15:22:16 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Feb 15 11:47:33 2013 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Code generation of pretty characters (and strings) *}
     1.5  
     1.6  theory Code_Char
     1.7 -imports List Code_Evaluation Main
     1.8 +imports Main "~~/src/HOL/Library/Char_ord"
     1.9  begin
    1.10  
    1.11  code_type char
    1.12 @@ -58,4 +58,47 @@
    1.13    (Haskell "_")
    1.14    (Scala "!(_.toList)")
    1.15  
    1.16 +
    1.17 +definition integer_of_char :: "char \<Rightarrow> integer"
    1.18 +where
    1.19 +  "integer_of_char = integer_of_nat o nat_of_char"
    1.20 +
    1.21 +definition char_of_integer :: "integer \<Rightarrow> char"
    1.22 +where
    1.23 +  "char_of_integer = char_of_nat \<circ> nat_of_integer"
    1.24 +
    1.25 +lemma [code]:
    1.26 +  "nat_of_char = nat_of_integer o integer_of_char"
    1.27 +  by (simp add: integer_of_char_def fun_eq_iff)
    1.28 +
    1.29 +lemma [code]:
    1.30 +  "char_of_nat = char_of_integer o integer_of_nat"
    1.31 +  by (simp add: char_of_integer_def fun_eq_iff)
    1.32 +
    1.33 +code_const integer_of_char and char_of_integer
    1.34 +  (SML "!(IntInf.fromInt o Char.ord)"
    1.35 +    and "!(Char.chr o IntInf.toInt)")
    1.36 +  (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
    1.37 +    and "Char.chr (Big'_int.int'_of'_big'_int _)")
    1.38 +  (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    1.39 +    and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
    1.40 +  (Scala "BigInt(_.toInt)"
    1.41 +    and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    1.42 +
    1.43 +
    1.44 +code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.45 +  (SML "!((_ : char) <= _)")
    1.46 +  (OCaml "!((_ : char) <= _)")
    1.47 +  (Haskell infix 4 "<=")
    1.48 +  (Scala infixl 4 "<=")
    1.49 +  (Eval infixl 6 "<=")
    1.50 +
    1.51 +code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.52 +  (SML "!((_ : char) < _)")
    1.53 +  (OCaml "!((_ : char) < _)")
    1.54 +  (Haskell infix 4 "<")
    1.55 +  (Scala infixl 4 "<")
    1.56 +  (Eval infixl 6 "<")
    1.57 +
    1.58  end
    1.59 +