author | haftmann |
Mon, 04 May 2009 14:49:47 +0200 | |
changeset 31032 | 38901ed00ec3 |
parent 28952 | 15a4b2cf8c34 |
permissions | -rw-r--r-- |
31032 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
24999 | 2 |
|
3 |
header {* Monolithic strings (message strings) for code generation *} |
|
4 |
||
5 |
theory Code_Message |
|
27487 | 6 |
imports Plain "~~/src/HOL/List" |
24999 | 7 |
begin |
8 |
||
9 |
subsection {* Datatype of messages *} |
|
10 |
||
11 |
datatype message_string = STR string |
|
12 |
||
28562 | 13 |
lemmas [code del] = message_string.recs message_string.cases |
24999 | 14 |
|
28562 | 15 |
lemma [code]: "size (s\<Colon>message_string) = 0" |
24999 | 16 |
by (cases s) simp_all |
17 |
||
28562 | 18 |
lemma [code]: "message_string_size (s\<Colon>message_string) = 0" |
25673 | 19 |
by (cases s) simp_all |
20 |
||
24999 | 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 {* |
|
28090
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
41 |
fold (fn target => add_literal_message @{const_name STR} target) |
29af3c712d2b
distributed literal code generation out of central infrastructure
haftmann
parents:
28064
diff
changeset
|
42 |
["SML", "OCaml", "Haskell"] |
24999 | 43 |
*} |
44 |
||
45 |
code_reserved SML string |
|
46 |
code_reserved OCaml string |
|
47 |
||
48 |
code_instance message_string :: eq |
|
49 |
(Haskell -) |
|
50 |
||
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28090
diff
changeset
|
51 |
code_const "eq_class.eq \<Colon> message_string \<Rightarrow> message_string \<Rightarrow> bool" |
24999 | 52 |
(SML "!((_ : string) = _)") |
53 |
(OCaml "!((_ : string) = _)") |
|
54 |
(Haskell infixl 4 "==") |
|
55 |
||
56 |
end |