src/HOL/Code_Message.thy
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 28952 15a4b2cf8c34
child 31032 38901ed00ec3
permissions -rw-r--r--
simplified method setup;
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Monolithic strings (message strings) for code generation *}
     6 
     7 theory Code_Message
     8 imports Plain "~~/src/HOL/List"
     9 begin
    10 
    11 subsection {* Datatype of messages *}
    12 
    13 datatype message_string = STR string
    14 
    15 lemmas [code del] = message_string.recs message_string.cases
    16 
    17 lemma [code]: "size (s\<Colon>message_string) = 0"
    18   by (cases s) simp_all
    19 
    20 lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    21   by (cases s) simp_all
    22 
    23 subsection {* ML interface *}
    24 
    25 ML {*
    26 structure Message_String =
    27 struct
    28 
    29 fun mk s = @{term STR} $ HOLogic.mk_string s;
    30 
    31 end;
    32 *}
    33 
    34 
    35 subsection {* Code serialization *}
    36 
    37 code_type message_string
    38   (SML "string")
    39   (OCaml "string")
    40   (Haskell "String")
    41 
    42 setup {*
    43   fold (fn target => add_literal_message @{const_name STR} target)
    44     ["SML", "OCaml", "Haskell"]
    45 *}
    46 
    47 code_reserved SML string
    48 code_reserved OCaml string
    49 
    50 code_instance message_string :: eq
    51   (Haskell -)
    52 
    53 code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    54   (SML "!((_ : string) = _)")
    55   (OCaml "!((_ : string) = _)")
    56   (Haskell infixl 4 "==")
    57 
    58 end