author | clasohm |
Tue, 16 Nov 1993 14:23:19 +0100 | |
changeset 123 | 0a2f744e008a |
parent 81 | 4cc5a34292a9 |
child 201 | 9e41c6cec27c |
permissions | -rw-r--r-- |
20 | 1 |
(* Title: Pure/Thy/syntax.ML |
0 | 2 |
ID: $Id$ |
20 | 3 |
Author: Sonia Mahjoub and Tobias Nipkow and Markus Wenzel, TU Muenchen |
0 | 4 |
|
5 |
Definition of theory syntax together with translation to ML code. |
|
6 |
*) |
|
7 |
||
8 |
signature THYSYN = |
|
9 |
sig |
|
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset
|
10 |
datatype basetype = Thy of string |
81 | 11 |
| File of string |
12 |
||
0 | 13 |
val read: string list -> string |
14 |
end; |
|
15 |
||
16 |
||
17 |
||
18 |
functor ThySynFUN (Parse: PARSE): THYSYN = |
|
19 |
struct |
|
20 |
||
21 |
||
22 |
(*-------------- OBJECT TO STRING TRANSLATION ---------------*) |
|
23 |
||
24 |
fun parent s = "(" ^ s ^ ")"; |
|
25 |
||
20 | 26 |
fun pair(a, b) = parent(a ^ ", " ^ b); |
0 | 27 |
|
20 | 28 |
fun pair_quote(a, b) = pair(quote a, quote b); |
0 | 29 |
|
20 | 30 |
fun pair_quote2(a, b) = pair(a, quote b); |
0 | 31 |
|
32 |
fun bracket s = "[" ^ s ^ "]"; |
|
33 |
||
34 |
val comma = space_implode ", "; |
|
35 |
||
36 |
val bracket_comma = bracket o comma; |
|
37 |
||
38 |
val big_bracket_comma = bracket o space_implode ",\n"; |
|
39 |
||
40 |
fun big_bracket_comma_ind ind strs = bracket (space_implode (",\n" ^ ind) strs); |
|
41 |
||
20 | 42 |
val bracket_comma_quote = bracket_comma o (map quote); |
0 | 43 |
|
44 |
||
45 |
(*------------------- ABSTRACT SYNTAX FUNCTIONS ---------------------*) |
|
46 |
||
47 |
datatype mixfix = Mixfix of string * string * string |
|
48 |
| Delimfix of string |
|
49 |
| Infixl of string |
|
50 |
| Infixr of string |
|
51 |
| Binder of string * string |
|
52 |
| TInfixl of string |
|
53 |
| TInfixr of string; |
|
54 |
||
55 |
||
56 |
datatype pfix_or_mfix = Pref of string | Mixf of string; |
|
57 |
||
58 |
fun pm_proj(Pref s) = s |
|
59 |
| pm_proj(Mixf s) = s; |
|
60 |
||
61 |
fun split_decls l = |
|
20 | 62 |
let val (p, m) = partition (fn Pref _ => true | _ => false) l; |
0 | 63 |
in (big_bracket_comma_ind " " (map pm_proj p), map pm_proj m) end; |
64 |
||
65 |
fun delim_mix (s, None) = Delimfix(s) |
|
20 | 66 |
| delim_mix (s, Some(l, n)) = Mixfix(s, l, n); |
0 | 67 |
|
20 | 68 |
fun mixfix (sy, c, ty, l, n) = "Mixfix(" ^ comma[quote sy, c, ty, l, n] ^ ")"; |
0 | 69 |
|
20 | 70 |
fun infixrl(ty, c, n) = parent(comma[ty, c, n]); |
0 | 71 |
|
20 | 72 |
fun binder(sy, c, ty, n) = "Binder(" ^ comma[quote sy, c, ty, "0", n] ^ ")"; |
0 | 73 |
|
20 | 74 |
fun delimfix (sy, c, ty) = "Delimfix(" ^ comma[quote sy, c, ty] ^ ")"; |
0 | 75 |
|
76 |
fun tinfixrl (ty, n) = "(" ^ comma[ty, ty, n] ^ ")"; |
|
77 |
||
20 | 78 |
fun mk_mfix((c, ty), mfix) = |
79 |
let val cs = quote c and tys = quote ty |
|
0 | 80 |
in case mfix of |
81 |
Mixfix(sy, l, n) => mixfix (sy, tys, cs, l, n) |
|
82 |
| Infixr(n) => "Infixr" ^ infixrl(cs, tys, n) |
|
83 |
| Infixl(n) => "Infixl" ^ infixrl(cs, tys, n) |
|
20 | 84 |
| Binder(sy, n) => binder(sy, tys, cs, n) |
0 | 85 |
| TInfixl(n) => "TInfixl" ^ tinfixrl(cs, n) |
86 |
| TInfixr(n) => "TInfixr" ^ tinfixrl(cs, n) |
|
87 |
| Delimfix(sy) => delimfix(sy, tys, cs) |
|
88 |
end; |
|
89 |
||
90 |
||
20 | 91 |
fun mk_mixfix((cs, ty), None) = |
92 |
[Pref(pair(bracket_comma_quote cs, quote ty))] |
|
93 |
| mk_mixfix((c::cs, ty), Some(mfix)) = |
|
94 |
Mixf(mk_mfix((c, ty), mfix)) :: mk_mixfix((cs, ty), Some(mfix)) |
|
95 |
| mk_mixfix(([], _), _) = []; |
|
0 | 96 |
|
20 | 97 |
fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_quote ts, n))] |
0 | 98 |
| mk_type_decl((t::ts, n), Some(tinfix)) = |
20 | 99 |
[Pref(pair(bracket(quote t), n)), Mixf(mk_mfix((t, n), tinfix))] @ |
0 | 100 |
mk_type_decl((ts, n), Some(tinfix)) |
101 |
| mk_type_decl(([], n), Some(tinfix)) = []; |
|
102 |
||
103 |
||
104 |
fun mk_extension (((((((cl, def), (ty, tinfix)), ar), (co, mfix)), tr), ax), ml) = |
|
105 |
((cl, def, ty, ar, co, ax), big_bracket_comma_ind " " tinfix, |
|
106 |
big_bracket_comma_ind " " mfix, big_bracket_comma_ind " " tr, ml); |
|
107 |
||
20 | 108 |
fun add_val((id, _), s) = "val " ^ id ^ " = get_axiom thy " ^ quote id ^ "\n" ^ s; |
0 | 109 |
|
110 |
fun mk_rules ps = |
|
111 |
let |
|
20 | 112 |
val axs = big_bracket_comma_ind " " (map pair_quote ps); |
0 | 113 |
val vals = foldr add_val (ps, "") |
114 |
in |
|
20 | 115 |
axs ^ "\n\n" ^ vals |
0 | 116 |
end; |
117 |
||
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset
|
118 |
fun mk_struct (id, s) = "structure " ^ id ^ " =\nstruct\n" ^ s ^ "\nend;\n"; |
0 | 119 |
|
120 |
||
121 |
fun mk_sext mfix trans = |
|
122 |
"Some (NewSext {\n\ |
|
123 |
\ mixfix =\n " ^ mfix ^ ",\n\ |
|
124 |
\ xrules =\n " ^ trans ^ ",\n\ |
|
125 |
\ parse_ast_translation = parse_ast_translation,\n\ |
|
126 |
\ parse_translation = parse_translation,\n\ |
|
127 |
\ print_translation = print_translation,\n\ |
|
128 |
\ print_ast_translation = print_ast_translation})"; |
|
129 |
||
130 |
fun mk_simple_sext mfix = |
|
131 |
"Some (Syntax.simple_sext\n " ^ mfix ^ ")"; |
|
132 |
||
133 |
fun mk_ext ((cl, def, ty, ar, co, ax), sext) = |
|
134 |
" (" ^ space_implode ",\n " [cl, def, ty, ar, co, sext] ^ ")\n " ^ ax ^ "\n"; |
|
135 |
||
136 |
fun mk_ext_thy (base, name, ext, sext) = |
|
20 | 137 |
"extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext); |
0 | 138 |
|
139 |
val preamble = |
|
140 |
"\nlocal\n\ |
|
141 |
\ val parse_ast_translation = []\n\ |
|
142 |
\ val parse_translation = []\n\ |
|
143 |
\ val print_translation = []\n\ |
|
144 |
\ val print_ast_translation = []\n\ |
|
145 |
\in\n\n\ |
|
146 |
\(**** begin of user section ****)\n"; |
|
147 |
||
148 |
val postamble = "\n(**** end of user section ****)\n"; |
|
149 |
||
150 |
fun mk_structure ((name, base), Some (ext, tinfix, mfix, trans, ml)) = |
|
151 |
let |
|
152 |
val noext = ("[]", "[]", "[]", "[]", "[]", "[]"); |
|
153 |
val basethy = |
|
74 | 154 |
if tinfix = "[]" then base ^ (quote name) |
155 |
else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix); |
|
0 | 156 |
val sext = |
157 |
if mfix = "[]" andalso trans = "[]" andalso ml = "" then "None" |
|
158 |
else mk_sext mfix trans; |
|
74 | 159 |
val thy = "val thy = " ^ mk_ext_thy (basethy, name, ext, sext); |
0 | 160 |
in |
161 |
mk_struct (name, preamble ^ ml ^ postamble ^ thy ^ "\nend") |
|
162 |
end |
|
74 | 163 |
| mk_structure ((name, base), None) = |
164 |
mk_struct (name, "\nval thy = " ^ base ^ (quote name)); |
|
0 | 165 |
|
123
0a2f744e008a
moved call of store_theory to end of use t.thy; use t.ML;
clasohm
parents:
81
diff
changeset
|
166 |
datatype basetype = Thy of string |
81 | 167 |
| File of string; |
168 |
||
74 | 169 |
fun merge thys = |
81 | 170 |
let fun make_list (Thy t :: ts) = |
171 |
("Thy \"" ^ t ^ "\"") :: make_list ts |
|
172 |
| make_list (File t :: ts) = |
|
173 |
("File \"" ^ t ^ "\"") :: make_list ts |
|
174 |
| make_list [] = [] |
|
175 |
in "base_on " ^ (bracket (space_implode "," (make_list thys))) ^ " " end; |
|
0 | 176 |
|
177 |
||
178 |
||
179 |
(*------------------------ PARSERS -------------------------*) |
|
180 |
||
181 |
||
182 |
open Parse |
|
183 |
||
184 |
(*------------------- VARIOUS PARSERS ----------------------*) |
|
185 |
||
20 | 186 |
val emptyl = empty >> K "[]"; |
0 | 187 |
|
20 | 188 |
val ids = list_of1 id >> bracket_comma_quote; |
0 | 189 |
(* -> "[id1, id2, ..., idn]" *) |
190 |
||
191 |
val stgorids = list_of1 (stg || id); |
|
192 |
||
20 | 193 |
val sort = id >> (bracket o quote) |
0 | 194 |
|| "{" $$-- (ids || emptyl) --$$ "}"; |
195 |
(* -> "[id]" |
|
20 | 196 |
-> "[id1, ..., idn]" *) |
0 | 197 |
|
198 |
val infxl = "infixl" $$-- !! nat |
|
199 |
and infxr = "infixr" $$-- !! nat |
|
200 |
||
201 |
||
202 |
(*------------------- CLASSES PARSER ----------------------*) |
|
203 |
||
204 |
||
205 |
||
206 |
||
20 | 207 |
val class = (id >> quote) -- ( "<" $$-- (!! ids) || emptyl) >> pair; |
0 | 208 |
|
209 |
(* -> "(id, [id1, ..., idn])" |
|
210 |
|| |
|
211 |
-> "(id, [])" *) |
|
212 |
||
213 |
||
214 |
val classes = "classes" $$-- !!(repeat1 class) >> bracket_comma |
|
215 |
|| emptyl; |
|
216 |
||
217 |
||
20 | 218 |
(* "[(id, [..]), ..., (id, [...])]" *) |
0 | 219 |
|
220 |
||
221 |
||
222 |
(*------------------- DEFAULT PARSER ---------------------*) |
|
223 |
||
224 |
||
225 |
val default = "default" $$-- !!sort |
|
226 |
|| emptyl; |
|
227 |
||
228 |
(* -> "[]" |
|
229 |
-> "[id]" |
|
20 | 230 |
-> "[id1, ..., idn]" *) |
0 | 231 |
|
232 |
||
233 |
(*-------------------- TYPES PARSER ----------------------*) |
|
234 |
||
235 |
||
236 |
val type_decl = stgorids -- nat; |
|
237 |
||
238 |
val tyinfix = infxl >> (Some o TInfixl) |
|
239 |
|| infxr >> (Some o TInfixr); |
|
240 |
||
241 |
val type_infix = "(" $$-- !! (tyinfix --$$ ")") |
|
242 |
|| empty >> K None; |
|
243 |
||
244 |
val types = "types" $$-- |
|
245 |
!! (repeat1 (type_decl -- type_infix >> mk_type_decl)) |
|
246 |
>> (split_decls o flat) |
|
247 |
|| empty >> (K ("[]", [])); |
|
248 |
||
249 |
(* ==> ("[(id, nat), ... ]", [strg, ...]) *) |
|
250 |
||
251 |
||
252 |
||
253 |
(*-------------------- ARITIES PARSER ----------------------*) |
|
254 |
||
255 |
||
256 |
val sorts = list_of sort >> bracket_comma; |
|
257 |
||
258 |
(* -> "[[id1, ...], ..., [id, ...]]" *) |
|
259 |
||
260 |
||
20 | 261 |
val arity = id >> (fn s => pair("[]", quote s)) |
262 |
|| "(" $$-- sorts --$$")" -- id >> (fn (l, s) => pair(l, quote s)); |
|
0 | 263 |
|
20 | 264 |
(* -> "([], id)" |
265 |
-> "([[id, ..], ..., [id, ..]], id)" *) |
|
0 | 266 |
|
20 | 267 |
val tys = stgorids >> bracket_comma_quote; |
0 | 268 |
|
269 |
val arities = "arities" $$-- !! (repeat1 (tys --$$ "::" -- arity >> pair)) |
|
270 |
>> bracket_comma |
|
271 |
|| emptyl; |
|
272 |
||
20 | 273 |
(* -> "[([id, ..], ([[id, ...], ...], id))]" *) |
0 | 274 |
|
275 |
||
276 |
(*--------------------- CONSTS PARSER ---------------------*) |
|
277 |
||
278 |
val natlist = "[" $$-- !!(list_of nat --$$ "]") >> bracket_comma |
|
20 | 279 |
|| empty >> K "[]"; |
0 | 280 |
|
281 |
||
282 |
(* "[nat, ...]" || "[]" *) |
|
283 |
||
284 |
||
285 |
val prio_opt = natlist -- nat >> Some |
|
286 |
|| empty >> K None; |
|
287 |
||
288 |
val mfix = stg -- !! prio_opt >> delim_mix |
|
289 |
|| infxl >> Infixl |
|
290 |
|| infxr >> Infixr |
|
291 |
|| "binder" $$-- !!(stg -- nat) >> Binder |
|
292 |
||
293 |
val const_decl = stgorids -- !! ("::" $$-- stg); |
|
294 |
||
295 |
(*("[exid, ...]", stg) *) |
|
296 |
||
297 |
||
298 |
val mixfix = "(" $$-- !! (mfix --$$ ")") >> Some |
|
299 |
|| empty >> K None; |
|
300 |
||
301 |
(* (s, e, l, n) *) |
|
302 |
||
303 |
||
304 |
val consts = "consts" $$-- |
|
305 |
!! (repeat1 (const_decl -- mixfix >> mk_mixfix)) |
|
306 |
>> (split_decls o flat) |
|
20 | 307 |
|| empty >> K ("[]", []); |
0 | 308 |
|
309 |
(* ("[([exid, ...], stg), ....]", [strg, ..]) *) |
|
310 |
||
311 |
||
312 |
(*---------------- TRANSLATIONS PARSER --------------------*) |
|
313 |
||
20 | 314 |
val xpat = "(" $$-- id --$$ ")" -- stg >> pair_quote |
315 |
|| stg >> (fn s => pair_quote ("logic", s)); |
|
0 | 316 |
|
317 |
val arrow = $$ "=>" >> K " |-> " |
|
318 |
|| $$ "<=" >> K " <-| " |
|
319 |
|| $$ "==" >> K " <-> "; |
|
320 |
||
321 |
val xrule = xpat -- !! (arrow -- xpat) >> (fn (xp1, (a, xp2)) => xp1 ^ a ^ xp2); |
|
322 |
||
323 |
val translations = "translations" $$-- !! (repeat1 xrule) |
|
324 |
|| empty; |
|
325 |
||
326 |
||
327 |
(*------------------- RULES PARSER -----------------------*) |
|
328 |
||
329 |
val rules = "rules" $$-- !! (repeat1 (id -- !! stg) >> mk_rules) |
|
330 |
|| emptyl; |
|
331 |
||
332 |
(* "[(id, stg), ...]" *) |
|
333 |
||
81 | 334 |
(*----------------------- BASE PARSER -------------------------*) |
335 |
||
336 |
||
337 |
fun base toks = |
|
338 |
let fun make_thy (b, toks) = (Thy b, toks); |
|
339 |
||
340 |
fun make_file (b, toks) = (File b, toks); |
|
341 |
||
342 |
val (b, toks) = make_thy (id toks) |
|
343 |
handle _ => make_file (stg toks) |
|
344 |
in (b, toks) end; |
|
0 | 345 |
|
346 |
||
347 |
(*----------------------- ML_TEXT -------------------------*) |
|
348 |
||
20 | 349 |
val mltxt = txt || empty >> K ""; |
0 | 350 |
|
351 |
||
352 |
(*---------------------------------------------------------*) |
|
353 |
||
354 |
val extension = "+" $$-- !! (classes -- default -- types -- arities |
|
355 |
-- consts -- translations -- rules --$$ "end" -- mltxt) |
|
356 |
>> (Some o mk_extension) |
|
357 |
|| empty >> K None; |
|
358 |
||
359 |
||
81 | 360 |
val bases = base -- repeat("+" $$-- base) >> op:: ; |
0 | 361 |
|
362 |
val theoryDef = !!(id --$$ "=" -- (bases >> merge) -- extension) |
|
363 |
>> mk_structure; |
|
364 |
||
365 |
val read = reader theoryDef |
|
366 |
||
367 |
end; |
|
368 |