1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Oct 12 10:26:18 2007 +0200
     1.3 @@ -0,0 +1,50 @@
     1.4 +(*  Title:      HOL/Library/Code_Char.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann
     1.7 +*)
     1.8 +
     1.9 +header {* Code generation of pretty characters (and strings) *}
    1.10 +
    1.11 +theory Code_Char
    1.12 +imports List
    1.13 +begin
    1.14 +
    1.15 +code_type char
    1.16 +  (SML "char")
    1.17 +  (OCaml "char")
    1.18 +  (Haskell "Char")
    1.19 +
    1.20 +setup {*
    1.21 +let
    1.22 +  val charr = @{const_name Char}
    1.23 +  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    1.24 +    @{const_name Nibble2}, @{const_name Nibble3},
    1.25 +    @{const_name Nibble4}, @{const_name Nibble5},
    1.26 +    @{const_name Nibble6}, @{const_name Nibble7},
    1.27 +    @{const_name Nibble8}, @{const_name Nibble9},
    1.28 +    @{const_name NibbleA}, @{const_name NibbleB},
    1.29 +    @{const_name NibbleC}, @{const_name NibbleD},
    1.30 +    @{const_name NibbleE}, @{const_name NibbleF}];
    1.31 +in
    1.32 +  fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
    1.33 +    ["SML", "OCaml", "Haskell"]
    1.34 +  #> CodeTarget.add_pretty_list_string "Haskell"
    1.35 +    @{const_name Nil} @{const_name Cons} charr nibbles
    1.36 +end
    1.37 +*}
    1.38 +
    1.39 +code_instance char :: eq
    1.40 +  (Haskell -)
    1.41 +
    1.42 +code_reserved SML
    1.43 +  char
    1.44 +
    1.45 +code_reserved OCaml
    1.46 +  char
    1.47 +
    1.48 +code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    1.49 +  (SML "!((_ : char) = _)")
    1.50 +  (OCaml "!((_ : char) = _)")
    1.51 +  (Haskell infixl 4 "==")
    1.52 +
    1.53 +end