27 type prtabs |
27 type prtabs |
28 val empty_prtabs: prtabs |
28 val empty_prtabs: prtabs |
29 val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
29 val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
30 val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
30 val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs |
31 val merge_prtabs: prtabs -> prtabs -> prtabs |
31 val merge_prtabs: prtabs -> prtabs -> prtabs |
32 val pretty_term_ast: Context.generic -> bool -> prtabs |
32 val pretty_term_ast: (string -> xstring) -> Context.generic -> bool -> prtabs |
33 -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list) |
33 -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list) |
34 -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T |
34 -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T |
35 val pretty_typ_ast: Context.generic -> bool -> prtabs |
35 val pretty_typ_ast: Context.generic -> bool -> prtabs |
36 -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list) |
36 -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list) |
37 -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T |
37 -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T |
263 |
263 |
264 fun is_chain [Block (_, pr)] = is_chain pr |
264 fun is_chain [Block (_, pr)] = is_chain pr |
265 | is_chain [Arg _] = true |
265 | is_chain [Arg _] = true |
266 | is_chain _ = false; |
266 | is_chain _ = false; |
267 |
267 |
268 fun pretty context tabs trf tokentrf type_mode curried ast0 p0 = |
268 fun pretty extern_const context tabs trf tokentrf type_mode curried ast0 p0 = |
269 let |
269 let |
270 val trans = apply_trans context "print ast translation"; |
270 val trans = apply_trans context "print ast translation"; |
271 |
271 |
272 fun token_trans c [Ast.Variable x] = |
272 fun token_trans c [Ast.Variable x] = |
273 (case tokentrf c of |
273 (case tokentrf c of |
288 | synT (TypArg p :: symbs, t :: args) = |
288 | synT (TypArg p :: symbs, t :: args) = |
289 let |
289 let |
290 val (Ts, args') = synT (symbs, args); |
290 val (Ts, args') = synT (symbs, args); |
291 in |
291 in |
292 if type_mode then (astT (t, p) @ Ts, args') |
292 if type_mode then (astT (t, p) @ Ts, args') |
293 else (pretty context tabs trf tokentrf true curried t p @ Ts, args') |
293 else (pretty I context tabs trf tokentrf true curried t p @ Ts, args') |
294 end |
294 end |
295 | synT (String s :: symbs, args) = |
295 | synT (String s :: symbs, args) = |
296 let val (Ts, args') = synT (symbs, args); |
296 let val (Ts, args') = synT (symbs, args); |
297 in (Pretty.str s :: Ts, args') end |
297 in (Pretty.str s :: Ts, args') end |
298 | synT (Block (i, bsymbs) :: symbs, args) = |
298 | synT (Block (i, bsymbs) :: symbs, args) = |
314 (if p > p' orelse |
314 (if p > p' orelse |
315 (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr)) |
315 (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr)) |
316 then [Block (1, String "(" :: pr @ [String ")"])] |
316 then [Block (1, String "(" :: pr @ [String ")"])] |
317 else pr, args)) |
317 else pr, args)) |
318 |
318 |
319 and prefixT (_, a, [], _) = [Pretty.str a] |
319 and atomT a = |
|
320 (case try (unprefix Lexicon.constN) a of |
|
321 SOME c => Pretty.str (extern_const c) |
|
322 | NONE => |
|
323 (case try (unprefix Lexicon.fixedN) a of |
|
324 SOME x => |
|
325 (case tokentrf "_free" of |
|
326 SOME f => Pretty.raw_str (f x) |
|
327 | NONE => Pretty.str x) |
|
328 | NONE => Pretty.str a)) |
|
329 |
|
330 and prefixT (_, a, [], _) = [atomT a] |
320 | prefixT (c, _, args, p) = astT (appT (c, args), p) |
331 | prefixT (c, _, args, p) = astT (appT (c, args), p) |
321 |
332 |
322 and splitT 0 ([x], ys) = (x, ys) |
333 and splitT 0 ([x], ys) = (x, ys) |
323 | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) |
334 | splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) |
324 | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) |
335 | splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) |
336 else if nargs > n andalso not type_mode then |
347 else if nargs > n andalso not type_mode then |
337 astT (appT (splitT n ([c], args)), p) |
348 astT (appT (splitT n ([c], args)), p) |
338 else prnt (prnps, tbs); |
349 else prnt (prnps, tbs); |
339 in |
350 in |
340 (case token_trans a args of (*try token translation function*) |
351 (case token_trans a args of (*try token translation function*) |
341 SOME s_len => [Pretty.raw_str s_len] |
352 SOME s => [Pretty.raw_str s] |
342 | NONE => (*try print translation functions*) |
353 | NONE => (*try print translation functions*) |
343 astT (trans a (trf a) args, p) handle Match => prnt ([], tabs)) |
354 astT (trans a (trf a) args, p) handle Match => prnt ([], tabs)) |
344 end |
355 end |
345 |
356 |
346 and astT (c as Ast.Constant a, p) = combT (c, a, [], p) |
357 and astT (c as Ast.Constant a, p) = combT (c, a, [], p) |
351 in astT (ast0, p0) end; |
362 in astT (ast0, p0) end; |
352 |
363 |
353 |
364 |
354 (* pretty_term_ast *) |
365 (* pretty_term_ast *) |
355 |
366 |
356 fun pretty_term_ast context curried prtabs trf tokentrf ast = |
367 fun pretty_term_ast extern_const context curried prtabs trf tokentrf ast = |
357 Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode)) |
368 Pretty.blk (0, pretty extern_const context (mode_tabs prtabs (! print_mode)) |
358 trf tokentrf false curried ast 0); |
369 trf tokentrf false curried ast 0); |
359 |
370 |
360 |
371 |
361 (* pretty_typ_ast *) |
372 (* pretty_typ_ast *) |
362 |
373 |
363 fun pretty_typ_ast context _ prtabs trf tokentrf ast = |
374 fun pretty_typ_ast context _ prtabs trf tokentrf ast = |
364 Pretty.blk (0, pretty context (mode_tabs prtabs (! print_mode)) |
375 Pretty.blk (0, pretty I context (mode_tabs prtabs (! print_mode)) |
365 trf tokentrf true false ast 0); |
376 trf tokentrf true false ast 0); |
366 |
377 |
367 end; |
378 end; |