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
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@24999
    15
lemmas [code func del] = message_string.recs message_string.cases
haftmann@24999
    16
haftmann@24999
    17
lemma [code func]: "size (s\<Colon>message_string) = 0"
haftmann@24999
    18
  by (cases s) simp_all
haftmann@24999
    19
berghofe@25673
    20
lemma [code func]: "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@24999
    43
let
haftmann@24999
    44
  val charr = @{const_name Char}
haftmann@24999
    45
  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
haftmann@24999
    46
    @{const_name Nibble2}, @{const_name Nibble3},
haftmann@24999
    47
    @{const_name Nibble4}, @{const_name Nibble5},
haftmann@24999
    48
    @{const_name Nibble6}, @{const_name Nibble7},
haftmann@24999
    49
    @{const_name Nibble8}, @{const_name Nibble9},
haftmann@24999
    50
    @{const_name NibbleA}, @{const_name NibbleB},
haftmann@24999
    51
    @{const_name NibbleC}, @{const_name NibbleD},
haftmann@24999
    52
    @{const_name NibbleE}, @{const_name NibbleF}];
haftmann@24999
    53
in
haftmann@24999
    54
  fold (fn target => CodeTarget.add_pretty_message target
haftmann@24999
    55
    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
haftmann@24999
    56
  ["SML", "OCaml", "Haskell"]
haftmann@24999
    57
end
haftmann@24999
    58
*}
haftmann@24999
    59
haftmann@24999
    60
code_reserved SML string
haftmann@24999
    61
code_reserved OCaml string
haftmann@24999
    62
haftmann@24999
    63
code_instance message_string :: eq
haftmann@24999
    64
  (Haskell -)
haftmann@24999
    65
haftmann@24999
    66
code_const "op = \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool"
haftmann@24999
    67
  (SML "!((_ : string) = _)")
haftmann@24999
    68
  (OCaml "!((_ : string) = _)")
haftmann@24999
    69
  (Haskell infixl 4 "==")
haftmann@24999
    70
haftmann@24999
    71
end