src/HOL/Code_Message.thy
changeset 31048 ac146fc38b51
parent 31047 c13b0406c039
child 31049 396d4d6a1594
     1.1 --- a/src/HOL/Code_Message.thy	Wed May 06 16:01:05 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,56 +0,0 @@
     1.4 -(* Author: Florian Haftmann, TU Muenchen *)
     1.5 -
     1.6 -header {* Monolithic strings (message strings) for code generation *}
     1.7 -
     1.8 -theory Code_Message
     1.9 -imports Plain "~~/src/HOL/List"
    1.10 -begin
    1.11 -
    1.12 -subsection {* Datatype of messages *}
    1.13 -
    1.14 -datatype message_string = STR string
    1.15 -
    1.16 -lemmas [code del] = message_string.recs message_string.cases
    1.17 -
    1.18 -lemma [code]: "size (s\<Colon>message_string) = 0"
    1.19 -  by (cases s) simp_all
    1.20 -
    1.21 -lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
    1.22 -  by (cases s) simp_all
    1.23 -
    1.24 -subsection {* ML interface *}
    1.25 -
    1.26 -ML {*
    1.27 -structure Message_String =
    1.28 -struct
    1.29 -
    1.30 -fun mk s = @{term STR} $ HOLogic.mk_string s;
    1.31 -
    1.32 -end;
    1.33 -*}
    1.34 -
    1.35 -
    1.36 -subsection {* Code serialization *}
    1.37 -
    1.38 -code_type message_string
    1.39 -  (SML "string")
    1.40 -  (OCaml "string")
    1.41 -  (Haskell "String")
    1.42 -
    1.43 -setup {*
    1.44 -  fold (fn target => add_literal_message @{const_name STR} target)
    1.45 -    ["SML", "OCaml", "Haskell"]
    1.46 -*}
    1.47 -
    1.48 -code_reserved SML string
    1.49 -code_reserved OCaml string
    1.50 -
    1.51 -code_instance message_string :: eq
    1.52 -  (Haskell -)
    1.53 -
    1.54 -code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
    1.55 -  (SML "!((_ : string) = _)")
    1.56 -  (OCaml "!((_ : string) = _)")
    1.57 -  (Haskell infixl 4 "==")
    1.58 -
    1.59 -end