src/HOL/Library/Code_Char.thy
author haftmann
Tue Oct 27 15:32:20 2009 +0100 (2009-10-27)
changeset 33234 a5eba0447559
parent 32657 5f13912245ff
child 37222 4d984bc33c66
permissions -rw-r--r--
added implode and explode
     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 List Code_Evaluation Main
     9 begin
    10 
    11 code_type char
    12   (SML "char")
    13   (OCaml "char")
    14   (Haskell "Char")
    15 
    16 setup {*
    17   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
    18   #> String_Code.add_literal_list_string "Haskell"
    19 *}
    20 
    21 code_instance char :: eq
    22   (Haskell -)
    23 
    24 code_reserved SML
    25   char
    26 
    27 code_reserved OCaml
    28   char
    29 
    30 code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    31   (SML "!((_ : char) = _)")
    32   (OCaml "!((_ : char) = _)")
    33   (Haskell infixl 4 "==")
    34 
    35 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    36   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    37 
    38 
    39 definition implode :: "string \<Rightarrow> String.literal" where
    40   "implode = STR"
    41 
    42 primrec explode :: "String.literal \<Rightarrow> string" where
    43   "explode (STR s) = s"
    44 
    45 lemma [code]:
    46   "literal_case f s = f (explode s)"
    47   "literal_rec f s = f (explode s)"
    48   by (cases s, simp)+
    49 
    50 code_reserved SML String
    51 
    52 code_const implode
    53   (SML "String.implode")
    54   (OCaml "failwith/ \"implode\"")
    55   (Haskell "_")
    56 
    57 code_const explode
    58   (SML "String.explode")
    59   (OCaml "failwith/ \"explode\"")
    60   (Haskell "_")
    61 
    62 end