18
|
1 |
(* Title: Pure/Syntax/syntax.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
18
|
4 |
|
|
5 |
Root of Isabelle's syntax module.
|
|
6 |
|
|
7 |
TODO:
|
167
|
8 |
fix empty_tables, extend_tables, mk_tables (requires empty_gram, extend_gram)
|
|
9 |
fix extend (requires extend_tables)
|
0
|
10 |
*)
|
|
11 |
|
|
12 |
signature SYNTAX =
|
|
13 |
sig
|
18
|
14 |
include AST0
|
0
|
15 |
include LEXICON0
|
|
16 |
include EXTENSION0
|
|
17 |
include TYPE_EXT0
|
|
18 |
include SEXTENSION1
|
|
19 |
include PRINTER0
|
18
|
20 |
type syntax
|
|
21 |
val type_syn: syntax
|
144
|
22 |
val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax
|
167
|
23 |
val merge: string list -> syntax -> syntax -> syntax
|
18
|
24 |
val print_gram: syntax -> unit
|
|
25 |
val print_trans: syntax -> unit
|
|
26 |
val print_syntax: syntax -> unit
|
|
27 |
val test_read: syntax -> string -> string -> unit
|
|
28 |
val read: syntax -> typ -> string -> term
|
144
|
29 |
val read_typ: syntax -> (indexname -> sort) -> string -> typ
|
18
|
30 |
val pretty_term: syntax -> term -> Pretty.T
|
|
31 |
val pretty_typ: syntax -> typ -> Pretty.T
|
|
32 |
val string_of_term: syntax -> term -> string
|
|
33 |
val string_of_typ: syntax -> typ -> string
|
0
|
34 |
end;
|
|
35 |
|
|
36 |
functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
|
|
37 |
and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER
|
18
|
38 |
sharing TypeExt.Extension = SExtension.Extension
|
|
39 |
and Parser.XGram = TypeExt.Extension.XGram = Printer.XGram
|
47
|
40 |
and Parser.XGram.Ast = Parser.ParseTree.Ast): SYNTAX =
|
0
|
41 |
struct
|
|
42 |
|
|
43 |
structure Extension = TypeExt.Extension;
|
|
44 |
structure XGram = Extension.XGram;
|
|
45 |
structure Lexicon = Parser.ParseTree.Lexicon;
|
18
|
46 |
open Lexicon Parser Parser.ParseTree Extension TypeExt SExtension Printer
|
|
47 |
XGram XGram.Ast;
|
0
|
48 |
|
|
49 |
|
|
50 |
fun lookup tab a = Symtab.lookup (tab, a);
|
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
(** datatype syntax **)
|
|
55 |
|
|
56 |
datatype tables =
|
18
|
57 |
Tabs of {
|
|
58 |
lexicon: lexicon,
|
|
59 |
roots: string list,
|
|
60 |
gram: gram,
|
|
61 |
consts: string list,
|
0
|
62 |
parse_ast_trtab: (ast list -> ast) Symtab.table,
|
|
63 |
parse_ruletab: (ast * ast) list Symtab.table,
|
|
64 |
parse_trtab: (term list -> term) Symtab.table,
|
|
65 |
print_trtab: (term list -> term) Symtab.table,
|
|
66 |
print_ruletab: (ast * ast) list Symtab.table,
|
18
|
67 |
prtab: prtab};
|
0
|
68 |
|
|
69 |
datatype gramgraph =
|
|
70 |
EmptyGG |
|
167
|
71 |
ExtGG of gramgraph ref * ext |
|
0
|
72 |
MergeGG of gramgraph ref * gramgraph ref;
|
|
73 |
|
|
74 |
datatype syntax = Syntax of gramgraph ref * tables;
|
|
75 |
|
|
76 |
|
|
77 |
|
|
78 |
(*** compile syntax ***)
|
|
79 |
|
18
|
80 |
(* translation funs *)
|
|
81 |
|
|
82 |
fun extend_trtab tab trfuns name =
|
|
83 |
Symtab.balance (Symtab.st_of_alist (trfuns, tab)) handle Symtab.DUPLICATE s
|
|
84 |
=> error ("More than one " ^ name ^ " for " ^ quote s);
|
|
85 |
|
|
86 |
val mk_trtab = extend_trtab Symtab.null;
|
|
87 |
|
|
88 |
|
|
89 |
(* translation rules *)
|
|
90 |
|
|
91 |
fun mk_ruletab rules =
|
|
92 |
let
|
|
93 |
fun add_rule (r, tab) =
|
|
94 |
let val a = head_of_rule r;
|
|
95 |
in
|
|
96 |
(case lookup tab a of
|
|
97 |
None => Symtab.update ((a, [r]), tab)
|
|
98 |
| Some rs => Symtab.update ((a, r :: rs), tab))
|
|
99 |
end;
|
|
100 |
in
|
|
101 |
Symtab.balance (foldr add_rule (rules, Symtab.null))
|
|
102 |
end;
|
|
103 |
|
|
104 |
fun extend_ruletab tab rules =
|
|
105 |
mk_ruletab (flat (map #2 (Symtab.alist_of tab)) @ rules);
|
|
106 |
|
|
107 |
|
167
|
108 |
|
|
109 |
(** tables **)
|
|
110 |
|
|
111 |
(* empty_tables *)
|
|
112 |
|
171
|
113 |
(*(* FIXME *)
|
167
|
114 |
val empty_tables =
|
|
115 |
Tabs {
|
|
116 |
lexicon = empty_lexicon,
|
|
117 |
roots = [],
|
171
|
118 |
gram = empty_gram,
|
167
|
119 |
consts = [],
|
|
120 |
parse_ast_trtab = Symtab.null,
|
|
121 |
parse_ruletab = Symtab.null,
|
|
122 |
parse_trtab = Symtab.null,
|
|
123 |
print_trtab = Symtab.null,
|
|
124 |
print_ruletab = Symtab.null,
|
|
125 |
prtab = empty_prtab};
|
171
|
126 |
*)
|
167
|
127 |
|
|
128 |
|
|
129 |
(* extend_tables *)
|
|
130 |
|
|
131 |
fun extend_tables (Tabs tabs) (XGram xgram) =
|
|
132 |
let
|
|
133 |
val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
|
|
134 |
parse_ruletab, parse_trtab, print_trtab, print_ruletab, prtab} = tabs;
|
|
135 |
val {roots = roots2, prods, consts = consts2, parse_ast_translation,
|
|
136 |
parse_rules, parse_translation, print_translation, print_rules,
|
|
137 |
print_ast_translation} = xgram;
|
|
138 |
in
|
|
139 |
(* FIXME *)
|
|
140 |
if not (null prods) then
|
|
141 |
error "extend_tables: called with non-empty prods"
|
|
142 |
else
|
|
143 |
|
|
144 |
Tabs {
|
|
145 |
lexicon = extend_lexicon lexicon (literals_of prods),
|
|
146 |
roots = roots2 union roots1,
|
|
147 |
(* gram = extend_gram gram roots2 prods, *) (* FIXME *)
|
|
148 |
gram = gram, (* FIXME *)
|
|
149 |
consts = consts2 union consts1,
|
|
150 |
parse_ast_trtab =
|
|
151 |
extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
|
|
152 |
parse_ruletab = extend_ruletab parse_ruletab parse_rules,
|
|
153 |
parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
|
|
154 |
print_trtab = extend_trtab print_trtab print_translation "print translation",
|
|
155 |
print_ruletab = extend_ruletab print_ruletab print_rules,
|
|
156 |
prtab = extend_prtab prtab prods print_ast_translation}
|
|
157 |
end;
|
|
158 |
|
|
159 |
|
18
|
160 |
(* mk_tables *)
|
|
161 |
|
171
|
162 |
(* FIXME *)
|
168
|
163 |
(* val mk_tables = extend_tables empty_tables; *)
|
167
|
164 |
|
|
165 |
(* FIXME *)
|
18
|
166 |
fun mk_tables (XGram xgram) =
|
|
167 |
let
|
|
168 |
val {roots, prods, consts, parse_ast_translation, parse_rules,
|
|
169 |
parse_translation, print_translation, print_rules,
|
|
170 |
print_ast_translation} = xgram;
|
|
171 |
in
|
|
172 |
Tabs {
|
|
173 |
lexicon = mk_lexicon (literals_of prods),
|
|
174 |
roots = roots,
|
|
175 |
gram = mk_gram roots prods,
|
|
176 |
consts = consts,
|
|
177 |
parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
|
|
178 |
parse_ruletab = mk_ruletab parse_rules,
|
|
179 |
parse_trtab = mk_trtab parse_translation "parse translation",
|
|
180 |
print_trtab = mk_trtab print_translation "print translation",
|
|
181 |
print_ruletab = mk_ruletab print_rules,
|
|
182 |
prtab = mk_prtab prods print_ast_translation}
|
|
183 |
end;
|
|
184 |
|
|
185 |
|
0
|
186 |
(* ggr_to_xgram *)
|
|
187 |
|
|
188 |
fun ggr_to_xgram ggr =
|
|
189 |
let
|
|
190 |
fun flatGG ggr (xg, v) =
|
|
191 |
if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v)
|
|
192 |
and flatGG' (ref EmptyGG) xgv = xgv
|
|
193 |
| flatGG' (ref (ExtGG (ggr, ext))) xgv =
|
|
194 |
let
|
18
|
195 |
val (xg', v') = flatGG ggr xgv;
|
0
|
196 |
in
|
18
|
197 |
(extend_xgram xg' ext, v')
|
0
|
198 |
end
|
|
199 |
| flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
|
|
200 |
flatGG ggr1 (flatGG ggr2 xgv);
|
|
201 |
in
|
18
|
202 |
#1 (flatGG ggr (empty_xgram, []))
|
0
|
203 |
end;
|
|
204 |
|
|
205 |
|
167
|
206 |
(* mk_syntax *)
|
0
|
207 |
|
167
|
208 |
fun mk_syntax ggr = Syntax (ggr, mk_tables (ggr_to_xgram ggr));
|
0
|
209 |
|
|
210 |
|
|
211 |
|
|
212 |
(*** inspect syntax ***)
|
|
213 |
|
|
214 |
fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
|
|
215 |
|
|
216 |
fun string_of_big_list name prts =
|
|
217 |
Pretty.string_of (Pretty.blk (2,
|
|
218 |
separate Pretty.fbrk (Pretty.str name :: prts)));
|
|
219 |
|
18
|
220 |
fun string_of_strings name strs =
|
|
221 |
Pretty.string_of (Pretty.blk (2,
|
|
222 |
separate (Pretty.brk 1)
|
|
223 |
(map Pretty.str (name :: map quote (sort_strings strs)))));
|
0
|
224 |
|
18
|
225 |
|
|
226 |
(* print_gram *)
|
0
|
227 |
|
|
228 |
fun prt_gram (XGram {roots, prods, ...}) =
|
|
229 |
let
|
|
230 |
fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1];
|
|
231 |
|
|
232 |
fun pretty_xsymbs (Terminal s :: xs) =
|
|
233 |
Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs
|
|
234 |
| pretty_xsymbs (Nonterminal (s, p) :: xs) =
|
|
235 |
(if is_terminal s then Pretty.str s
|
|
236 |
else Pretty.str (s ^ "[" ^ string_of_int p ^ "]"))
|
|
237 |
:: Pretty.brk 1 :: pretty_xsymbs xs
|
|
238 |
| pretty_xsymbs (_ :: xs) = pretty_xsymbs xs
|
|
239 |
| pretty_xsymbs [] = [];
|
|
240 |
|
|
241 |
fun pretty_const "" = [Pretty.brk 1]
|
|
242 |
| pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1];
|
|
243 |
|
|
244 |
fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
|
|
245 |
|
|
246 |
fun pretty_prod (Prod (name, xsymbs, const, pri)) =
|
|
247 |
Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
|
|
248 |
pretty_const const @ pretty_pri pri);
|
|
249 |
in
|
18
|
250 |
writeln (string_of_strings "lexicon:" (literals_of prods));
|
0
|
251 |
writeln (Pretty.string_of (Pretty.blk (2,
|
|
252 |
separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
|
|
253 |
writeln (string_of_big_list "prods:" (map pretty_prod prods))
|
|
254 |
end;
|
|
255 |
|
|
256 |
val print_gram = prt_gram o xgram_of;
|
|
257 |
|
|
258 |
|
18
|
259 |
(* print_trans *)
|
0
|
260 |
|
|
261 |
fun prt_trans (XGram xgram) =
|
|
262 |
let
|
|
263 |
fun string_of_trs name trs = string_of_strings name (map fst trs);
|
|
264 |
|
|
265 |
fun string_of_rules name rules =
|
|
266 |
string_of_big_list name (map pretty_rule rules);
|
|
267 |
|
18
|
268 |
val {consts, parse_ast_translation, parse_rules, parse_translation,
|
|
269 |
print_translation, print_rules, print_ast_translation, ...} = xgram;
|
0
|
270 |
in
|
|
271 |
writeln (string_of_strings "consts:" consts);
|
|
272 |
writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
|
|
273 |
writeln (string_of_rules "parse_rules:" parse_rules);
|
|
274 |
writeln (string_of_trs "parse_translation:" parse_translation);
|
|
275 |
writeln (string_of_trs "print_translation:" print_translation);
|
|
276 |
writeln (string_of_rules "print_rules:" print_rules);
|
|
277 |
writeln (string_of_trs "print_ast_translation:" print_ast_translation)
|
|
278 |
end;
|
|
279 |
|
|
280 |
val print_trans = prt_trans o xgram_of;
|
|
281 |
|
|
282 |
|
|
283 |
(* print_syntax *)
|
|
284 |
|
|
285 |
fun print_syntax syn =
|
|
286 |
let
|
|
287 |
val xgram = xgram_of syn;
|
|
288 |
in
|
|
289 |
prt_gram xgram; prt_trans xgram
|
|
290 |
end;
|
|
291 |
|
|
292 |
|
|
293 |
|
|
294 |
(*** parsing and printing ***)
|
|
295 |
|
18
|
296 |
(* mk_get_rules *)
|
0
|
297 |
|
18
|
298 |
fun mk_get_rules ruletab =
|
0
|
299 |
let
|
|
300 |
fun get_rules a =
|
|
301 |
(case lookup ruletab a of
|
|
302 |
Some rules => rules
|
|
303 |
| None => []);
|
|
304 |
in
|
18
|
305 |
if Symtab.is_null ruletab then None else Some get_rules
|
|
306 |
end;
|
|
307 |
|
|
308 |
|
|
309 |
(* read_ast *)
|
|
310 |
|
|
311 |
fun read_ast (Syntax (_, tabs)) xids root str =
|
|
312 |
let
|
|
313 |
val Tabs {lexicon, gram, parse_ast_trtab, ...} = tabs;
|
|
314 |
in
|
|
315 |
pt_to_ast (lookup parse_ast_trtab)
|
|
316 |
(parse gram root (tokenize lexicon xids str))
|
0
|
317 |
end;
|
|
318 |
|
|
319 |
|
|
320 |
|
18
|
321 |
(** test_read **)
|
|
322 |
|
|
323 |
fun test_read (Syntax (_, tabs)) root str =
|
|
324 |
let
|
|
325 |
val Tabs {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
|
|
326 |
|
|
327 |
val toks = tokenize lexicon false str;
|
|
328 |
val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
|
|
329 |
|
|
330 |
val pt = parse gram root toks;
|
|
331 |
val raw_ast = pt_to_ast (K None) pt;
|
|
332 |
val _ = writeln ("raw: " ^ str_of_ast raw_ast);
|
|
333 |
|
|
334 |
val pre_ast = pt_to_ast (lookup parse_ast_trtab) pt;
|
|
335 |
val _ = normalize true true (mk_get_rules parse_ruletab) pre_ast;
|
|
336 |
in () end;
|
|
337 |
|
|
338 |
|
|
339 |
|
0
|
340 |
(** read **)
|
|
341 |
|
18
|
342 |
fun read (syn as Syntax (_, tabs)) ty str =
|
0
|
343 |
let
|
18
|
344 |
val Tabs {parse_ruletab, parse_trtab, ...} = tabs;
|
|
345 |
val ast = read_ast syn false (typ_to_nonterm ty) str;
|
0
|
346 |
in
|
|
347 |
ast_to_term (lookup parse_trtab)
|
18
|
348 |
(normalize_ast (mk_get_rules parse_ruletab) ast)
|
0
|
349 |
end;
|
|
350 |
|
|
351 |
|
|
352 |
|
144
|
353 |
(** read_typ **)
|
|
354 |
|
|
355 |
fun read_typ syn def_sort str = typ_of_term def_sort (read syn typeT str);
|
|
356 |
|
|
357 |
|
|
358 |
|
18
|
359 |
(** read_rule **)
|
|
360 |
|
|
361 |
fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
|
|
362 |
let
|
|
363 |
val Syntax (_, Tabs {consts, ...}) = syn;
|
|
364 |
|
|
365 |
fun constantify (ast as Constant _) = ast
|
|
366 |
| constantify (ast as Variable x) =
|
|
367 |
if x mem consts then Constant x else ast
|
|
368 |
| constantify (Appl asts) = Appl (map constantify asts);
|
0
|
369 |
|
18
|
370 |
fun read_pat (root, str) =
|
|
371 |
constantify (read_ast syn true root str)
|
|
372 |
handle ERROR => error ("The error above occurred in " ^ quote str);
|
|
373 |
|
|
374 |
val rule as (lhs, rhs) = (pairself read_pat) xrule;
|
|
375 |
in
|
|
376 |
(case rule_error rule of
|
|
377 |
Some msg =>
|
|
378 |
error ("Error in syntax translation rule: " ^ msg ^
|
|
379 |
"\nexternal: " ^ quote lhs_src ^ " -> " ^ quote rhs_src ^
|
|
380 |
"\ninternal: " ^ str_of_ast lhs ^ " -> " ^ str_of_ast rhs)
|
|
381 |
| None => rule)
|
|
382 |
end;
|
0
|
383 |
|
|
384 |
|
|
385 |
|
18
|
386 |
(** read_xrules **)
|
|
387 |
|
|
388 |
fun read_xrules syn xrules =
|
|
389 |
let
|
|
390 |
fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
|
|
391 |
| right_rule (xpat1 <-| xpat2) = None
|
|
392 |
| right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
|
0
|
393 |
|
18
|
394 |
fun left_rule (xpat1 |-> xpat2) = None
|
|
395 |
| left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
|
|
396 |
| left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
|
|
397 |
in
|
|
398 |
(map (read_rule syn) (mapfilter right_rule xrules),
|
|
399 |
map (read_rule syn) (mapfilter left_rule xrules))
|
|
400 |
end;
|
|
401 |
|
|
402 |
|
|
403 |
|
|
404 |
(** pretty terms or typs **)
|
|
405 |
|
|
406 |
fun pretty_t t_to_ast pretty_t (syn as Syntax (_, tabs)) t =
|
0
|
407 |
let
|
18
|
408 |
val Tabs {print_trtab, print_ruletab, prtab, ...} = tabs;
|
0
|
409 |
val ast = t_to_ast (lookup print_trtab) t;
|
|
410 |
in
|
18
|
411 |
pretty_t prtab (normalize_ast (mk_get_rules print_ruletab) ast)
|
0
|
412 |
end;
|
|
413 |
|
|
414 |
val pretty_term = pretty_t term_to_ast pretty_term_ast;
|
|
415 |
|
|
416 |
val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
|
|
417 |
|
|
418 |
fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
|
|
419 |
|
|
420 |
fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
|
|
421 |
|
|
422 |
|
|
423 |
|
|
424 |
(*** build syntax ***)
|
|
425 |
|
|
426 |
(* type_syn *)
|
|
427 |
|
167
|
428 |
val type_syn = mk_syntax (ref (ExtGG (ref EmptyGG, type_ext)));
|
|
429 |
|
|
430 |
|
171
|
431 |
(* extend *) (* FIXME *)
|
167
|
432 |
|
174
|
433 |
fun extend syn read_ty (roots, xconsts, sext) =
|
167
|
434 |
let
|
174
|
435 |
val Syntax (ggr0, tabs0 as Tabs {roots = roots0, ...}) = syn;
|
167
|
436 |
|
|
437 |
val ext1 = ext_of_sext ((distinct roots) \\ roots0) xconsts read_ty sext;
|
174
|
438 |
|
|
439 |
val (syn1 as Syntax (ggr1, tabs1)) =
|
175
|
440 |
(case ext1 of
|
|
441 |
Ext {roots = [], mfix = [], ...} =>
|
|
442 |
Syntax (ref (ExtGG (ggr0, ext1)), extend_tables tabs0 (mk_xgram ext1))
|
174
|
443 |
| _ => mk_syntax (ref (ExtGG (ggr0, ext1))));
|
167
|
444 |
|
|
445 |
val (parse_rules, print_rules) = read_xrules syn1 (xrules_of sext);
|
|
446 |
val ext2 = ExtRules {parse_rules = parse_rules, print_rules = print_rules};
|
|
447 |
in
|
|
448 |
Syntax (ref (ExtGG (ggr1, ext2)), extend_tables tabs1 (mk_xgram ext2))
|
|
449 |
end;
|
0
|
450 |
|
|
451 |
|
|
452 |
(* merge *)
|
|
453 |
|
167
|
454 |
fun merge roots syn1 syn2 =
|
|
455 |
let
|
|
456 |
val Syntax (ggr1, Tabs {roots = roots1, ...}) = syn1;
|
|
457 |
val Syntax (ggr2, Tabs {roots = roots2, ...}) = syn2;
|
|
458 |
val mggr = ref (MergeGG (ggr1, ggr2));
|
|
459 |
in
|
|
460 |
(case ((distinct roots) \\ roots1) \\ roots2 of
|
|
461 |
[] => mk_syntax mggr
|
|
462 |
| new_roots => mk_syntax (ref (ExtGG (mggr, ExtRoots new_roots))))
|
|
463 |
end;
|
0
|
464 |
|
|
465 |
|
|
466 |
end;
|
|
467 |
|