--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Message.thy Wed Dec 03 15:58:44 2008 +0100
@@ -0,0 +1,58 @@
+(* ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+header {* Monolithic strings (message strings) for code generation *}
+
+theory Code_Message
+imports Plain "~~/src/HOL/List"
+begin
+
+subsection {* Datatype of messages *}
+
+datatype message_string = STR string
+
+lemmas [code del] = message_string.recs message_string.cases
+
+lemma [code]: "size (s\<Colon>message_string) = 0"
+ by (cases s) simp_all
+
+lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
+ by (cases s) simp_all
+
+subsection {* ML interface *}
+
+ML {*
+structure Message_String =
+struct
+
+fun mk s = @{term STR} $ HOLogic.mk_string s;
+
+end;
+*}
+
+
+subsection {* Code serialization *}
+
+code_type message_string
+ (SML "string")
+ (OCaml "string")
+ (Haskell "String")
+
+setup {*
+ fold (fn target => add_literal_message @{const_name STR} target)
+ ["SML", "OCaml", "Haskell"]
+*}
+
+code_reserved SML string
+code_reserved OCaml string
+
+code_instance message_string :: eq
+ (Haskell -)
+
+code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
+ (SML "!((_ : string) = _)")
+ (OCaml "!((_ : string) = _)")
+ (Haskell infixl 4 "==")
+
+end