author | krauss |
Sat, 07 Apr 2007 18:54:30 +0200 | |
changeset 22612 | 1f017e6a0395 |
parent 22552 | 70f5cf8a0fad |
child 22665 | cf152ff55d16 |
permissions | -rw-r--r-- |
20400 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Monolithic strings for ML *} |
|
6 |
||
7 |
theory MLString |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
8 |
imports List |
20400 | 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. Note |
|
22 |
that in Haskell these strings are identified |
|
23 |
with Haskell strings. |
|
24 |
*} |
|
25 |
||
26 |
||
27 |
subsection {* Datatype of monolithic strings *} |
|
28 |
||
29 |
datatype ml_string = STR string |
|
30 |
||
22520 | 31 |
fun |
20400 | 32 |
explode :: "ml_string \<Rightarrow> string" |
22520 | 33 |
where |
20400 | 34 |
"explode (STR s) = s" |
35 |
||
36 |
||
37 |
subsection {* ML interface *} |
|
38 |
||
39 |
ML {* |
|
40 |
structure MLString = |
|
41 |
struct |
|
42 |
||
22520 | 43 |
fun mk s = @{term STR} $ HOLogic.mk_string s; |
20400 | 44 |
|
45 |
end; |
|
46 |
*} |
|
47 |
||
48 |
||
49 |
subsection {* Code serialization *} |
|
50 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
51 |
code_type ml_string |
21113 | 52 |
(SML "string") |
53 |
(Haskell "String") |
|
20400 | 54 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
55 |
code_const STR |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
56 |
(Haskell "_") |
20400 | 57 |
|
58 |
setup {* |
|
21756 | 59 |
CodegenSerializer.add_pretty_ml_string "SML" |
22520 | 60 |
@{const_name Nil} @{const_name Cons} @{const_name STR} |
21756 | 61 |
ML_Syntax.print_char ML_Syntax.print_string "String.implode" |
20400 | 62 |
*} |
63 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
64 |
code_const explode |
21113 | 65 |
(SML "String.explode") |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
66 |
(Haskell "_") |
20400 | 67 |
|
21079 | 68 |
code_reserved SML string explode |
69 |
||
22552 | 70 |
code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool" |
71 |
(SML "!((_ : string) = _)") |
|
72 |
(Haskell infixl 4 "==") |
|
73 |
||
74 |
code_instance ml_string :: eq (Haskell -) |
|
75 |
||
22016 | 76 |
text {* disable something ugly *} |
77 |
||
78 |
code_const "ml_string_rec" and "ml_string_case" and "size \<Colon> ml_string \<Rightarrow> nat" |
|
79 |
(SML "!((_); (_); raise Fail \"ml'_string'_rec\")" |
|
80 |
and "!((_); (_); raise Fail \"ml'_string'_case\")" |
|
81 |
and "!((_); raise Fail \"size'_ml'_string\")") |
|
82 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
83 |
end |