(*  Title:      HOL/Library/Code_Char.thy

     Author:     Florian Haftmann

 *)

 header {* Code generation of pretty characters (and strings) *}

 theory Code_Char

 imports List Code_Evaluation Main

 begin

 code_type char

   (SML "char")

   (OCaml "char")

   (Haskell "Prelude.Char")

   (Scala "Char")

 setup {*

   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 

   #> String_Code.add_literal_list_string "Haskell"

 *}

 code_instance char :: equal

   (Haskell -)

 code_reserved SML

   char

 code_reserved OCaml

   char

 code_reserved Scala

   char

 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"

   (SML "!((_ : char) = _)")

   (OCaml "!((_ : char) = _)")

   (Haskell infix 4 "==")

   (Scala infixl 5 "==")

 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"

   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")

 definition implode :: "string \<Rightarrow> String.literal" where

   "implode = STR"

 code_reserved SML String

 code_const implode

   (SML "String.implode")

   (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)")

   (Haskell "_")

   (Scala "!(\"\" ++/ _)")

 code_const explode

   (SML "String.explode")

   (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) [])")

   (Haskell "_")

   (Scala "!(_.toList)")

 end