author | haftmann |
Fri, 20 Oct 2006 17:07:27 +0200 | |
changeset 21079 | 747d716e98d0 |
parent 20699 | 0cc77abb185a |
child 21113 | 5b76e541cc0a |
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 |
section {* Monolithic strings for ML *} |
|
12 |
||
13 |
subsection {* Motivation *} |
|
14 |
||
15 |
text {* |
|
16 |
Strings are represented in HOL as list of characters. |
|
17 |
For code generation to Haskell, this is no problem |
|
18 |
since in Haskell "abc" is equivalent to ['a', 'b', 'c']. |
|
19 |
On the other hand, in ML all strings have to |
|
20 |
be represented as list of characters which |
|
21 |
is awkward to read. This theory provides a distinguished |
|
22 |
datatype for strings which then by convention |
|
23 |
are serialized as monolithic ML strings. Note |
|
24 |
that in Haskell these strings are identified |
|
25 |
with Haskell strings. |
|
26 |
*} |
|
27 |
||
28 |
||
29 |
subsection {* Datatype of monolithic strings *} |
|
30 |
||
31 |
datatype ml_string = STR string |
|
32 |
||
33 |
consts |
|
34 |
explode :: "ml_string \<Rightarrow> string" |
|
35 |
||
36 |
primrec |
|
37 |
"explode (STR s) = s" |
|
38 |
||
39 |
||
40 |
subsection {* ML interface *} |
|
41 |
||
42 |
ML {* |
|
43 |
structure MLString = |
|
44 |
struct |
|
45 |
||
46 |
local |
|
47 |
val thy = the_context (); |
|
48 |
val const_STR = Sign.intern_const thy "STR"; |
|
49 |
in |
|
50 |
val typ_ml_string = Type (Sign.intern_type thy "ml_string", []); |
|
51 |
fun term_ml_string s = Const (const_STR, HOList.typ_string --> typ_ml_string) |
|
52 |
$ HOList.term_string s |
|
53 |
end; |
|
54 |
||
55 |
end; |
|
56 |
*} |
|
57 |
||
58 |
||
59 |
subsection {* Code serialization *} |
|
60 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
61 |
code_type ml_string |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
62 |
(SML target_atom "string") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
63 |
(Haskell target_atom "String") |
20400 | 64 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
65 |
code_const STR |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
66 |
(Haskell "_") |
20400 | 67 |
|
68 |
setup {* |
|
20699 | 69 |
CodegenSerializer.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR" |
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
70 |
HOList.print_char HOList.print_string "String.implode" |
20400 | 71 |
*} |
72 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
73 |
code_const explode |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
74 |
(SML target_atom "String.explode") |
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
75 |
(Haskell "_") |
20400 | 76 |
|
21079 | 77 |
code_reserved SML string explode |
78 |
code_reserved Haskell string |
|
79 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
80 |
end |