1 (* ID: $Id$ |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Monolithic strings for ML *} |
|
6 |
|
7 theory MLString |
|
8 imports List |
|
9 begin |
|
10 |
|
11 subsection {* Motivation *} |
|
12 |
|
13 text {* |
|
14 Strings are represented in HOL as list of characters. |
|
15 For code generation to Haskell, this is no problem |
|
16 since in Haskell "abc" is equivalent to ['a', 'b', 'c']. |
|
17 On the other hand, in ML all strings have to |
|
18 be represented as list of characters which |
|
19 is awkward to read. This theory provides a distinguished |
|
20 datatype for strings which then by convention |
|
21 are serialized as monolithic ML strings. |
|
22 *} |
|
23 |
|
24 |
|
25 subsection {* Datatype of monolithic strings *} |
|
26 |
|
27 datatype ml_string = STR string |
|
28 |
|
29 lemmas [code func del] = ml_string.recs ml_string.cases |
|
30 |
|
31 lemma [code func]: "size (s\<Colon>ml_string) = 0" |
|
32 by (cases s) simp_all |
|
33 |
|
34 subsection {* ML interface *} |
|
35 |
|
36 ML {* |
|
37 structure MLString = |
|
38 struct |
|
39 |
|
40 fun mk s = @{term STR} $ HOLogic.mk_string s; |
|
41 |
|
42 end; |
|
43 *} |
|
44 |
|
45 |
|
46 subsection {* Code serialization *} |
|
47 |
|
48 code_type ml_string |
|
49 (SML "string") |
|
50 |
|
51 setup {* |
|
52 let |
|
53 val charr = @{const_name Char} |
|
54 val nibbles = [@{const_name Nibble0}, @{const_name Nibble1}, |
|
55 @{const_name Nibble2}, @{const_name Nibble3}, |
|
56 @{const_name Nibble4}, @{const_name Nibble5}, |
|
57 @{const_name Nibble6}, @{const_name Nibble7}, |
|
58 @{const_name Nibble8}, @{const_name Nibble9}, |
|
59 @{const_name NibbleA}, @{const_name NibbleB}, |
|
60 @{const_name NibbleC}, @{const_name NibbleD}, |
|
61 @{const_name NibbleE}, @{const_name NibbleF}]; |
|
62 in |
|
63 CodegenSerializer.add_pretty_ml_string "SML" |
|
64 charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR} |
|
65 end |
|
66 *} |
|
67 |
|
68 code_reserved SML string |
|
69 |
|
70 code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool" |
|
71 (SML "!((_ : string) = _)") |
|
72 |
|
73 end |
|