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