src/HOL/Library/Code_Char.thy
author haftmann
Tue Feb 19 19:44:10 2013 +0100 (2013-02-19)
changeset 51188 9b5bf1a9a710
parent 51160 599ff65b85e2
child 51542 738598beeb26
permissions -rw-r--r--
dropped spurious left-over from 0a2371e7ced3
     1 (*  Title:      HOL/Library/Code_Char.thy
     2     Author:     Florian Haftmann
     3 *)
     4 
     5 header {* Code generation of pretty characters (and strings) *}
     6 
     7 theory Code_Char
     8 imports Main "~~/src/HOL/Library/Char_ord"
     9 begin
    10 
    11 code_type char
    12   (SML "char")
    13   (OCaml "char")
    14   (Haskell "Prelude.Char")
    15   (Scala "Char")
    16 
    17 setup {*
    18   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    19   #> String_Code.add_literal_list_string "Haskell"
    20 *}
    21 
    22 code_instance char :: equal
    23   (Haskell -)
    24 
    25 code_reserved SML
    26   char
    27 
    28 code_reserved OCaml
    29   char
    30 
    31 code_reserved Scala
    32   char
    33 
    34 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    35   (SML "!((_ : char) = _)")
    36   (OCaml "!((_ : char) = _)")
    37   (Haskell infix 4 "==")
    38   (Scala infixl 5 "==")
    39 
    40 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    41   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    42 
    43 
    44 definition implode :: "string \<Rightarrow> String.literal" where
    45   "implode = STR"
    46 
    47 code_reserved SML String
    48 
    49 code_const implode
    50   (SML "String.implode")
    51   (OCaml "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)")
    52   (Haskell "_")
    53   (Scala "!(\"\" ++/ _)")
    54 
    55 code_const explode
    56   (SML "String.explode")
    57   (OCaml "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])")
    58   (Haskell "_")
    59   (Scala "!(_.toList)")
    60 
    61 
    62 definition integer_of_char :: "char \<Rightarrow> integer"
    63 where
    64   "integer_of_char = integer_of_nat o nat_of_char"
    65 
    66 definition char_of_integer :: "integer \<Rightarrow> char"
    67 where
    68   "char_of_integer = char_of_nat \<circ> nat_of_integer"
    69 
    70 lemma [code]:
    71   "nat_of_char = nat_of_integer o integer_of_char"
    72   by (simp add: integer_of_char_def fun_eq_iff)
    73 
    74 lemma [code]:
    75   "char_of_nat = char_of_integer o integer_of_nat"
    76   by (simp add: char_of_integer_def fun_eq_iff)
    77 
    78 code_const integer_of_char and char_of_integer
    79   (SML "!(IntInf.fromInt o Char.ord)"
    80     and "!(Char.chr o IntInf.toInt)")
    81   (OCaml "Big'_int.big'_int'_of'_int (Char.code _)"
    82     and "Char.chr (Big'_int.int'_of'_big'_int _)")
    83   (Haskell "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
    84     and "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)")
    85   (Scala "BigInt(_.toInt)"
    86     and "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else error(\"character value out of range\"))")
    87 
    88 
    89 code_const "Orderings.less_eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    90   (SML "!((_ : char) <= _)")
    91   (OCaml "!((_ : char) <= _)")
    92   (Haskell infix 4 "<=")
    93   (Scala infixl 4 "<=")
    94   (Eval infixl 6 "<=")
    95 
    96 code_const "Orderings.less \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    97   (SML "!((_ : char) < _)")
    98   (OCaml "!((_ : char) < _)")
    99   (Haskell infix 4 "<")
   100   (Scala infixl 4 "<")
   101   (Eval infixl 6 "<")
   102 
   103 end
   104