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