src/HOL/Library/Code_Message.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 28054 2b84d34c5d02
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     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 func del] = message_string.recs message_string.cases
    16 
    17 lemma [code func]: "size (s\<Colon>message_string) = 0"
    18   by (cases s) simp_all
    19 
    20 lemma [code func]: "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 let
    44   val charr = @{const_name Char}
    45   val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    46     @{const_name Nibble2}, @{const_name Nibble3},
    47     @{const_name Nibble4}, @{const_name Nibble5},
    48     @{const_name Nibble6}, @{const_name Nibble7},
    49     @{const_name Nibble8}, @{const_name Nibble9},
    50     @{const_name NibbleA}, @{const_name NibbleB},
    51     @{const_name NibbleC}, @{const_name NibbleD},
    52     @{const_name NibbleE}, @{const_name NibbleF}];
    53 in
    54   fold (fn target => CodeTarget.add_pretty_message target
    55     charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
    56   ["SML", "OCaml", "Haskell"]
    57 end
    58 *}
    59 
    60 code_reserved SML string
    61 code_reserved OCaml string
    62 
    63 code_instance message_string :: eq
    64   (Haskell -)
    65 
    66 code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    67   (SML "!((_ : string) = _)")
    68   (OCaml "!((_ : string) = _)")
    69   (Haskell infixl 4 "==")
    70 
    71 end