|
1 (* Title: Pure/Syntax/syntax |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 signature SYNTAX = |
|
7 sig |
|
8 (* FIXME include AST0 (?) *) |
|
9 include LEXICON0 |
|
10 include EXTENSION0 |
|
11 include TYPE_EXT0 |
|
12 include SEXTENSION1 |
|
13 include PRINTER0 |
|
14 structure Extension: EXTENSION |
|
15 structure Pretty: PRETTY |
|
16 local open Extension.XGram Extension.XGram.Ast in |
|
17 type syntax |
|
18 val print_gram: syntax -> unit |
|
19 val print_trans: syntax -> unit |
|
20 val print_syntax: syntax -> unit |
|
21 val read_ast: syntax -> string * string -> ast |
|
22 val read: syntax -> typ -> string -> term |
|
23 val pretty_term: syntax -> term -> Pretty.T |
|
24 val pretty_typ: syntax -> typ -> Pretty.T |
|
25 val string_of_term: syntax -> term -> string |
|
26 val string_of_typ: syntax -> typ -> string |
|
27 val type_syn: syntax |
|
28 val extend: syntax * (indexname -> sort) -> string list * string list * sext |
|
29 -> syntax |
|
30 val merge: syntax * syntax -> syntax |
|
31 end |
|
32 end; |
|
33 |
|
34 functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT |
|
35 and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER |
|
36 sharing TypeExt.Extension.XGram = Parser.XGram = Printer.XGram |
|
37 and TypeExt.Extension = SExtension.Extension |
|
38 and Parser.ParseTree.Ast = Parser.XGram.Ast)(*: SYNTAX *) = (* FIXME *) |
|
39 struct |
|
40 |
|
41 structure Extension = TypeExt.Extension; |
|
42 structure XGram = Extension.XGram; |
|
43 structure Lexicon = Parser.ParseTree.Lexicon; |
|
44 open Lexicon Extension TypeExt SExtension Printer XGram XGram.Ast; |
|
45 |
|
46 |
|
47 fun lookup tab a = Symtab.lookup (tab, a); |
|
48 |
|
49 |
|
50 |
|
51 (** datatype syntax **) |
|
52 |
|
53 datatype tables = |
|
54 Tab of { |
|
55 gram: Parser.Gram, |
|
56 lexicon: Lexicon, |
|
57 const_tab: unit Symtab.table, |
|
58 parse_ast_trtab: (ast list -> ast) Symtab.table, |
|
59 parse_preproc: ast -> ast, |
|
60 parse_ruletab: (ast * ast) list Symtab.table, |
|
61 parse_postproc: ast -> ast, |
|
62 parse_trtab: (term list -> term) Symtab.table, |
|
63 print_trtab: (term list -> term) Symtab.table, |
|
64 print_preproc: ast -> ast, |
|
65 print_ruletab: (ast * ast) list Symtab.table, |
|
66 print_postproc: ast -> ast, |
|
67 print_tab: Printer.tab}; |
|
68 |
|
69 datatype gramgraph = |
|
70 EmptyGG | |
|
71 ExtGG of gramgraph ref * (ext * synrules) | |
|
72 MergeGG of gramgraph ref * gramgraph ref; |
|
73 |
|
74 datatype syntax = Syntax of gramgraph ref * tables; |
|
75 |
|
76 |
|
77 |
|
78 (*** compile syntax ***) |
|
79 |
|
80 (* ggr_to_xgram *) |
|
81 |
|
82 fun ggr_to_xgram ggr = |
|
83 let |
|
84 fun flatGG ggr (xg, v) = |
|
85 if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v) |
|
86 and flatGG' (ref EmptyGG) xgv = xgv |
|
87 | flatGG' (ref (ExtGG (ggr, ext))) xgv = |
|
88 let |
|
89 val (xg', v') = flatGG ggr xgv |
|
90 in |
|
91 (Extension.extend xg' ext, v') |
|
92 end |
|
93 | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv = |
|
94 flatGG ggr1 (flatGG ggr2 xgv); |
|
95 in |
|
96 fst (flatGG ggr (Extension.empty, [])) |
|
97 end; |
|
98 |
|
99 |
|
100 (* mk_ruletab *) |
|
101 |
|
102 fun mk_ruletab rules = |
|
103 let |
|
104 fun add_rule (r, tab) = |
|
105 let |
|
106 val a = head_of_rule r |
|
107 in |
|
108 case lookup tab a of |
|
109 None => Symtab.update ((a, [r]), tab) |
|
110 | Some rs => Symtab.update ((a, r :: rs), tab) |
|
111 end; |
|
112 in |
|
113 Symtab.balance (foldr add_rule (rules, Symtab.null)) |
|
114 end; |
|
115 |
|
116 |
|
117 (* make_syntax *) |
|
118 |
|
119 fun make_syntax ggr = |
|
120 let |
|
121 fun mk_const_tab cs = |
|
122 Symtab.balance |
|
123 (Symtab.st_of_alist ((map (fn c => (c, ())) cs), Symtab.null)); |
|
124 |
|
125 fun mk_trtab alst name = |
|
126 Symtab.balance (Symtab.st_of_alist (alst, Symtab.null)) |
|
127 handle Symtab.DUPLICATE s => error ("More than one " ^ name ^ " for " ^ quote s); |
|
128 |
|
129 fun mk_proc (Some f) = f |
|
130 | mk_proc None = I; |
|
131 |
|
132 fun all_strings (opl: string prod list): string list = |
|
133 flat (map (fn Prod (_, syn, _, _) => terminals syn) opl); |
|
134 |
|
135 fun str_to_tok (opl: string prod list, lex: Lexicon): Token prod list = |
|
136 map |
|
137 (fn Prod (t, syn, s, pa) => |
|
138 Prod (t, translate (hd o tokenize lex) syn, s, pa)) |
|
139 opl; |
|
140 |
|
141 fun xgram_to_tables (XGram xgram) = |
|
142 let |
|
143 val {roots, prods, consts, parse_ast_translation, parse_preproc, parse_rules, |
|
144 parse_postproc, parse_translation, print_translation, print_preproc, |
|
145 print_rules, print_postproc, print_ast_translation} = xgram; |
|
146 val lexicon = mk_lexicon (all_strings prods); |
|
147 in |
|
148 Tab { |
|
149 gram = Parser.compile_xgram (roots, str_to_tok (prods, lexicon)), |
|
150 lexicon = lexicon, |
|
151 const_tab = mk_const_tab consts, |
|
152 parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation", |
|
153 parse_preproc = mk_proc parse_preproc, |
|
154 parse_ruletab = mk_ruletab parse_rules, |
|
155 parse_postproc = mk_proc parse_postproc, |
|
156 parse_trtab = mk_trtab parse_translation "parse translation", |
|
157 print_trtab = mk_trtab print_translation "print translation", |
|
158 print_preproc = mk_proc print_preproc, |
|
159 print_ruletab = mk_ruletab print_rules, |
|
160 print_postproc = mk_proc print_postproc, |
|
161 print_tab = mk_print_tab prods |
|
162 (mk_trtab print_ast_translation "print ast translation")} |
|
163 end; |
|
164 in |
|
165 Syntax (ggr, xgram_to_tables (ggr_to_xgram ggr)) |
|
166 end; |
|
167 |
|
168 |
|
169 (* add_synrules *) |
|
170 |
|
171 fun add_synrules (Tab tabs) (SynRules rules) = |
|
172 let |
|
173 val {gram, lexicon, const_tab, parse_ast_trtab, parse_preproc, parse_ruletab, |
|
174 parse_postproc, parse_trtab, print_trtab, print_preproc, print_ruletab, |
|
175 print_postproc, print_tab} = tabs; |
|
176 val {parse_rules, print_rules} = rules; |
|
177 val parse_rs = flat (map snd (Symtab.alist_of parse_ruletab)) @ parse_rules; |
|
178 val print_rs = flat (map snd (Symtab.alist_of print_ruletab)) @ print_rules; |
|
179 in |
|
180 Tab { |
|
181 gram = gram, lexicon = lexicon, const_tab = const_tab, |
|
182 parse_ast_trtab = parse_ast_trtab, |
|
183 parse_preproc = parse_preproc, |
|
184 parse_ruletab = mk_ruletab parse_rs, |
|
185 parse_postproc = parse_postproc, |
|
186 parse_trtab = parse_trtab, |
|
187 print_trtab = print_trtab, |
|
188 print_preproc = print_preproc, |
|
189 print_ruletab = mk_ruletab print_rs, |
|
190 print_postproc = print_postproc, |
|
191 print_tab = print_tab} |
|
192 end; |
|
193 |
|
194 |
|
195 |
|
196 (*** inspect syntax ***) |
|
197 |
|
198 (* print_syntax_old *) (* FIXME remove *) |
|
199 |
|
200 fun print_syntax_old (Syntax (_, Tab {gram, lexicon, ...})) = |
|
201 Parser.print_gram (gram, lexicon); |
|
202 |
|
203 |
|
204 |
|
205 fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr; |
|
206 |
|
207 fun string_of_big_list name prts = |
|
208 Pretty.string_of (Pretty.blk (2, |
|
209 separate Pretty.fbrk (Pretty.str name :: prts))); |
|
210 |
|
211 |
|
212 (* print_gram *) (* FIXME check *) |
|
213 |
|
214 fun prt_gram (XGram {roots, prods, ...}) = |
|
215 let |
|
216 fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1]; |
|
217 |
|
218 fun pretty_xsymbs (Terminal s :: xs) = |
|
219 Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs |
|
220 | pretty_xsymbs (Nonterminal (s, p) :: xs) = |
|
221 (if is_terminal s then Pretty.str s |
|
222 else Pretty.str (s ^ "[" ^ string_of_int p ^ "]")) |
|
223 :: Pretty.brk 1 :: pretty_xsymbs xs |
|
224 | pretty_xsymbs (_ :: xs) = pretty_xsymbs xs |
|
225 | pretty_xsymbs [] = []; |
|
226 |
|
227 fun pretty_const "" = [Pretty.brk 1] |
|
228 | pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1]; |
|
229 |
|
230 fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")]; |
|
231 |
|
232 fun pretty_prod (Prod (name, xsymbs, const, pri)) = |
|
233 Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @ |
|
234 pretty_const const @ pretty_pri pri); |
|
235 in |
|
236 writeln (Pretty.string_of (Pretty.blk (2, |
|
237 separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots))))); |
|
238 writeln (string_of_big_list "prods:" (map pretty_prod prods)) |
|
239 end; |
|
240 |
|
241 |
|
242 val print_gram = prt_gram o xgram_of; |
|
243 |
|
244 |
|
245 (* print_trans *) (* FIXME check *) |
|
246 |
|
247 fun prt_trans (XGram xgram) = |
|
248 let |
|
249 fun string_of_strings name strs = |
|
250 Pretty.string_of (Pretty.blk (2, |
|
251 separate (Pretty.brk 1) (map Pretty.str (name :: map quote strs)))); |
|
252 |
|
253 fun string_of_trs name trs = string_of_strings name (map fst trs); |
|
254 |
|
255 fun string_of_proc name proc = |
|
256 Pretty.string_of (Pretty.blk (2, [Pretty.str name, Pretty.brk 1, |
|
257 Pretty.str (if is_none proc then "None" else "Some fn")])); |
|
258 |
|
259 fun string_of_rules name rules = |
|
260 string_of_big_list name (map pretty_rule rules); |
|
261 |
|
262 |
|
263 val {consts, parse_ast_translation, parse_preproc, parse_rules, |
|
264 parse_postproc, parse_translation, print_translation, print_preproc, |
|
265 print_rules, print_postproc, print_ast_translation, ...} = xgram; |
|
266 in |
|
267 writeln (string_of_strings "consts:" consts); |
|
268 writeln (string_of_trs "parse_ast_translation:" parse_ast_translation); |
|
269 writeln (string_of_proc "parse_preproc:" parse_preproc); |
|
270 writeln (string_of_rules "parse_rules:" parse_rules); |
|
271 writeln (string_of_proc "parse_postproc:" parse_postproc); |
|
272 writeln (string_of_trs "parse_translation:" parse_translation); |
|
273 writeln (string_of_trs "print_translation:" print_translation); |
|
274 writeln (string_of_proc "print_preproc:" print_preproc); |
|
275 writeln (string_of_rules "print_rules:" print_rules); |
|
276 writeln (string_of_proc "print_postproc:" print_postproc); |
|
277 writeln (string_of_trs "print_ast_translation:" print_ast_translation) |
|
278 end; |
|
279 |
|
280 |
|
281 val print_trans = prt_trans o xgram_of; |
|
282 |
|
283 |
|
284 (* print_syntax *) |
|
285 |
|
286 fun print_syntax syn = |
|
287 let |
|
288 val xgram = xgram_of syn; |
|
289 in |
|
290 prt_gram xgram; prt_trans xgram |
|
291 end; |
|
292 |
|
293 |
|
294 |
|
295 (*** parsing and printing ***) |
|
296 |
|
297 (* read_ast *) |
|
298 |
|
299 fun read_ast syn (root, s) = |
|
300 let |
|
301 val Syntax (_, Tab {gram, lexicon, parse_ast_trtab, ...}) = syn; |
|
302 val root = if Parser.parsable (gram, root) then root else error ("Unparsable root " ^ root) (* Extension.logic *); (* FIXME *) |
|
303 fun syn_err toks = |
|
304 error ("Syntax error at\n" ^ space_implode " " (map token_to_string toks)); |
|
305 in |
|
306 Parser.ParseTree.pt_to_ast (lookup parse_ast_trtab) |
|
307 (Parser.parse (gram, root, tokenize lexicon s)) |
|
308 handle Parser.SYNTAX_ERR toks => syn_err toks |
|
309 end; |
|
310 |
|
311 |
|
312 (* norm_ast *) |
|
313 |
|
314 fun norm_ast ruletab ast = |
|
315 let |
|
316 fun get_rules a = |
|
317 (case lookup ruletab a of |
|
318 Some rules => rules |
|
319 | None => []); |
|
320 in |
|
321 normalize (if Symtab.is_null ruletab then None else Some get_rules) ast |
|
322 end; |
|
323 |
|
324 |
|
325 |
|
326 (** read **) |
|
327 |
|
328 fun read (syn as Syntax (_, Tab tabs)) ty s = |
|
329 let |
|
330 val {parse_preproc, parse_ruletab, parse_postproc, parse_trtab, ...} = tabs; |
|
331 val ast = read_ast syn (typ_to_nt ty, s); |
|
332 in |
|
333 ast_to_term (lookup parse_trtab) |
|
334 (parse_postproc (norm_ast parse_ruletab (parse_preproc ast))) |
|
335 end; |
|
336 |
|
337 |
|
338 |
|
339 (** pprint_ast **) |
|
340 |
|
341 val pprint_ast = Pretty.pprint o pretty_ast; |
|
342 |
|
343 |
|
344 |
|
345 (** pretty term, typ **) |
|
346 |
|
347 fun pretty_t t_to_ast pretty_t (syn as Syntax (_, Tab tabs)) t = |
|
348 let |
|
349 val {print_trtab, print_preproc, print_ruletab, print_postproc, print_tab, ...} = tabs; |
|
350 val ast = t_to_ast (lookup print_trtab) t; |
|
351 in |
|
352 pretty_t print_tab |
|
353 (print_postproc (norm_ast print_ruletab (print_preproc ast))) |
|
354 end; |
|
355 |
|
356 val pretty_term = pretty_t term_to_ast pretty_term_ast; |
|
357 |
|
358 val pretty_typ = pretty_t typ_to_ast pretty_typ_ast; |
|
359 |
|
360 fun string_of_term syn t = Pretty.string_of (pretty_term syn t); |
|
361 |
|
362 fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty); |
|
363 |
|
364 |
|
365 |
|
366 (*** build syntax ***) |
|
367 |
|
368 (* type_syn *) |
|
369 |
|
370 val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules)))); |
|
371 |
|
372 |
|
373 (* extend *) (* FIXME check *) |
|
374 |
|
375 fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) = |
|
376 let |
|
377 fun read_typ s = typ_of_term def_sort (read old_syn typeT s); |
|
378 val ext = ext_of_sext roots xconsts read_typ sext; |
|
379 |
|
380 fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2) |
|
381 | right_rule (xpat1 <-| xpat2) = None |
|
382 | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2); |
|
383 |
|
384 fun left_rule (xpat1 |-> xpat2) = None |
|
385 | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1) |
|
386 | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1); |
|
387 |
|
388 val (tmp_syn as Syntax (_, tmp_tabs)) = |
|
389 make_syntax (ref (ExtGG (ggr, (ext, empty_synrules)))); |
|
390 val Syntax (_, Tab {const_tab, ...}) = tmp_syn; |
|
391 |
|
392 fun constantify (ast as (Constant _)) = ast |
|
393 | constantify (ast as (Variable x)) = |
|
394 if is_some (lookup const_tab x) then Constant x else ast |
|
395 | constantify (Appl asts) = Appl (map constantify asts); |
|
396 |
|
397 fun read_pat (r_s as (root, s)) = |
|
398 constantify ((read_ast tmp_syn r_s) |
|
399 handle ERROR => error ("The error above occurred in " ^ quote s)); |
|
400 |
|
401 fun read_rule (xrule as ((_, lhs_src), (_, rhs_src))) = |
|
402 let |
|
403 val rule as (lhs, rhs) = (pairself read_pat) xrule; |
|
404 in |
|
405 case rule_error rule of |
|
406 Some msg => |
|
407 error ("Error in syntax translation rule: " ^ msg ^ |
|
408 "\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^ |
|
409 "\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs) |
|
410 | None => rule |
|
411 end; |
|
412 |
|
413 val xrules = xrules_of sext; |
|
414 val new_rules = |
|
415 SynRules { |
|
416 parse_rules = map read_rule (mapfilter right_rule xrules), |
|
417 print_rules = map read_rule (mapfilter left_rule xrules)}; |
|
418 in |
|
419 Syntax (ref (ExtGG (ggr, (ext, new_rules))), add_synrules tmp_tabs new_rules) |
|
420 end; |
|
421 |
|
422 |
|
423 (* merge *) |
|
424 |
|
425 fun merge (Syntax (ggr1, _), Syntax (ggr2, _)) = |
|
426 make_syntax (ref (MergeGG (ggr1, ggr2))); |
|
427 |
|
428 |
|
429 end; |
|
430 |