wenzelm@18
|
1 |
(* Title: Pure/Syntax/printer.ML
|
clasohm@0
|
2 |
ID: $Id$
|
clasohm@0
|
3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
|
wenzelm@18
|
4 |
|
wenzelm@18
|
5 |
Pretty printing of asts, terms, types and print (ast) translation.
|
clasohm@0
|
6 |
*)
|
clasohm@0
|
7 |
|
clasohm@0
|
8 |
signature PRINTER0 =
|
wenzelm@2384
|
9 |
sig
|
nipkow@504
|
10 |
val show_brackets: bool ref
|
nipkow@504
|
11 |
val show_sorts: bool ref
|
clasohm@0
|
12 |
val show_types: bool ref
|
wenzelm@617
|
13 |
val show_no_free_types: bool ref
|
wenzelm@2200
|
14 |
val print_mode: string list ref
|
wenzelm@2384
|
15 |
end;
|
clasohm@0
|
16 |
|
clasohm@0
|
17 |
signature PRINTER =
|
wenzelm@2384
|
18 |
sig
|
clasohm@0
|
19 |
include PRINTER0
|
wenzelm@2384
|
20 |
val term_to_ast: (string -> (typ -> term list -> term) option) -> term -> Ast.ast
|
wenzelm@2384
|
21 |
val typ_to_ast: (string -> (typ -> term list -> term) option) -> typ -> Ast.ast
|
wenzelm@2200
|
22 |
type prtabs
|
wenzelm@2200
|
23 |
val prmodes_of: prtabs -> string list
|
wenzelm@2200
|
24 |
val empty_prtabs: prtabs
|
wenzelm@2200
|
25 |
val extend_prtabs: prtabs -> string -> SynExt.xprod list -> prtabs
|
wenzelm@2200
|
26 |
val merge_prtabs: prtabs -> prtabs -> prtabs
|
wenzelm@2200
|
27 |
val pretty_term_ast: bool -> prtabs
|
wenzelm@2200
|
28 |
-> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T
|
wenzelm@2200
|
29 |
val pretty_typ_ast: bool -> prtabs
|
wenzelm@2200
|
30 |
-> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T
|
wenzelm@2384
|
31 |
end;
|
clasohm@0
|
32 |
|
wenzelm@2365
|
33 |
structure Printer: PRINTER =
|
clasohm@0
|
34 |
struct
|
wenzelm@2200
|
35 |
|
paulson@1509
|
36 |
open Lexicon Ast SynExt TypeExt SynTrans;
|
clasohm@0
|
37 |
|
wenzelm@2200
|
38 |
|
clasohm@0
|
39 |
(** options for printing **)
|
clasohm@0
|
40 |
|
clasohm@0
|
41 |
val show_types = ref false;
|
clasohm@0
|
42 |
val show_sorts = ref false;
|
nipkow@504
|
43 |
val show_brackets = ref false;
|
wenzelm@617
|
44 |
val show_no_free_types = ref false;
|
wenzelm@2200
|
45 |
val print_mode = ref ([]:string list);
|
wenzelm@617
|
46 |
|
clasohm@0
|
47 |
|
clasohm@0
|
48 |
|
wenzelm@18
|
49 |
(** convert term or typ to ast **)
|
clasohm@0
|
50 |
|
wenzelm@18
|
51 |
fun apply_trans name a f args =
|
wenzelm@18
|
52 |
(f args handle
|
clasohm@0
|
53 |
Match => raise Match
|
wenzelm@18
|
54 |
| exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn));
|
clasohm@0
|
55 |
|
clasohm@0
|
56 |
|
clasohm@0
|
57 |
fun ast_of_term trf show_types show_sorts tm =
|
clasohm@0
|
58 |
let
|
wenzelm@617
|
59 |
val no_freeTs = ! show_no_free_types;
|
wenzelm@617
|
60 |
|
clasohm@0
|
61 |
fun prune_typs (t_seen as (Const _, _)) = t_seen
|
clasohm@0
|
62 |
| prune_typs (t as Free (x, ty), seen) =
|
clasohm@0
|
63 |
if ty = dummyT then (t, seen)
|
wenzelm@617
|
64 |
else if no_freeTs orelse t mem seen then (free x, seen)
|
clasohm@0
|
65 |
else (t, t :: seen)
|
clasohm@0
|
66 |
| prune_typs (t as Var (xi, ty), seen) =
|
clasohm@0
|
67 |
if ty = dummyT then (t, seen)
|
wenzelm@617
|
68 |
else if no_freeTs orelse t mem seen then (var xi, seen)
|
clasohm@0
|
69 |
else (t, t :: seen)
|
clasohm@0
|
70 |
| prune_typs (t_seen as (Bound _, _)) = t_seen
|
clasohm@0
|
71 |
| prune_typs (Abs (x, ty, t), seen) =
|
clasohm@0
|
72 |
let val (t', seen') = prune_typs (t, seen);
|
clasohm@0
|
73 |
in (Abs (x, ty, t'), seen') end
|
clasohm@0
|
74 |
| prune_typs (t1 $ t2, seen) =
|
clasohm@0
|
75 |
let
|
clasohm@0
|
76 |
val (t1', seen') = prune_typs (t1, seen);
|
clasohm@0
|
77 |
val (t2', seen'') = prune_typs (t2, seen');
|
clasohm@0
|
78 |
in
|
clasohm@0
|
79 |
(t1' $ t2', seen'')
|
clasohm@0
|
80 |
end;
|
clasohm@0
|
81 |
|
clasohm@0
|
82 |
|
wenzelm@2384
|
83 |
fun ast_of (Const (a, T)) = trans a T []
|
wenzelm@554
|
84 |
| ast_of (Free (x, ty)) = constrain x (free x) ty
|
wenzelm@554
|
85 |
| ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (var xi) ty
|
clasohm@0
|
86 |
| ast_of (Bound i) = Variable ("B." ^ string_of_int i)
|
clasohm@0
|
87 |
| ast_of (t as Abs _) = ast_of (abs_tr' t)
|
clasohm@0
|
88 |
| ast_of (t as _ $ _) =
|
clasohm@0
|
89 |
(case strip_comb t of
|
wenzelm@2384
|
90 |
(Const (a, T), args) => trans a T args
|
clasohm@0
|
91 |
| (f, args) => Appl (map ast_of (f :: args)))
|
clasohm@0
|
92 |
|
wenzelm@2384
|
93 |
and trans a T args =
|
clasohm@0
|
94 |
(case trf a of
|
wenzelm@2384
|
95 |
Some f => ast_of (apply_trans "print translation" a (uncurry f) (T, args))
|
clasohm@0
|
96 |
| None => raise Match)
|
clasohm@0
|
97 |
handle Match => mk_appl (Constant a) (map ast_of args)
|
clasohm@0
|
98 |
|
clasohm@0
|
99 |
and constrain x t ty =
|
clasohm@0
|
100 |
if show_types andalso ty <> dummyT then
|
wenzelm@554
|
101 |
ast_of (const constrainC $ t $ term_of_typ show_sorts ty)
|
clasohm@0
|
102 |
else Variable x;
|
clasohm@0
|
103 |
in
|
wenzelm@381
|
104 |
if show_types then
|
wenzelm@381
|
105 |
ast_of (#1 (prune_typs (prop_tr' show_sorts tm, [])))
|
wenzelm@381
|
106 |
else ast_of (prop_tr' show_sorts tm)
|
clasohm@0
|
107 |
end;
|
clasohm@0
|
108 |
|
clasohm@0
|
109 |
|
clasohm@0
|
110 |
(* term_to_ast *)
|
clasohm@0
|
111 |
|
clasohm@0
|
112 |
fun term_to_ast trf tm =
|
wenzelm@2200
|
113 |
ast_of_term trf (! show_types orelse ! show_sorts) (! show_sorts) tm;
|
clasohm@0
|
114 |
|
clasohm@0
|
115 |
|
clasohm@0
|
116 |
(* typ_to_ast *)
|
clasohm@0
|
117 |
|
clasohm@0
|
118 |
fun typ_to_ast trf ty =
|
clasohm@0
|
119 |
ast_of_term trf false false (term_of_typ (! show_sorts) ty);
|
clasohm@0
|
120 |
|
clasohm@0
|
121 |
|
clasohm@0
|
122 |
|
wenzelm@2200
|
123 |
(** type prtabs **)
|
clasohm@0
|
124 |
|
clasohm@0
|
125 |
datatype symb =
|
clasohm@0
|
126 |
Arg of int |
|
clasohm@0
|
127 |
TypArg of int |
|
clasohm@0
|
128 |
String of string |
|
clasohm@0
|
129 |
Break of int |
|
clasohm@0
|
130 |
Block of int * symb list;
|
clasohm@0
|
131 |
|
wenzelm@2200
|
132 |
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
|
wenzelm@2200
|
133 |
|
wenzelm@2365
|
134 |
fun prmodes_of prtabs = filter_out (equal "") (map fst prtabs);
|
wenzelm@2200
|
135 |
|
wenzelm@2200
|
136 |
(*find tab for mode*)
|
wenzelm@2200
|
137 |
fun get_tab prtabs mode =
|
wenzelm@2200
|
138 |
if_none (assoc (prtabs, mode)) Symtab.null;
|
wenzelm@2200
|
139 |
|
wenzelm@2200
|
140 |
(*collect tabs for mode hierarchy (default "")*)
|
wenzelm@2200
|
141 |
fun tabs_of prtabs modes =
|
wenzelm@2200
|
142 |
mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]);
|
wenzelm@2200
|
143 |
|
wenzelm@2200
|
144 |
(*find formats in tab hierarchy*)
|
wenzelm@2200
|
145 |
fun get_fmts [] _ = []
|
wenzelm@2200
|
146 |
| get_fmts (tab :: tabs) a = Symtab.lookup_multi (tab, a) @ get_fmts tabs a;
|
clasohm@0
|
147 |
|
clasohm@0
|
148 |
|
wenzelm@237
|
149 |
(* xprods_to_fmts *)
|
clasohm@0
|
150 |
|
wenzelm@237
|
151 |
fun xprod_to_fmt (XProd (_, _, "", _)) = None
|
wenzelm@237
|
152 |
| xprod_to_fmt (XProd (_, xsymbs, const, pri)) =
|
wenzelm@237
|
153 |
let
|
wenzelm@2384
|
154 |
fun cons_str s (String s' :: syms) = String (s ^ s') :: syms
|
wenzelm@2384
|
155 |
| cons_str s syms = String s :: syms;
|
wenzelm@2384
|
156 |
|
wenzelm@237
|
157 |
fun arg (s, p) =
|
wenzelm@237
|
158 |
(if s = "type" then TypArg else Arg)
|
nipkow@506
|
159 |
(if is_terminal s then max_pri else p);
|
wenzelm@237
|
160 |
|
wenzelm@237
|
161 |
fun xsyms_to_syms (Delim s :: xsyms) =
|
wenzelm@2384
|
162 |
apfst (cons_str s) (xsyms_to_syms xsyms)
|
wenzelm@237
|
163 |
| xsyms_to_syms (Argument s_p :: xsyms) =
|
wenzelm@237
|
164 |
apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
|
wenzelm@237
|
165 |
| xsyms_to_syms (Space s :: xsyms) =
|
wenzelm@2384
|
166 |
apfst (cons_str s) (xsyms_to_syms xsyms)
|
wenzelm@237
|
167 |
| xsyms_to_syms (Bg i :: xsyms) =
|
wenzelm@237
|
168 |
let
|
wenzelm@237
|
169 |
val (bsyms, xsyms') = xsyms_to_syms xsyms;
|
wenzelm@237
|
170 |
val (syms, xsyms'') = xsyms_to_syms xsyms';
|
wenzelm@237
|
171 |
in
|
wenzelm@237
|
172 |
(Block (i, bsyms) :: syms, xsyms'')
|
wenzelm@237
|
173 |
end
|
wenzelm@237
|
174 |
| xsyms_to_syms (Brk i :: xsyms) =
|
wenzelm@237
|
175 |
apfst (cons (Break i)) (xsyms_to_syms xsyms)
|
wenzelm@237
|
176 |
| xsyms_to_syms (En :: xsyms) = ([], xsyms)
|
wenzelm@237
|
177 |
| xsyms_to_syms [] = ([], []);
|
wenzelm@237
|
178 |
|
wenzelm@237
|
179 |
fun nargs (Arg _ :: syms) = nargs syms + 1
|
wenzelm@237
|
180 |
| nargs (TypArg _ :: syms) = nargs syms + 1
|
wenzelm@237
|
181 |
| nargs (String _ :: syms) = nargs syms
|
wenzelm@237
|
182 |
| nargs (Break _ :: syms) = nargs syms
|
wenzelm@237
|
183 |
| nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms
|
wenzelm@237
|
184 |
| nargs [] = 0;
|
wenzelm@237
|
185 |
in
|
wenzelm@237
|
186 |
(case xsyms_to_syms xsymbs of
|
wenzelm@237
|
187 |
(symbs, []) => Some (const, (symbs, nargs symbs, pri))
|
wenzelm@237
|
188 |
| _ => sys_error "xprod_to_fmt: unbalanced blocks")
|
wenzelm@237
|
189 |
end;
|
wenzelm@237
|
190 |
|
wenzelm@2200
|
191 |
fun xprods_to_fmts xprods = mapfilter xprod_to_fmt xprods;
|
wenzelm@237
|
192 |
|
wenzelm@237
|
193 |
|
wenzelm@237
|
194 |
(* empty, extend, merge prtabs *)
|
wenzelm@237
|
195 |
|
wenzelm@2200
|
196 |
val empty_prtabs = [];
|
clasohm@0
|
197 |
|
wenzelm@2200
|
198 |
fun extend_prtabs prtabs mode xprods =
|
wenzelm@2200
|
199 |
let
|
wenzelm@2200
|
200 |
val fmts = xprods_to_fmts xprods;
|
wenzelm@2200
|
201 |
val tab = get_tab prtabs mode;
|
wenzelm@2200
|
202 |
val new_tab = generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab fmts;
|
wenzelm@2200
|
203 |
in overwrite (prtabs, (mode, new_tab)) end;
|
clasohm@0
|
204 |
|
wenzelm@2200
|
205 |
fun merge_prtabs prtabs1 prtabs2 =
|
wenzelm@2200
|
206 |
let
|
wenzelm@2200
|
207 |
val modes = distinct (map fst (prtabs1 @ prtabs2));
|
wenzelm@2200
|
208 |
fun merge mode =
|
wenzelm@2200
|
209 |
(mode,
|
wenzelm@2200
|
210 |
generic_merge (op =) Symtab.dest_multi Symtab.make_multi
|
wenzelm@2200
|
211 |
(get_tab prtabs1 mode) (get_tab prtabs2 mode));
|
wenzelm@2200
|
212 |
in
|
wenzelm@2200
|
213 |
map merge modes
|
wenzelm@2200
|
214 |
end;
|
wenzelm@18
|
215 |
|
wenzelm@18
|
216 |
|
clasohm@0
|
217 |
|
wenzelm@237
|
218 |
(** pretty term or typ asts **)
|
clasohm@0
|
219 |
|
wenzelm@2200
|
220 |
fun is_chain [Block (_, pr)] = is_chain pr
|
wenzelm@2200
|
221 |
| is_chain [Arg _] = true
|
wenzelm@2200
|
222 |
| is_chain _ = false;
|
nipkow@506
|
223 |
|
wenzelm@2200
|
224 |
fun pretty tabs trf type_mode curried ast0 p0 =
|
clasohm@0
|
225 |
let
|
wenzelm@18
|
226 |
val trans = apply_trans "print ast translation";
|
wenzelm@18
|
227 |
|
wenzelm@2200
|
228 |
(*default applications: prefix / postfix*)
|
wenzelm@2200
|
229 |
val appT =
|
wenzelm@2200
|
230 |
if type_mode then tappl_ast_tr'
|
wenzelm@2200
|
231 |
else if curried then applC_ast_tr'
|
wenzelm@2200
|
232 |
else appl_ast_tr';
|
wenzelm@18
|
233 |
|
clasohm@0
|
234 |
fun synT ([], args) = ([], args)
|
clasohm@0
|
235 |
| synT (Arg p :: symbs, t :: args) =
|
wenzelm@18
|
236 |
let val (Ts, args') = synT (symbs, args);
|
clasohm@0
|
237 |
in (astT (t, p) @ Ts, args') end
|
clasohm@0
|
238 |
| synT (TypArg p :: symbs, t :: args) =
|
wenzelm@237
|
239 |
let
|
wenzelm@237
|
240 |
val (Ts, args') = synT (symbs, args);
|
wenzelm@237
|
241 |
in
|
wenzelm@237
|
242 |
if type_mode then (astT (t, p) @ Ts, args')
|
wenzelm@2200
|
243 |
else (pretty tabs trf true curried t p @ Ts, args')
|
wenzelm@237
|
244 |
end
|
clasohm@0
|
245 |
| synT (String s :: symbs, args) =
|
wenzelm@18
|
246 |
let val (Ts, args') = synT (symbs, args);
|
clasohm@0
|
247 |
in (Pretty.str s :: Ts, args') end
|
clasohm@0
|
248 |
| synT (Block (i, bsymbs) :: symbs, args) =
|
clasohm@0
|
249 |
let
|
clasohm@0
|
250 |
val (bTs, args') = synT (bsymbs, args);
|
clasohm@0
|
251 |
val (Ts, args'') = synT (symbs, args');
|
clasohm@0
|
252 |
in (Pretty.blk (i, bTs) :: Ts, args'') end
|
clasohm@0
|
253 |
| synT (Break i :: symbs, args) =
|
wenzelm@18
|
254 |
let val (Ts, args') = synT (symbs, args);
|
wenzelm@18
|
255 |
in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end
|
wenzelm@237
|
256 |
| synT (_ :: _, []) = sys_error "synT"
|
clasohm@0
|
257 |
|
wenzelm@554
|
258 |
and parT (pr, args, p, p': int) = #1 (synT
|
wenzelm@554
|
259 |
(if p > p' orelse
|
wenzelm@2200
|
260 |
(! show_brackets andalso p' <> max_pri andalso not (is_chain pr))
|
wenzelm@554
|
261 |
then [Block (1, String "(" :: pr @ [String ")"])]
|
wenzelm@554
|
262 |
else pr, args))
|
clasohm@0
|
263 |
|
clasohm@0
|
264 |
and prefixT (_, a, [], _) = [Pretty.str a]
|
wenzelm@2384
|
265 |
| prefixT (c, _, args, p) =
|
wenzelm@2384
|
266 |
if c = Constant "_appl" orelse c = Constant "_applC" then
|
wenzelm@2384
|
267 |
error "Syntax insufficient for printing prefix applications"
|
wenzelm@2384
|
268 |
else astT (appT (c, args), p)
|
clasohm@0
|
269 |
|
wenzelm@18
|
270 |
and splitT 0 ([x], ys) = (x, ys)
|
wenzelm@18
|
271 |
| splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys)
|
wenzelm@18
|
272 |
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys)
|
wenzelm@237
|
273 |
| splitT _ _ = sys_error "splitT"
|
wenzelm@18
|
274 |
|
clasohm@0
|
275 |
and combT (tup as (c, a, args, p)) =
|
clasohm@0
|
276 |
let
|
clasohm@0
|
277 |
val nargs = length args;
|
wenzelm@18
|
278 |
|
wenzelm@2200
|
279 |
(*find matching table entry, or print as prefix/postfix*)
|
wenzelm@2200
|
280 |
fun prnt [] = prefixT tup
|
wenzelm@2200
|
281 |
| prnt ((pr, n, p') :: prnps) =
|
wenzelm@2200
|
282 |
if nargs = n then parT (pr, args, p, p')
|
wenzelm@2200
|
283 |
else if nargs > n andalso not type_mode then
|
wenzelm@2200
|
284 |
astT (appT (splitT n ([c], args)), p)
|
wenzelm@2200
|
285 |
else prnt prnps;
|
wenzelm@2200
|
286 |
in
|
wenzelm@2200
|
287 |
(*try translation function first*)
|
wenzelm@2200
|
288 |
(case trf a of
|
wenzelm@2200
|
289 |
None => prnt (get_fmts tabs a)
|
wenzelm@2200
|
290 |
| Some f => (astT (trans a f args, p) handle Match => prnt (get_fmts tabs a)))
|
wenzelm@2200
|
291 |
end
|
wenzelm@2200
|
292 |
|
clasohm@0
|
293 |
and astT (c as Constant a, p) = combT (c, a, [], p)
|
clasohm@0
|
294 |
| astT (Variable x, _) = [Pretty.str x]
|
wenzelm@18
|
295 |
| astT (Appl ((c as Constant a) :: (args as _ :: _)), p) =
|
wenzelm@18
|
296 |
combT (c, a, args, p)
|
clasohm@0
|
297 |
| astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
|
wenzelm@18
|
298 |
| astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast];
|
clasohm@0
|
299 |
in
|
clasohm@0
|
300 |
astT (ast0, p0)
|
clasohm@0
|
301 |
end;
|
clasohm@0
|
302 |
|
clasohm@0
|
303 |
|
clasohm@0
|
304 |
(* pretty_term_ast *)
|
clasohm@0
|
305 |
|
wenzelm@2200
|
306 |
fun pretty_term_ast curried prtabs trf ast =
|
wenzelm@2200
|
307 |
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) trf false curried ast 0);
|
clasohm@0
|
308 |
|
clasohm@0
|
309 |
|
clasohm@0
|
310 |
(* pretty_typ_ast *)
|
clasohm@0
|
311 |
|
wenzelm@2200
|
312 |
fun pretty_typ_ast _ prtabs trf ast =
|
wenzelm@2200
|
313 |
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) trf true false ast 0);
|
clasohm@0
|
314 |
|
clasohm@0
|
315 |
|
clasohm@0
|
316 |
end;
|