equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
|
2 |
|
3 header {* Monolithic strings (message strings) for code generation *} |
|
4 |
|
5 theory Code_Message |
|
6 imports Plain "~~/src/HOL/List" |
|
7 begin |
|
8 |
|
9 subsection {* Datatype of messages *} |
|
10 |
|
11 datatype message_string = STR string |
|
12 |
|
13 lemmas [code del] = message_string.recs message_string.cases |
|
14 |
|
15 lemma [code]: "size (s\<Colon>message_string) = 0" |
|
16 by (cases s) simp_all |
|
17 |
|
18 lemma [code]: "message_string_size (s\<Colon>message_string) = 0" |
|
19 by (cases s) simp_all |
|
20 |
|
21 subsection {* ML interface *} |
|
22 |
|
23 ML {* |
|
24 structure Message_String = |
|
25 struct |
|
26 |
|
27 fun mk s = @{term STR} $ HOLogic.mk_string s; |
|
28 |
|
29 end; |
|
30 *} |
|
31 |
|
32 |
|
33 subsection {* Code serialization *} |
|
34 |
|
35 code_type message_string |
|
36 (SML "string") |
|
37 (OCaml "string") |
|
38 (Haskell "String") |
|
39 |
|
40 setup {* |
|
41 fold (fn target => add_literal_message @{const_name STR} target) |
|
42 ["SML", "OCaml", "Haskell"] |
|
43 *} |
|
44 |
|
45 code_reserved SML string |
|
46 code_reserved OCaml string |
|
47 |
|
48 code_instance message_string :: eq |
|
49 (Haskell -) |
|
50 |
|
51 code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool" |
|
52 (SML "!((_ : string) = _)") |
|
53 (OCaml "!((_ : string) = _)") |
|
54 (Haskell infixl 4 "==") |
|
55 |
|
56 end |
|