author | wenzelm |
Thu, 03 Feb 1994 13:59:00 +0100 | |
changeset 258 | e540b7d4ecb1 |
parent 237 | a7d3e712767a |
child 381 | 8af09380c517 |
permissions | -rw-r--r-- |
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 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
18 |
structure SynExt: SYN_EXT |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
19 |
local open SynExt SynExt.Ast SynExt.Ast.Pretty in |
0 | 20 |
val term_to_ast: (string -> (term list -> term) option) -> term -> ast |
21 |
val typ_to_ast: (string -> (term list -> term) option) -> typ -> ast |
|
18 | 22 |
type prtab |
23 |
val empty_prtab: prtab |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
24 |
val extend_prtab: prtab -> xprod list -> prtab |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
25 |
val merge_prtabs: prtab -> prtab -> prtab |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
26 |
val pretty_term_ast: prtab -> (string -> (ast list -> ast) option) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
27 |
-> ast -> Pretty.T |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
28 |
val pretty_typ_ast: prtab -> (string -> (ast list -> ast) option) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
29 |
-> ast -> Pretty.T |
0 | 30 |
end |
31 |
end; |
|
32 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
33 |
functor PrinterFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
34 |
and SExtension: SEXTENSION sharing TypeExt.SynExt = SExtension.Parser.SynExt) |
258 | 35 |
: PRINTER = |
0 | 36 |
struct |
37 |
||
38 |
structure Symtab = Symtab; |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
39 |
structure SynExt = TypeExt.SynExt; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
40 |
open SExtension.Parser.Lexicon SynExt.Ast SynExt TypeExt SExtension; |
0 | 41 |
|
42 |
||
43 |
(** options for printing **) |
|
44 |
||
45 |
val show_types = ref false; |
|
46 |
val show_sorts = ref false; |
|
47 |
||
48 |
||
49 |
||
18 | 50 |
(** convert term or typ to ast **) |
0 | 51 |
|
18 | 52 |
fun apply_trans name a f args = |
53 |
(f args handle |
|
0 | 54 |
Match => raise Match |
18 | 55 |
| exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn)); |
0 | 56 |
|
57 |
||
58 |
fun ast_of_term trf show_types show_sorts tm = |
|
59 |
let |
|
18 | 60 |
fun aprop t = Const (apropC, dummyT) $ t; |
61 |
||
62 |
fun is_prop tys tm = |
|
62 | 63 |
fastype_of1 (tys, tm) = propT handle TERM _ => false; |
18 | 64 |
|
65 |
fun fix_aprop _ (tm as Const _) = tm |
|
66 |
| fix_aprop _ (tm as Free (x, ty)) = |
|
67 |
if ty = propT then aprop (Free (x, dummyT)) else tm |
|
68 |
| fix_aprop _ (tm as Var (xi, ty)) = |
|
69 |
if ty = propT then aprop (Var (xi, dummyT)) else tm |
|
70 |
| fix_aprop tys (tm as Bound _) = |
|
71 |
if is_prop tys tm then aprop tm else tm |
|
72 |
| fix_aprop tys (Abs (x, ty, t)) = Abs (x, ty, fix_aprop (ty :: tys) t) |
|
73 |
| fix_aprop tys (tm as t1 $ t2) = |
|
74 |
(if is_Const (head_of tm) orelse not (is_prop tys tm) |
|
75 |
then I else aprop) (fix_aprop tys t1 $ fix_aprop tys t2); |
|
76 |
||
0 | 77 |
|
78 |
fun prune_typs (t_seen as (Const _, _)) = t_seen |
|
79 |
| prune_typs (t as Free (x, ty), seen) = |
|
80 |
if ty = dummyT then (t, seen) |
|
81 |
else if t mem seen then (Free (x, dummyT), seen) |
|
82 |
else (t, t :: seen) |
|
83 |
| prune_typs (t as Var (xi, ty), seen) = |
|
84 |
if ty = dummyT then (t, seen) |
|
85 |
else if t mem seen then (Var (xi, dummyT), seen) |
|
86 |
else (t, t :: seen) |
|
87 |
| prune_typs (t_seen as (Bound _, _)) = t_seen |
|
88 |
| prune_typs (Abs (x, ty, t), seen) = |
|
89 |
let val (t', seen') = prune_typs (t, seen); |
|
90 |
in (Abs (x, ty, t'), seen') end |
|
91 |
| prune_typs (t1 $ t2, seen) = |
|
92 |
let |
|
93 |
val (t1', seen') = prune_typs (t1, seen); |
|
94 |
val (t2', seen'') = prune_typs (t2, seen'); |
|
95 |
in |
|
96 |
(t1' $ t2', seen'') |
|
97 |
end; |
|
98 |
||
99 |
||
100 |
fun ast_of (Const (a, _)) = trans a [] |
|
101 |
| ast_of (Free (x, ty)) = constrain x (Free (x, dummyT)) ty |
|
102 |
| ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (Var (xi, dummyT)) ty |
|
103 |
| ast_of (Bound i) = Variable ("B." ^ string_of_int i) |
|
104 |
| ast_of (t as Abs _) = ast_of (abs_tr' t) |
|
105 |
| ast_of (t as _ $ _) = |
|
106 |
(case strip_comb t of |
|
107 |
(Const (a, _), args) => trans a args |
|
108 |
| (f, args) => Appl (map ast_of (f :: args))) |
|
109 |
||
110 |
and trans a args = |
|
111 |
(case trf a of |
|
18 | 112 |
Some f => ast_of (apply_trans "print translation" a f args) |
0 | 113 |
| None => raise Match) |
114 |
handle Match => mk_appl (Constant a) (map ast_of args) |
|
115 |
||
116 |
and constrain x t ty = |
|
117 |
if show_types andalso ty <> dummyT then |
|
118 |
ast_of (Const (constrainC, dummyT) $ t $ term_of_typ show_sorts ty) |
|
119 |
else Variable x; |
|
120 |
in |
|
18 | 121 |
if show_types then ast_of (#1 (prune_typs (fix_aprop [] tm, []))) |
122 |
else ast_of (fix_aprop [] tm) |
|
0 | 123 |
end; |
124 |
||
125 |
||
126 |
(* term_to_ast *) |
|
127 |
||
128 |
fun term_to_ast trf tm = |
|
129 |
ast_of_term trf (! show_types) (! show_sorts) tm; |
|
130 |
||
131 |
||
132 |
(* typ_to_ast *) |
|
133 |
||
134 |
fun typ_to_ast trf ty = |
|
135 |
ast_of_term trf false false (term_of_typ (! show_sorts) ty); |
|
136 |
||
137 |
||
138 |
||
18 | 139 |
(** type prtab **) |
0 | 140 |
|
141 |
datatype symb = |
|
142 |
Arg of int | |
|
143 |
TypArg of int | |
|
144 |
String of string | |
|
145 |
Break of int | |
|
146 |
Block of int * symb list; |
|
147 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
148 |
type prtab = (symb list * int * int) Symtab.table; |
18 | 149 |
|
150 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
151 |
(* xprods_to_fmts *) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
152 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
153 |
fun xprod_to_fmt (XProd (_, _, "", _)) = None |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
154 |
| xprod_to_fmt (XProd (_, xsymbs, const, pri)) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
155 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
156 |
fun cons_str s (String s' :: syms) = String (s ^ s') :: syms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
157 |
| cons_str s syms = String s :: syms; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
158 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
159 |
fun arg (s, p) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
160 |
(if s = "type" then TypArg else Arg) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
161 |
(if is_terminal s then 1000 else p); (* FIXME 1000 vs. 0 vs. p (?) *) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
162 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
163 |
fun xsyms_to_syms (Delim s :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
164 |
apfst (cons_str s) (xsyms_to_syms xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
165 |
| xsyms_to_syms (Argument s_p :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
166 |
apfst (cons (arg s_p)) (xsyms_to_syms xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
167 |
| xsyms_to_syms (Space s :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
168 |
apfst (cons_str s) (xsyms_to_syms xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
169 |
| xsyms_to_syms (Bg i :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
170 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
171 |
val (bsyms, xsyms') = xsyms_to_syms xsyms; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
172 |
val (syms, xsyms'') = xsyms_to_syms xsyms'; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
173 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
174 |
(Block (i, bsyms) :: syms, xsyms'') |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
175 |
end |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
176 |
| xsyms_to_syms (Brk i :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
177 |
apfst (cons (Break i)) (xsyms_to_syms xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
178 |
| xsyms_to_syms (En :: xsyms) = ([], xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
179 |
| xsyms_to_syms [] = ([], []); |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
180 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
181 |
fun nargs (Arg _ :: syms) = nargs syms + 1 |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
182 |
| nargs (TypArg _ :: syms) = nargs syms + 1 |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
183 |
| nargs (String _ :: syms) = nargs syms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
184 |
| nargs (Break _ :: syms) = nargs syms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
185 |
| nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
186 |
| nargs [] = 0; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
187 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
188 |
(case xsyms_to_syms xsymbs of |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
189 |
(symbs, []) => Some (const, (symbs, nargs symbs, pri)) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
190 |
| _ => sys_error "xprod_to_fmt: unbalanced blocks") |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
191 |
end; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
192 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
193 |
fun xprods_to_fmts xprods = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
194 |
gen_distinct eq_fst (mapfilter xprod_to_fmt xprods); |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
195 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
196 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
197 |
(* empty, extend, merge prtabs *) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
198 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
199 |
fun err_dup_fmt c = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
200 |
sys_error ("duplicate fmt in prtab for " ^ quote c); |
18 | 201 |
|
202 |
val empty_prtab = Symtab.null; |
|
0 | 203 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
204 |
fun extend_prtab tab xprods = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
205 |
Symtab.extend (op =) (tab, xprods_to_fmts xprods) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
206 |
handle Symtab.DUPLICATE c => err_dup_fmt c; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
207 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
208 |
fun merge_prtabs tab1 tab2 = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
209 |
Symtab.merge (op =) (tab1, tab2) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
210 |
handle Symtab.DUPLICATE c => err_dup_fmt c; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
211 |
|
0 | 212 |
|
213 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
214 |
(** pretty term or typ asts **) |
0 | 215 |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
216 |
fun pretty prtab trf type_mode ast0 p0 = |
0 | 217 |
let |
18 | 218 |
val trans = apply_trans "print ast translation"; |
219 |
||
220 |
val appT = if type_mode then tappl_ast_tr' else appl_ast_tr'; |
|
221 |
||
0 | 222 |
fun synT ([], args) = ([], args) |
223 |
| synT (Arg p :: symbs, t :: args) = |
|
18 | 224 |
let val (Ts, args') = synT (symbs, args); |
0 | 225 |
in (astT (t, p) @ Ts, args') end |
226 |
| synT (TypArg p :: symbs, t :: args) = |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
227 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
228 |
val (Ts, args') = synT (symbs, args); |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
229 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
230 |
if type_mode then (astT (t, p) @ Ts, args') |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
231 |
else (pretty prtab trf true t p @ Ts, args') |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
232 |
end |
0 | 233 |
| synT (String s :: symbs, args) = |
18 | 234 |
let val (Ts, args') = synT (symbs, args); |
0 | 235 |
in (Pretty.str s :: Ts, args') end |
236 |
| synT (Block (i, bsymbs) :: symbs, args) = |
|
237 |
let |
|
238 |
val (bTs, args') = synT (bsymbs, args); |
|
239 |
val (Ts, args'') = synT (symbs, args'); |
|
240 |
in (Pretty.blk (i, bTs) :: Ts, args'') end |
|
241 |
| synT (Break i :: symbs, args) = |
|
18 | 242 |
let val (Ts, args') = synT (symbs, args); |
243 |
in ((if i < 0 then Pretty.fbrk else Pretty.brk i) :: Ts, args') end |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
244 |
| synT (_ :: _, []) = sys_error "synT" |
0 | 245 |
|
246 |
and parT (pr, args, p, p': int) = |
|
18 | 247 |
if p > p' then |
248 |
#1 (synT ([Block (1, String "(" :: pr @ [String ")"])], args)) |
|
249 |
else #1 (synT (pr, args)) |
|
0 | 250 |
|
251 |
and prefixT (_, a, [], _) = [Pretty.str a] |
|
252 |
| prefixT (c, _, args, p) = astT (appT (c, args), p) |
|
253 |
||
18 | 254 |
and splitT 0 ([x], ys) = (x, ys) |
255 |
| splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys) |
|
256 |
| splitT n (rev_xs, y :: ys) = splitT (n - 1) (y :: rev_xs, ys) |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
257 |
| splitT _ _ = sys_error "splitT" |
18 | 258 |
|
0 | 259 |
and combT (tup as (c, a, args, p)) = |
260 |
let |
|
261 |
val nargs = length args; |
|
18 | 262 |
|
0 | 263 |
fun prnt (pr, n, p') = |
18 | 264 |
if nargs = n then parT (pr, args, p, p') |
265 |
else if nargs < n orelse type_mode then prefixT tup |
|
266 |
else astT (appT (splitT n ([c], args)), p); |
|
0 | 267 |
in |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
268 |
(case (trf a, Symtab.lookup (prtab, a)) of |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
269 |
(None, None) => prefixT tup |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
270 |
| (None, Some prnp) => prnt prnp |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
271 |
| (Some f, None) => |
18 | 272 |
(astT (trans a f args, p) handle Match => prefixT tup) |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
273 |
| (Some f, Some prnp) => |
18 | 274 |
(astT (trans a f args, p) handle Match => prnt prnp)) |
0 | 275 |
end |
276 |
||
277 |
and astT (c as Constant a, p) = combT (c, a, [], p) |
|
278 |
| astT (Variable x, _) = [Pretty.str x] |
|
18 | 279 |
| astT (Appl ((c as Constant a) :: (args as _ :: _)), p) = |
280 |
combT (c, a, args, p) |
|
0 | 281 |
| astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) |
18 | 282 |
| astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast]; |
0 | 283 |
in |
284 |
astT (ast0, p0) |
|
285 |
end; |
|
286 |
||
287 |
||
288 |
(* pretty_term_ast *) |
|
289 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
290 |
fun pretty_term_ast prtab trf ast = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
291 |
Pretty.blk (0, pretty prtab trf false ast 0); |
0 | 292 |
|
293 |
||
294 |
(* pretty_typ_ast *) |
|
295 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
296 |
fun pretty_typ_ast prtab trf ast = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
297 |
Pretty.blk (0, pretty prtab trf true ast 0); |
0 | 298 |
|
299 |
||
300 |
end; |
|
301 |