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