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@32657: imports List Code_Evaluation Main
haftmann@24999: begin
haftmann@24999: 
haftmann@24999: code_type char
haftmann@24999:   (SML "char")
haftmann@24999:   (OCaml "char")
haftmann@49446:   (Haskell "Prelude.Char")
haftmann@37221:   (Scala "Char")
haftmann@24999: 
haftmann@24999: setup {*
haftmann@37221:   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
haftmann@31053:   #> String_Code.add_literal_list_string "Haskell"
haftmann@24999: *}
haftmann@24999: 
haftmann@39086: code_instance char :: equal
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@37221: code_reserved Scala
haftmann@37221:   char
haftmann@37221: 
haftmann@39086: code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
haftmann@24999:   (SML "!((_ : char) = _)")
haftmann@24999:   (OCaml "!((_ : char) = _)")
haftmann@39499:   (Haskell infix 4 "==")
haftmann@37221:   (Scala infixl 5 "==")
haftmann@24999: 
haftmann@32657: code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
haftmann@31046:   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
haftmann@28228: 
haftmann@33226: 
haftmann@33226: definition implode :: "string \<Rightarrow> String.literal" where
haftmann@33226:   "implode = STR"
haftmann@33226: 
haftmann@33226: code_reserved SML String
haftmann@33226: 
haftmann@33226: code_const implode
haftmann@33226:   (SML "String.implode")
bulwahn@43469:   (OCaml "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)")
haftmann@33226:   (Haskell "_")
haftmann@37434:   (Scala "!(\"\" ++/ _)")
haftmann@33226: 
haftmann@33226: code_const explode
haftmann@33226:   (SML "String.explode")
bulwahn@43469:   (OCaml "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])")
haftmann@33226:   (Haskell "_")
haftmann@37434:   (Scala "!(_.toList)")
haftmann@33226: 
haftmann@24999: end