src/HOL/Library/Code_Char.thy
author haftmann
Thu Aug 28 22:09:20 2008 +0200 (2008-08-28)
changeset 28054 2b84d34c5d02
parent 27487 c8a6ce181805
child 28064 d4a6460c53d1
permissions -rw-r--r--
restructured and split code serializer module
     1 (*  Title:      HOL/Library/Code_Char.thy
     2     ID:         $Id$
     3     Author:     Florian Haftmann
     4 *)
     5 
     6 header {* Code generation of pretty characters (and strings) *}
     7 
     8 theory Code_Char
     9 imports Plain "~~/src/HOL/List"
    10 begin
    11 
    12 declare char.recs [code func del] char.cases [code func del]
    13 
    14 lemma [code func]:
    15   "size (c\<Colon>char) = 0"
    16   by (cases c) simp
    17 
    18 lemma [code func]:
    19   "char_size (c\<Colon>char) = 0"
    20   by (cases c) simp
    21 
    22 code_type char
    23   (SML "char")
    24   (OCaml "char")
    25   (Haskell "Char")
    26 
    27 setup {*
    28 let
    29   val charr = @{const_name Char}
    30   val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    31     @{const_name Nibble2}, @{const_name Nibble3},
    32     @{const_name Nibble4}, @{const_name Nibble5},
    33     @{const_name Nibble6}, @{const_name Nibble7},
    34     @{const_name Nibble8}, @{const_name Nibble9},
    35     @{const_name NibbleA}, @{const_name NibbleB},
    36     @{const_name NibbleC}, @{const_name NibbleD},
    37     @{const_name NibbleE}, @{const_name NibbleF}];
    38 in
    39   fold (fn target => Code_Target.add_pretty_char target charr nibbles)
    40     ["SML", "OCaml", "Haskell"]
    41   #> Code_Target.add_pretty_list_string "Haskell"
    42     @{const_name Nil} @{const_name Cons} charr nibbles
    43 end
    44 *}
    45 
    46 code_instance char :: eq
    47   (Haskell -)
    48 
    49 code_reserved SML
    50   char
    51 
    52 code_reserved OCaml
    53   char
    54 
    55 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    56   (SML "!((_ : char) = _)")
    57   (OCaml "!((_ : char) = _)")
    58   (Haskell infixl 4 "==")
    59 
    60 end