author | huffman |
Wed, 20 Jun 2007 17:28:55 +0200 | |
changeset 23438 | dd824e86fa8a |
parent 22849 | 3c41e8492ba6 |
permissions | -rw-r--r-- |
20400 | 1 |
(* ID: $Id$ |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
22665 | 5 |
header {* Monolithic strings for ML *} |
20400 | 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 |
|
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
21 |
are serialized as monolithic ML strings. |
20400 | 22 |
*} |
23 |
||
24 |
||
25 |
subsection {* Datatype of monolithic strings *} |
|
26 |
||
27 |
datatype ml_string = STR string |
|
28 |
||
22849 | 29 |
lemmas [code func del] = ml_string.recs ml_string.cases |
20400 | 30 |
|
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
31 |
lemma [code func]: "size (s\<Colon>ml_string) = 0" |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
32 |
by (cases s) simp_all |
20400 | 33 |
|
34 |
subsection {* ML interface *} |
|
35 |
||
36 |
ML {* |
|
37 |
structure MLString = |
|
38 |
struct |
|
39 |
||
22520 | 40 |
fun mk s = @{term STR} $ HOLogic.mk_string s; |
20400 | 41 |
|
42 |
end; |
|
43 |
*} |
|
44 |
||
45 |
||
46 |
subsection {* Code serialization *} |
|
47 |
||
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
48 |
code_type ml_string |
21113 | 49 |
(SML "string") |
20400 | 50 |
|
51 |
setup {* |
|
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
52 |
let |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
53 |
val charr = @{const_name Char} |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
54 |
val nibbles = [@{const_name Nibble0}, @{const_name Nibble1}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
55 |
@{const_name Nibble2}, @{const_name Nibble3}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
56 |
@{const_name Nibble4}, @{const_name Nibble5}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
57 |
@{const_name Nibble6}, @{const_name Nibble7}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
58 |
@{const_name Nibble8}, @{const_name Nibble9}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
59 |
@{const_name NibbleA}, @{const_name NibbleB}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
60 |
@{const_name NibbleC}, @{const_name NibbleD}, |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
61 |
@{const_name NibbleE}, @{const_name NibbleF}]; |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
62 |
in |
21756 | 63 |
CodegenSerializer.add_pretty_ml_string "SML" |
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
64 |
charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR} |
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
65 |
end |
20400 | 66 |
*} |
67 |
||
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22665
diff
changeset
|
68 |
code_reserved SML string |
21079 | 69 |
|
22552 | 70 |
code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool" |
71 |
(SML "!((_ : string) = _)") |
|
22016 | 72 |
|
20453
855f07fabd76
final syntax for some Isar code generator keywords
haftmann
parents:
20439
diff
changeset
|
73 |
end |