18
|
1 |
(* Title: Pure/Syntax/printer.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
18
|
4 |
|
|
5 |
Pretty printing of asts, terms, types and print (ast) translation.
|
0
|
6 |
*)
|
|
7 |
|
|
8 |
signature PRINTER0 =
|
|
9 |
sig
|
|
10 |
val show_types: bool ref
|
|
11 |
val show_sorts: bool ref
|
|
12 |
end;
|
|
13 |
|
|
14 |
signature PRINTER =
|
|
15 |
sig
|
|
16 |
include PRINTER0
|
|
17 |
structure Symtab: SYMTAB
|
|
18 |
structure XGram: XGRAM
|
|
19 |
structure Pretty: PRETTY
|
|
20 |
local open XGram XGram.Ast in
|
|
21 |
val term_to_ast: (string -> (term list -> term) option) -> term -> ast
|
|
22 |
val typ_to_ast: (string -> (term list -> term) option) -> typ -> ast
|
18
|
23 |
type prtab
|
|
24 |
val empty_prtab: prtab
|
|
25 |
val extend_prtab: prtab -> (string prod list) -> (string * (ast list -> ast)) list
|
|
26 |
-> prtab
|
|
27 |
val mk_prtab: (string prod list) -> (string * (ast list -> ast)) list -> prtab
|
|
28 |
val pretty_term_ast: prtab -> ast -> Pretty.T
|
|
29 |
val pretty_typ_ast: prtab -> ast -> Pretty.T
|
0
|
30 |
end
|
|
31 |
end;
|
|
32 |
|
|
33 |
functor PrinterFun(structure Symtab: SYMTAB and Lexicon: LEXICON
|
|
34 |
and TypeExt: TYPE_EXT and SExtension: SEXTENSION and Pretty: PRETTY
|
|
35 |
sharing TypeExt.Extension = SExtension.Extension) (*: PRINTER *) = (* FIXME *)
|
|
36 |
struct
|
|
37 |
|
|
38 |
structure Symtab = Symtab;
|
|
39 |
structure Extension = TypeExt.Extension;
|
|
40 |
structure XGram = Extension.XGram;
|
|
41 |
structure Pretty = Pretty;
|
|
42 |
open XGram XGram.Ast Lexicon TypeExt Extension SExtension;
|
|
43 |
|
|
44 |
|
|
45 |
(** options for printing **)
|
|
46 |
|
|
47 |
val show_types = ref false;
|
|
48 |
val show_sorts = ref false;
|
|
49 |
|
|
50 |
|
|
51 |
|
18
|
52 |
(** convert term or typ to ast **)
|
0
|
53 |
|
18
|
54 |
fun apply_trans name a f args =
|
|
55 |
(f args handle
|
0
|
56 |
Match => raise Match
|
18
|
57 |
| exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
|
0
|
58 |
|
|
59 |
|
|
60 |
fun ast_of_term trf show_types show_sorts tm =
|
|
61 |
let
|
18
|
62 |
(*(* FIXME old - remove *)
|
|
63 |
fun fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t)
|
|
64 |
| fix_aprop tys t =
|
|
65 |
let
|
|
66 |
val (f, args) = strip_comb t;
|
|
67 |
val t' = list_comb (f, map (fix_aprop tys) args);
|
|
68 |
in
|
|
69 |
if not (is_Const f) andalso fastype_of (tys, t) = propT
|
|
70 |
then Const (apropC, dummyT) $ t' else t'
|
|
71 |
end;
|
|
72 |
|
0
|
73 |
val aprop_const = Const (apropC, dummyT);
|
|
74 |
|
|
75 |
fun fix_aprop (tm as Const _) = tm
|
|
76 |
| fix_aprop (tm as Free (x, ty)) =
|
|
77 |
if ty = propT then aprop_const $ Free (x, dummyT) else tm
|
|
78 |
| fix_aprop (tm as Var (xi, ty)) =
|
|
79 |
if ty = propT then aprop_const $ Var (xi, dummyT) else tm
|
|
80 |
| fix_aprop (tm as Bound _) = tm
|
|
81 |
| fix_aprop (Abs (x, ty, t)) = Abs (x, ty, fix_aprop t)
|
|
82 |
| fix_aprop (t1 $ t2) = fix_aprop t1 $ fix_aprop t2;
|
|
83 |
|
18
|
84 |
val fix_aprop = fn _ => fn tm => fix_aprop tm;
|
|
85 |
*)
|
|
86 |
|
|
87 |
(* FIXME check *)
|
|
88 |
|
|
89 |
fun aprop t = Const (apropC, dummyT) $ t;
|
|
90 |
|
|
91 |
fun is_prop tys tm =
|
|
92 |
fastype_of (tys, tm) = propT handle TERM _ => false;
|
|
93 |
|
|
94 |
fun fix_aprop _ (tm as Const _) = tm
|
|
95 |
| fix_aprop _ (tm as Free (x, ty)) =
|
|
96 |
if ty = propT then aprop (Free (x, dummyT)) else tm
|
|
97 |
| fix_aprop _ (tm as Var (xi, ty)) =
|
|
98 |
if ty = propT then aprop (Var (xi, dummyT)) else tm
|
|
99 |
| fix_aprop tys (tm as Bound _) =
|
|
100 |
if is_prop tys tm then aprop tm else tm
|
|
101 |
| fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t)
|
|
102 |
| fix_aprop tys (tm as t1 $ t2) =
|
|
103 |
(if is_Const (head_of tm) orelse not (is_prop tys tm)
|
|
104 |
then I else aprop) (fix_aprop tys t1 $ fix_aprop tys t2);
|
|
105 |
|
0
|
106 |
|
|
107 |
fun prune_typs (t_seen as (Const _, _)) = t_seen
|
|
108 |
| prune_typs (t as Free (x, ty), seen) =
|
|
109 |
if ty = dummyT then (t, seen)
|
|
110 |
else if t mem seen then (Free (x, dummyT), seen)
|
|
111 |
else (t, t :: seen)
|
|
112 |
| prune_typs (t as Var (xi, ty), seen) =
|
|
113 |
if ty = dummyT then (t, seen)
|
|
114 |
else if t mem seen then (Var (xi, dummyT), seen)
|
|
115 |
else (t, t :: seen)
|
|
116 |
| prune_typs (t_seen as (Bound _, _)) = t_seen
|
|
117 |
| prune_typs (Abs (x, ty, t), seen) =
|
|
118 |
let val (t', seen') = prune_typs (t, seen);
|
|
119 |
in (Abs (x, ty, t'), seen') end
|
|
120 |
| prune_typs (t1 $ t2, seen) =
|
|
121 |
let
|
|
122 |
val (t1', seen') = prune_typs (t1, seen);
|
|
123 |
val (t2', seen'') = prune_typs (t2, seen');
|
|
124 |
in
|
|
125 |
(t1' $ t2', seen'')
|
|
126 |
end;
|
|
127 |
|
|
128 |
|
|
129 |
fun ast_of (Const (a, _)) = trans a []
|
|
130 |
| ast_of (Free (x, ty)) = constrain x (Free (x, dummyT)) ty
|
|
131 |
| ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (Var (xi, dummyT)) ty
|
|
132 |
| ast_of (Bound i) = Variable ("B." ^ string_of_int i)
|
|
133 |
| ast_of (t as Abs _) = ast_of (abs_tr' t)
|
|
134 |
| ast_of (t as _ $ _) =
|
|
135 |
(case strip_comb t of
|
|
136 |
(Const (a, _), args) => trans a args
|
|
137 |
| (f, args) => Appl (map ast_of (f :: args)))
|
|
138 |
|
|
139 |
and trans a args =
|
|
140 |
(case trf a of
|
18
|
141 |
Some f => ast_of (apply_trans "print translation" a f args)
|
0
|
142 |
| None => raise Match)
|
|
143 |
handle Match => mk_appl (Constant a) (map ast_of args)
|
|
144 |
|
|
145 |
and constrain x t ty =
|
|
146 |
if show_types andalso ty <> dummyT then
|
|
147 |
ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty)
|
|
148 |
else Variable x;
|
|
149 |
in
|
18
|
150 |
if show_types then ast_of (#1 (prune_typs (fix_aprop [] tm, [])))
|
|
151 |
else ast_of (fix_aprop [] tm)
|
0
|
152 |
end;
|
|
153 |
|
|
154 |
|
|
155 |
(* term_to_ast *)
|
|
156 |
|
|
157 |
fun term_to_ast trf tm =
|
|
158 |
ast_of_term trf (! show_types) (! show_sorts) tm;
|
|
159 |
|
|
160 |
|
|
161 |
(* typ_to_ast *)
|
|
162 |
|
|
163 |
fun typ_to_ast trf ty =
|
|
164 |
ast_of_term trf false false (term_of_typ (! show_sorts) ty);
|
|
165 |
|
|
166 |
|
|
167 |
|
18
|
168 |
(** type prtab **)
|
0
|
169 |
|
|
170 |
datatype symb =
|
|
171 |
Arg of int |
|
|
172 |
TypArg of int |
|
|
173 |
String of string |
|
|
174 |
Break of int |
|
|
175 |
Block of int * symb list;
|
|
176 |
|
|
177 |
datatype format =
|
|
178 |
Prnt of symb list * int * int |
|
|
179 |
Trns of ast list -> ast |
|
|
180 |
TorP of (ast list -> ast) * (symb list * int * int);
|
|
181 |
|
18
|
182 |
type prtab = format Symtab.table;
|
|
183 |
|
|
184 |
|
|
185 |
(* empty_prtab *)
|
|
186 |
|
|
187 |
val empty_prtab = Symtab.null;
|
0
|
188 |
|
|
189 |
|
|
190 |
|
18
|
191 |
(** extend_prtab **)
|
0
|
192 |
|
18
|
193 |
fun extend_prtab prtab prods trfuns =
|
0
|
194 |
let
|
|
195 |
fun nargs (Arg _ :: symbs) = nargs symbs + 1
|
|
196 |
| nargs (TypArg _ :: symbs) = nargs symbs + 1
|
|
197 |
| nargs (String _ :: symbs) = nargs symbs
|
|
198 |
| nargs (Break _ :: symbs) = nargs symbs
|
|
199 |
| nargs (Block (_, bsymbs) :: symbs) = nargs symbs + nargs bsymbs
|
|
200 |
| nargs [] = 0;
|
|
201 |
|
|
202 |
fun merge (s, String s' :: l) = String (s ^ s') :: l
|
|
203 |
| merge (s, l) = String s :: l;
|
|
204 |
|
18
|
205 |
fun mk_prnp sy c p =
|
0
|
206 |
let
|
18
|
207 |
val constr = (c = constrainC orelse c = constrainIdtC);
|
0
|
208 |
|
|
209 |
fun syn2pr (Terminal s :: sy) =
|
18
|
210 |
let val (symbs, sy') = syn2pr sy;
|
0
|
211 |
in (merge (s, symbs), sy') end
|
|
212 |
| syn2pr (Space s :: sy) =
|
18
|
213 |
let val (symbs, sy') = syn2pr sy;
|
0
|
214 |
in (merge (s, symbs), sy') end
|
|
215 |
| syn2pr (Nonterminal (s, p) :: sy) =
|
|
216 |
let
|
|
217 |
val (symbs, sy') = syn2pr sy;
|
|
218 |
val symb =
|
|
219 |
(if constr andalso s = "type" then TypArg else Arg)
|
|
220 |
(if is_terminal s then 0 else p);
|
|
221 |
in (symb :: symbs, sy') end
|
|
222 |
| syn2pr (Bg i :: sy) =
|
|
223 |
let
|
|
224 |
val (bsymbs, sy') = syn2pr sy;
|
|
225 |
val (symbs, sy'') = syn2pr sy';
|
|
226 |
in (Block (i, bsymbs) :: symbs, sy'') end
|
|
227 |
| syn2pr (Brk i :: sy) =
|
18
|
228 |
let val (symbs, sy') = syn2pr sy;
|
0
|
229 |
in (Break i :: symbs, sy') end
|
|
230 |
| syn2pr (En :: sy) = ([], sy)
|
|
231 |
| syn2pr [] = ([], []);
|
|
232 |
|
|
233 |
val (pr, _) = syn2pr sy;
|
|
234 |
in
|
|
235 |
(pr, nargs pr, p)
|
|
236 |
end;
|
|
237 |
|
18
|
238 |
fun trns_err c = error ("More than one parse ast translation for " ^ quote c);
|
|
239 |
|
|
240 |
fun add_fmt tab c fmt x = Symtab.update ((c, fmt x), tab);
|
0
|
241 |
|
18
|
242 |
fun add_prod (tab, Prod (_, _, "", _)) = tab
|
|
243 |
| add_prod (tab, Prod (_, sy, c, p)) =
|
|
244 |
(case Symtab.lookup (tab, c) of
|
|
245 |
None => add_fmt tab c Prnt (mk_prnp sy c p)
|
|
246 |
| Some (Prnt _) => add_fmt tab c Prnt (mk_prnp sy c p)
|
|
247 |
| Some (Trns f) => add_fmt tab c TorP (f, mk_prnp sy c p)
|
|
248 |
| Some (TorP (f, _)) => add_fmt tab c TorP (f, mk_prnp sy c p));
|
|
249 |
|
|
250 |
fun add_tr (tab, (c, f)) =
|
|
251 |
(case Symtab.lookup (tab, c) of
|
|
252 |
None => add_fmt tab c Trns f
|
|
253 |
| Some (Prnt pr) => add_fmt tab c TorP (f, pr)
|
|
254 |
| Some (Trns _) => trns_err c
|
|
255 |
| Some (TorP _) => trns_err c);
|
0
|
256 |
in
|
18
|
257 |
Symtab.balance (foldl add_prod (foldl add_tr (prtab, trfuns), prods))
|
0
|
258 |
end;
|
|
259 |
|
|
260 |
|
18
|
261 |
(* mk_prtab *)
|
0
|
262 |
|
18
|
263 |
val mk_prtab = extend_prtab empty_prtab;
|
|
264 |
|
|
265 |
|
|
266 |
|
|
267 |
(** pretty term/typ asts **)
|
0
|
268 |
|
18
|
269 |
(*pretty assumes a syntax derived from Pure, otherwise it may loop forever*)
|
0
|
270 |
|
18
|
271 |
fun pretty tab type_mode ast0 p0 =
|
0
|
272 |
let
|
18
|
273 |
val trans = apply_trans "print ast translation";
|
|
274 |
|
|
275 |
val appT = if type_mode then tappl_ast_tr' else appl_ast_tr';
|
|
276 |
|
0
|
277 |
fun synT ([], args) = ([], args)
|
|
278 |
| synT (Arg p :: symbs, t :: args) =
|
18
|
279 |
let val (Ts, args') = synT (symbs, args);
|
0
|
280 |
in (astT (t, p) @ Ts, args') end
|
|
281 |
| synT (TypArg p :: symbs, t :: args) =
|
18
|
282 |
let val (Ts, args') = synT (symbs, args);
|
|
283 |
in (pretty tab true t p @ Ts, args') end
|
0
|
284 |
| synT (String s :: symbs, args) =
|
18
|
285 |
let val (Ts, args') = synT (symbs, args);
|
0
|
286 |
in (Pretty.str s :: Ts, args') end
|
|
287 |
| synT (Block (i, bsymbs) :: symbs, args) =
|
|
288 |
let
|
|
289 |
val (bTs, args') = synT (bsymbs, args);
|
|
290 |
val (Ts, args'') = synT (symbs, args');
|
|
291 |
in (Pretty.blk (i, bTs) :: Ts, args'') end
|
|
292 |
| synT (Break i :: symbs, args) =
|
18
|
293 |
let val (Ts, args') = synT (symbs, args);
|
|
294 |
in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
|
0
|
295 |
| synT (_ :: _, []) = error "synT"
|
|
296 |
|
|
297 |
and parT (pr, args, p, p': int) =
|
18
|
298 |
if p > p' then
|
|
299 |
#1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args))
|
|
300 |
else #1 (synT (pr, args))
|
0
|
301 |
|
|
302 |
and prefixT (_, a, [], _) = [Pretty.str a]
|
|
303 |
| prefixT (c, _, args, p) = astT (appT (c, args), p)
|
|
304 |
|
18
|
305 |
and splitT 0 ([x], ys) = (x, ys)
|
|
306 |
| splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys)
|
|
307 |
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
|
|
308 |
| splitT _ _ = error "splitT"
|
|
309 |
|
0
|
310 |
and combT (tup as (c, a, args, p)) =
|
|
311 |
let
|
|
312 |
val nargs = length args;
|
18
|
313 |
|
0
|
314 |
fun prnt (pr, n, p') =
|
18
|
315 |
if nargs = n then parT (pr, args, p, p')
|
|
316 |
else if nargs < n orelse type_mode then prefixT tup
|
|
317 |
else astT (appT (splitT n ([c], args)), p);
|
0
|
318 |
in
|
18
|
319 |
(case Symtab.lookup (tab, a) of
|
0
|
320 |
None => prefixT tup
|
|
321 |
| Some (Prnt prnp) => prnt prnp
|
|
322 |
| Some (Trns f) =>
|
18
|
323 |
(astT (trans a f args, p) handle Match => prefixT tup)
|
0
|
324 |
| Some (TorP (f, prnp)) =>
|
18
|
325 |
(astT (trans a f args, p) handle Match => prnt prnp))
|
0
|
326 |
end
|
|
327 |
|
|
328 |
and astT (c as Constant a, p) = combT (c, a, [], p)
|
|
329 |
| astT (Variable x, _) = [Pretty.str x]
|
18
|
330 |
| astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
|
|
331 |
combT (c, a, args, p)
|
0
|
332 |
| astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
|
18
|
333 |
| astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
|
0
|
334 |
in
|
|
335 |
astT (ast0, p0)
|
|
336 |
end;
|
|
337 |
|
|
338 |
|
|
339 |
(* pretty_term_ast *)
|
|
340 |
|
|
341 |
fun pretty_term_ast tab ast =
|
18
|
342 |
Pretty.blk (0, pretty tab false ast 0);
|
0
|
343 |
|
|
344 |
|
|
345 |
(* pretty_typ_ast *)
|
|
346 |
|
|
347 |
fun pretty_typ_ast tab ast =
|
18
|
348 |
Pretty.blk (0, pretty tab true ast 0);
|
0
|
349 |
|
|
350 |
|
|
351 |
end;
|
|
352 |
|