src/HOL/Library/Code_Char.thy
author haftmann
Tue Sep 02 20:38:17 2008 +0200 (2008-09-02)
changeset 28090 29af3c712d2b
parent 28064 d4a6460c53d1
child 28228 7ebe8dc06cbb
permissions -rw-r--r--
distributed literal code generation out of central infrastructure
     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   fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] 
    29   #> add_literal_list_string "Haskell"
    30 *}
    31 
    32 code_instance char :: eq
    33   (Haskell -)
    34 
    35 code_reserved SML
    36   char
    37 
    38 code_reserved OCaml
    39   char
    40 
    41 code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    42   (SML "!((_ : char) = _)")
    43   (OCaml "!((_ : char) = _)")
    44   (Haskell infixl 4 "==")
    45 
    46 end