src/HOL/Library/Code_Char.thy
author bulwahn
Thu Sep 09 14:38:14 2010 +0200 (2010-09-09)
changeset 39250 548a3e5521ab
parent 38857 97775f3e8722
child 39272 0b61951d2682
permissions -rw-r--r--
changing String.literal to a type instead of a datatype
     1 (*  Title:      HOL/Library/Code_Char.thy
     2     Author:     Florian Haftmann
     3 *)
     4 
     5 header {* Code generation of pretty characters (and strings) *}
     6 
     7 theory Code_Char
     8 imports List Code_Evaluation Main
     9 begin
    10 
    11 code_type char
    12   (SML "char")
    13   (OCaml "char")
    14   (Haskell "Char")
    15   (Scala "Char")
    16 
    17 setup {*
    18   fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"] 
    19   #> String_Code.add_literal_list_string "Haskell"
    20 *}
    21 
    22 code_instance char :: equal
    23   (Haskell -)
    24 
    25 code_reserved SML
    26   char
    27 
    28 code_reserved OCaml
    29   char
    30 
    31 code_reserved Scala
    32   char
    33 
    34 code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
    35   (SML "!((_ : char) = _)")
    36   (OCaml "!((_ : char) = _)")
    37   (Haskell infixl 4 "==")
    38   (Scala infixl 5 "==")
    39 
    40 code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"
    41   (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))")
    42 
    43 
    44 definition implode :: "string \<Rightarrow> String.literal" where
    45   "implode = STR"
    46 
    47 code_reserved SML String
    48 
    49 code_const implode
    50   (SML "String.implode")
    51   (OCaml "failwith/ \"implode\"")
    52   (Haskell "_")
    53   (Scala "!(\"\" ++/ _)")
    54 
    55 code_const explode
    56   (SML "String.explode")
    57   (OCaml "failwith/ \"explode\"")
    58   (Haskell "_")
    59   (Scala "!(_.toList)")
    60 
    61 end