haftmann@31051
|
1 |
(* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *)
|
haftmann@31051
|
2 |
|
haftmann@31051
|
3 |
header {* Character and string types *}
|
haftmann@31051
|
4 |
|
haftmann@31051
|
5 |
theory String
|
haftmann@31051
|
6 |
imports List
|
haftmann@31055
|
7 |
uses
|
wenzelm@35118
|
8 |
("Tools/string_syntax.ML")
|
haftmann@31055
|
9 |
("Tools/string_code.ML")
|
haftmann@31051
|
10 |
begin
|
haftmann@31051
|
11 |
|
haftmann@31051
|
12 |
subsection {* Characters *}
|
haftmann@31051
|
13 |
|
haftmann@31051
|
14 |
datatype nibble =
|
haftmann@31051
|
15 |
Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
|
haftmann@31051
|
16 |
| Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
|
haftmann@31051
|
17 |
|
haftmann@31051
|
18 |
lemma UNIV_nibble:
|
haftmann@31051
|
19 |
"UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
|
haftmann@31051
|
20 |
Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
|
haftmann@31051
|
21 |
proof (rule UNIV_eq_I)
|
haftmann@31051
|
22 |
fix x show "x \<in> ?A" by (cases x) simp_all
|
haftmann@31051
|
23 |
qed
|
haftmann@31051
|
24 |
|
haftmann@31051
|
25 |
instance nibble :: finite
|
haftmann@31051
|
26 |
by default (simp add: UNIV_nibble)
|
haftmann@31051
|
27 |
|
haftmann@31051
|
28 |
datatype char = Char nibble nibble
|
haftmann@31051
|
29 |
-- "Note: canonical order of character encoding coincides with standard term ordering"
|
haftmann@31051
|
30 |
|
haftmann@31051
|
31 |
lemma UNIV_char:
|
haftmann@31051
|
32 |
"UNIV = image (split Char) (UNIV \<times> UNIV)"
|
haftmann@31051
|
33 |
proof (rule UNIV_eq_I)
|
haftmann@31051
|
34 |
fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
|
haftmann@31051
|
35 |
qed
|
haftmann@31051
|
36 |
|
haftmann@31051
|
37 |
instance char :: finite
|
haftmann@31051
|
38 |
by default (simp add: UNIV_char)
|
haftmann@31051
|
39 |
|
haftmann@31051
|
40 |
lemma size_char [code, simp]:
|
haftmann@31051
|
41 |
"size (c::char) = 0" by (cases c) simp
|
haftmann@31051
|
42 |
|
haftmann@31051
|
43 |
lemma char_size [code, simp]:
|
haftmann@31051
|
44 |
"char_size (c::char) = 0" by (cases c) simp
|
haftmann@31051
|
45 |
|
haftmann@31051
|
46 |
primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
|
haftmann@31051
|
47 |
"nibble_pair_of_char (Char n m) = (n, m)"
|
haftmann@31051
|
48 |
|
haftmann@31051
|
49 |
setup {*
|
haftmann@31051
|
50 |
let
|
haftmann@33061
|
51 |
val nibbles = map_range (Thm.cterm_of @{theory} o HOLogic.mk_nibble) 16;
|
haftmann@31051
|
52 |
val thms = map_product
|
haftmann@31051
|
53 |
(fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
|
haftmann@31051
|
54 |
nibbles nibbles;
|
haftmann@31051
|
55 |
in
|
wenzelm@43311
|
56 |
Global_Theory.note_thmss ""
|
wenzelm@39814
|
57 |
[((@{binding nibble_pair_of_char_simps}, []), [(thms, [])])]
|
haftmann@31051
|
58 |
#-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
|
haftmann@31051
|
59 |
end
|
haftmann@31051
|
60 |
*}
|
haftmann@31051
|
61 |
|
haftmann@32061
|
62 |
lemma char_case_nibble_pair [code, code_unfold]:
|
haftmann@31051
|
63 |
"char_case f = split f o nibble_pair_of_char"
|
nipkow@39535
|
64 |
by (simp add: fun_eq_iff split: char.split)
|
haftmann@31051
|
65 |
|
haftmann@32061
|
66 |
lemma char_rec_nibble_pair [code, code_unfold]:
|
haftmann@31051
|
67 |
"char_rec f = split f o nibble_pair_of_char"
|
haftmann@31051
|
68 |
unfolding char_case_nibble_pair [symmetric]
|
nipkow@39535
|
69 |
by (simp add: fun_eq_iff split: char.split)
|
haftmann@31051
|
70 |
|
haftmann@31051
|
71 |
syntax
|
haftmann@31051
|
72 |
"_Char" :: "xstr => char" ("CHR _")
|
haftmann@31051
|
73 |
|
haftmann@31051
|
74 |
|
haftmann@31051
|
75 |
subsection {* Strings *}
|
haftmann@31051
|
76 |
|
bulwahn@43034
|
77 |
type_synonym string = "char list"
|
haftmann@31051
|
78 |
|
haftmann@31051
|
79 |
syntax
|
haftmann@31051
|
80 |
"_String" :: "xstr => string" ("_")
|
haftmann@31051
|
81 |
|
wenzelm@35118
|
82 |
use "Tools/string_syntax.ML"
|
wenzelm@35123
|
83 |
setup String_Syntax.setup
|
haftmann@31051
|
84 |
|
haftmann@31493
|
85 |
definition chars :: string where
|
haftmann@31493
|
86 |
"chars = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
|
haftmann@31493
|
87 |
Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
|
haftmann@31493
|
88 |
Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
|
haftmann@31493
|
89 |
Char Nibble0 Nibble9, Char Nibble0 NibbleA, Char Nibble0 NibbleB,
|
haftmann@31493
|
90 |
Char Nibble0 NibbleC, Char Nibble0 NibbleD, Char Nibble0 NibbleE,
|
haftmann@31493
|
91 |
Char Nibble0 NibbleF, Char Nibble1 Nibble0, Char Nibble1 Nibble1,
|
haftmann@31493
|
92 |
Char Nibble1 Nibble2, Char Nibble1 Nibble3, Char Nibble1 Nibble4,
|
haftmann@31493
|
93 |
Char Nibble1 Nibble5, Char Nibble1 Nibble6, Char Nibble1 Nibble7,
|
haftmann@31493
|
94 |
Char Nibble1 Nibble8, Char Nibble1 Nibble9, Char Nibble1 NibbleA,
|
haftmann@31493
|
95 |
Char Nibble1 NibbleB, Char Nibble1 NibbleC, Char Nibble1 NibbleD,
|
haftmann@31493
|
96 |
Char Nibble1 NibbleE, Char Nibble1 NibbleF, CHR '' '', CHR ''!'',
|
haftmann@31493
|
97 |
Char Nibble2 Nibble2, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'',
|
haftmann@31493
|
98 |
Char Nibble2 Nibble7, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','',
|
haftmann@31493
|
99 |
CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'',
|
haftmann@31493
|
100 |
CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'',
|
haftmann@31493
|
101 |
CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'',
|
haftmann@31493
|
102 |
CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'',
|
haftmann@31493
|
103 |
CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'',
|
haftmann@31493
|
104 |
CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'',
|
haftmann@31493
|
105 |
CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', Char Nibble5 NibbleC,
|
haftmann@31493
|
106 |
CHR '']'', CHR ''^'', CHR ''_'', Char Nibble6 Nibble0, CHR ''a'', CHR ''b'',
|
haftmann@31493
|
107 |
CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'',
|
haftmann@31493
|
108 |
CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'',
|
haftmann@31493
|
109 |
CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'',
|
haftmann@31493
|
110 |
CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'',
|
haftmann@31493
|
111 |
Char Nibble7 NibbleF, Char Nibble8 Nibble0, Char Nibble8 Nibble1,
|
haftmann@31493
|
112 |
Char Nibble8 Nibble2, Char Nibble8 Nibble3, Char Nibble8 Nibble4,
|
haftmann@31493
|
113 |
Char Nibble8 Nibble5, Char Nibble8 Nibble6, Char Nibble8 Nibble7,
|
haftmann@31493
|
114 |
Char Nibble8 Nibble8, Char Nibble8 Nibble9, Char Nibble8 NibbleA,
|
haftmann@31493
|
115 |
Char Nibble8 NibbleB, Char Nibble8 NibbleC, Char Nibble8 NibbleD,
|
haftmann@31493
|
116 |
Char Nibble8 NibbleE, Char Nibble8 NibbleF, Char Nibble9 Nibble0,
|
haftmann@31493
|
117 |
Char Nibble9 Nibble1, Char Nibble9 Nibble2, Char Nibble9 Nibble3,
|
haftmann@31493
|
118 |
Char Nibble9 Nibble4, Char Nibble9 Nibble5, Char Nibble9 Nibble6,
|
haftmann@31493
|
119 |
Char Nibble9 Nibble7, Char Nibble9 Nibble8, Char Nibble9 Nibble9,
|
haftmann@31493
|
120 |
Char Nibble9 NibbleA, Char Nibble9 NibbleB, Char Nibble9 NibbleC,
|
haftmann@31493
|
121 |
Char Nibble9 NibbleD, Char Nibble9 NibbleE, Char Nibble9 NibbleF,
|
haftmann@31493
|
122 |
Char NibbleA Nibble0, Char NibbleA Nibble1, Char NibbleA Nibble2,
|
haftmann@31493
|
123 |
Char NibbleA Nibble3, Char NibbleA Nibble4, Char NibbleA Nibble5,
|
haftmann@31493
|
124 |
Char NibbleA Nibble6, Char NibbleA Nibble7, Char NibbleA Nibble8,
|
haftmann@31493
|
125 |
Char NibbleA Nibble9, Char NibbleA NibbleA, Char NibbleA NibbleB,
|
haftmann@31493
|
126 |
Char NibbleA NibbleC, Char NibbleA NibbleD, Char NibbleA NibbleE,
|
haftmann@31493
|
127 |
Char NibbleA NibbleF, Char NibbleB Nibble0, Char NibbleB Nibble1,
|
haftmann@31493
|
128 |
Char NibbleB Nibble2, Char NibbleB Nibble3, Char NibbleB Nibble4,
|
haftmann@31493
|
129 |
Char NibbleB Nibble5, Char NibbleB Nibble6, Char NibbleB Nibble7,
|
haftmann@31493
|
130 |
Char NibbleB Nibble8, Char NibbleB Nibble9, Char NibbleB NibbleA,
|
haftmann@31493
|
131 |
Char NibbleB NibbleB, Char NibbleB NibbleC, Char NibbleB NibbleD,
|
haftmann@31493
|
132 |
Char NibbleB NibbleE, Char NibbleB NibbleF, Char NibbleC Nibble0,
|
haftmann@31493
|
133 |
Char NibbleC Nibble1, Char NibbleC Nibble2, Char NibbleC Nibble3,
|
haftmann@31493
|
134 |
Char NibbleC Nibble4, Char NibbleC Nibble5, Char NibbleC Nibble6,
|
haftmann@31493
|
135 |
Char NibbleC Nibble7, Char NibbleC Nibble8, Char NibbleC Nibble9,
|
haftmann@31493
|
136 |
Char NibbleC NibbleA, Char NibbleC NibbleB, Char NibbleC NibbleC,
|
haftmann@31493
|
137 |
Char NibbleC NibbleD, Char NibbleC NibbleE, Char NibbleC NibbleF,
|
haftmann@31493
|
138 |
Char NibbleD Nibble0, Char NibbleD Nibble1, Char NibbleD Nibble2,
|
haftmann@31493
|
139 |
Char NibbleD Nibble3, Char NibbleD Nibble4, Char NibbleD Nibble5,
|
haftmann@31493
|
140 |
Char NibbleD Nibble6, Char NibbleD Nibble7, Char NibbleD Nibble8,
|
haftmann@31493
|
141 |
Char NibbleD Nibble9, Char NibbleD NibbleA, Char NibbleD NibbleB,
|
haftmann@31493
|
142 |
Char NibbleD NibbleC, Char NibbleD NibbleD, Char NibbleD NibbleE,
|
haftmann@31493
|
143 |
Char NibbleD NibbleF, Char NibbleE Nibble0, Char NibbleE Nibble1,
|
haftmann@31493
|
144 |
Char NibbleE Nibble2, Char NibbleE Nibble3, Char NibbleE Nibble4,
|
haftmann@31493
|
145 |
Char NibbleE Nibble5, Char NibbleE Nibble6, Char NibbleE Nibble7,
|
haftmann@31493
|
146 |
Char NibbleE Nibble8, Char NibbleE Nibble9, Char NibbleE NibbleA,
|
haftmann@31493
|
147 |
Char NibbleE NibbleB, Char NibbleE NibbleC, Char NibbleE NibbleD,
|
haftmann@31493
|
148 |
Char NibbleE NibbleE, Char NibbleE NibbleF, Char NibbleF Nibble0,
|
haftmann@31493
|
149 |
Char NibbleF Nibble1, Char NibbleF Nibble2, Char NibbleF Nibble3,
|
haftmann@31493
|
150 |
Char NibbleF Nibble4, Char NibbleF Nibble5, Char NibbleF Nibble6,
|
haftmann@31493
|
151 |
Char NibbleF Nibble7, Char NibbleF Nibble8, Char NibbleF Nibble9,
|
haftmann@31493
|
152 |
Char NibbleF NibbleA, Char NibbleF NibbleB, Char NibbleF NibbleC,
|
haftmann@31493
|
153 |
Char NibbleF NibbleD, Char NibbleF NibbleE, Char NibbleF NibbleF]"
|
haftmann@31493
|
154 |
|
haftmann@31051
|
155 |
|
bulwahn@39477
|
156 |
subsection {* Strings as dedicated type *}
|
haftmann@31051
|
157 |
|
bulwahn@39477
|
158 |
typedef (open) literal = "UNIV :: string \<Rightarrow> bool"
|
bulwahn@39477
|
159 |
morphisms explode STR ..
|
haftmann@31051
|
160 |
|
bulwahn@39477
|
161 |
instantiation literal :: size
|
bulwahn@39477
|
162 |
begin
|
haftmann@31051
|
163 |
|
bulwahn@39477
|
164 |
definition size_literal :: "literal \<Rightarrow> nat"
|
bulwahn@39477
|
165 |
where
|
bulwahn@39477
|
166 |
[code]: "size_literal (s\<Colon>literal) = 0"
|
haftmann@31051
|
167 |
|
bulwahn@39477
|
168 |
instance ..
|
bulwahn@39477
|
169 |
|
bulwahn@39477
|
170 |
end
|
bulwahn@39477
|
171 |
|
bulwahn@39477
|
172 |
instantiation literal :: equal
|
bulwahn@39477
|
173 |
begin
|
bulwahn@39477
|
174 |
|
bulwahn@39477
|
175 |
definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool"
|
bulwahn@39477
|
176 |
where
|
bulwahn@39477
|
177 |
"equal_literal s1 s2 \<longleftrightarrow> explode s1 = explode s2"
|
bulwahn@39477
|
178 |
|
bulwahn@39477
|
179 |
instance
|
bulwahn@39477
|
180 |
proof
|
bulwahn@39477
|
181 |
qed (auto simp add: equal_literal_def explode_inject)
|
bulwahn@39477
|
182 |
|
bulwahn@39477
|
183 |
end
|
haftmann@31051
|
184 |
|
bulwahn@39501
|
185 |
lemma STR_inject' [simp]: "(STR xs = STR ys) = (xs = ys)"
|
bulwahn@39501
|
186 |
by(simp add: STR_inject)
|
bulwahn@39501
|
187 |
|
bulwahn@39501
|
188 |
|
haftmann@31051
|
189 |
subsection {* Code generator *}
|
haftmann@31051
|
190 |
|
haftmann@31055
|
191 |
use "Tools/string_code.ML"
|
haftmann@31051
|
192 |
|
haftmann@33229
|
193 |
code_reserved SML string
|
haftmann@33229
|
194 |
code_reserved OCaml string
|
haftmann@34886
|
195 |
code_reserved Scala string
|
haftmann@33229
|
196 |
|
haftmann@31205
|
197 |
code_type literal
|
haftmann@31051
|
198 |
(SML "string")
|
haftmann@31051
|
199 |
(OCaml "string")
|
haftmann@31051
|
200 |
(Haskell "String")
|
haftmann@34886
|
201 |
(Scala "String")
|
haftmann@31051
|
202 |
|
haftmann@31051
|
203 |
setup {*
|
haftmann@34886
|
204 |
fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
|
haftmann@31051
|
205 |
*}
|
haftmann@31051
|
206 |
|
haftmann@39086
|
207 |
code_instance literal :: equal
|
haftmann@31051
|
208 |
(Haskell -)
|
haftmann@31051
|
209 |
|
haftmann@39086
|
210 |
code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
|
haftmann@31051
|
211 |
(SML "!((_ : string) = _)")
|
haftmann@31051
|
212 |
(OCaml "!((_ : string) = _)")
|
haftmann@39499
|
213 |
(Haskell infix 4 "==")
|
haftmann@34886
|
214 |
(Scala infixl 5 "==")
|
haftmann@31051
|
215 |
|
haftmann@31051
|
216 |
types_code
|
haftmann@31051
|
217 |
"char" ("string")
|
haftmann@31051
|
218 |
attach (term_of) {*
|
haftmann@31051
|
219 |
val term_of_char = HOLogic.mk_char o ord;
|
haftmann@31051
|
220 |
*}
|
haftmann@31051
|
221 |
attach (test) {*
|
haftmann@31051
|
222 |
fun gen_char i =
|
haftmann@31051
|
223 |
let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
|
haftmann@31051
|
224 |
in (chr j, fn () => HOLogic.mk_char j) end;
|
haftmann@31051
|
225 |
*}
|
haftmann@31051
|
226 |
|
haftmann@31051
|
227 |
setup {*
|
haftmann@31051
|
228 |
let
|
haftmann@31051
|
229 |
|
wenzelm@43292
|
230 |
fun char_codegen thy mode defs dep thyname b t gr =
|
haftmann@31051
|
231 |
let
|
haftmann@31051
|
232 |
val i = HOLogic.dest_char t;
|
wenzelm@43292
|
233 |
val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
|
haftmann@31051
|
234 |
(fastype_of t) gr;
|
haftmann@31051
|
235 |
in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
|
haftmann@31051
|
236 |
end handle TERM _ => NONE;
|
haftmann@31051
|
237 |
|
haftmann@31051
|
238 |
in Codegen.add_codegen "char_codegen" char_codegen end
|
haftmann@31051
|
239 |
*}
|
haftmann@31051
|
240 |
|
wenzelm@36176
|
241 |
hide_type (open) literal
|
haftmann@31205
|
242 |
|
bulwahn@39477
|
243 |
end
|