haftmann@24999: (*  Title:      HOL/Library/Code_Char.thy
haftmann@24999:     Author:     Florian Haftmann
haftmann@24999: *)
haftmann@24999: 
haftmann@24999: header {* Code generation of pretty characters (and strings) *}
haftmann@24999: 
haftmann@24999: theory Code_Char
haftmann@30663: imports List Code_Eval Main
haftmann@24999: begin
haftmann@24999: 
haftmann@24999: code_type char
haftmann@24999:   (SML "char")
haftmann@24999:   (OCaml "char")
haftmann@24999:   (Haskell "Char")
haftmann@24999: 
haftmann@24999: setup {*
haftmann@31053:   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] 
haftmann@31053:   #> String_Code.add_literal_list_string "Haskell"
haftmann@24999: *}
haftmann@24999: 
haftmann@24999: code_instance char :: eq
haftmann@24999:   (Haskell -)
haftmann@24999: 
haftmann@24999: code_reserved SML
haftmann@24999:   char
haftmann@24999: 
haftmann@24999: code_reserved OCaml
haftmann@24999:   char
haftmann@24999: 
haftmann@28346: code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
haftmann@24999:   (SML "!((_ : char) = _)")
haftmann@24999:   (OCaml "!((_ : char) = _)")
haftmann@24999:   (Haskell infixl 4 "==")
haftmann@24999: 
haftmann@28228: code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term"
haftmann@31046:   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
haftmann@28228: 
haftmann@24999: end