author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5691  3a6de95c09d0 
child 6164  a0e9501d56f8 
permissions  rwrr 
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 = 

2384  9 
sig 
504
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

10 
val show_brackets: bool ref 
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

11 
val show_sorts: bool ref 
0  12 
val show_types: bool ref 
617  13 
val show_no_free_types: bool ref 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

14 
val print_mode: string list ref 
2384  15 
end; 
0  16 

17 
signature PRINTER = 

2384  18 
sig 
0  19 
include PRINTER0 
5691  20 
val term_to_ast: (string > (bool > typ > term list > term) list) > term > Ast.ast 
21 
val typ_to_ast: (string > (bool > typ > term list > term) list) > typ > Ast.ast 

22 
val sort_to_ast: (string > (bool > typ > term list > term) list) > sort > Ast.ast 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

23 
type prtabs 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

24 
val empty_prtabs: prtabs 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

25 
val extend_prtabs: prtabs > string > SynExt.xprod list > prtabs 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

26 
val merge_prtabs: prtabs > prtabs > prtabs 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

27 
val pretty_term_ast: bool > prtabs 
5691  28 
> (string > (Ast.ast list > Ast.ast) list) 
2701  29 
> (string > (string > string * int) option) > Ast.ast > Pretty.T 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

30 
val pretty_typ_ast: bool > prtabs 
5691  31 
> (string > (Ast.ast list > Ast.ast) list) 
2701  32 
> (string > (string > string * int) option) > Ast.ast > Pretty.T 
2384  33 
end; 
0  34 

2365  35 
structure Printer: PRINTER = 
0  36 
struct 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

37 

2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

38 

0  39 
(** options for printing **) 
40 

41 
val show_types = ref false; 

42 
val show_sorts = ref false; 

504
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset

43 
val show_brackets = ref false; 
617  44 
val show_no_free_types = ref false; 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

45 
val print_mode = ref ([]:string list); 
617  46 

0  47 

48 

2701  49 
(** misc utils **) 
50 

51 
(* apply print (ast) translation function *) 

0  52 

5691  53 
fun apply_first [] x = raise Match 
54 
 apply_first (f :: fs) x = f x handle Match => apply_first fs x; 

55 

56 
fun apply_trans name a fs args = 

57 
(apply_first fs args handle 

0  58 
Match => raise Match 
18  59 
 exn => (writeln ("Error in " ^ name ^ " for " ^ quote a); raise exn)); 
0  60 

5691  61 
fun apply_typed x y fs = map (fn f => f x y) fs; 
4147  62 

0  63 

2701  64 
(* simple_ast_of *) 
65 

5691  66 
fun simple_ast_of (Const (c, _)) = Ast.Constant c 
67 
 simple_ast_of (Free (x, _)) = Ast.Variable x 

68 
 simple_ast_of (Var (xi, _)) = Ast.Variable (Lexicon.string_of_vname xi) 

2701  69 
 simple_ast_of (t as _ $ _) = 
70 
let val (f, args) = strip_comb t in 

5691  71 
Ast.mk_appl (simple_ast_of f) (map simple_ast_of args) 
2701  72 
end 
5691  73 
 simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i) 
2701  74 
 simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs"; 
75 

76 

77 

3776  78 
(** sort_to_ast, typ_to_ast **) 
2701  79 

80 
fun ast_of_termT trf tm = 

0  81 
let 
5691  82 
(* FIXME improve: lookup token classes *) 
2701  83 
fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t 
84 
 ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t 

85 
 ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t 

86 
 ast_of (Const (a, _)) = trans a [] 

87 
 ast_of (t as _ $ _) = 

88 
(case strip_comb t of 

89 
(Const (a, _), args) => trans a args 

5691  90 
 (f, args) => Ast.Appl (map ast_of (f :: args))) 
91 
 ast_of t = simple_ast_of t 

2701  92 
and trans a args = 
5691  93 
ast_of (apply_trans "print translation" a (apply_typed false dummyT (trf a)) args) 
94 
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args); 

95 
in ast_of tm end; 

617  96 

5691  97 
fun sort_to_ast trf S = ast_of_termT trf (TypeExt.term_of_sort S); 
98 
fun typ_to_ast trf T = ast_of_termT trf (TypeExt.term_of_typ (! show_sorts) T); 

2701  99 

100 

101 

102 
(** term_to_ast **) 

103 

104 
fun mark_freevars (t $ u) = mark_freevars t $ mark_freevars u 

105 
 mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t) 

5691  106 
 mark_freevars (t as Free _) = Lexicon.const "_free" $ t 
107 
 mark_freevars (t as Var _) = Lexicon.const "_var" $ t 

2701  108 
 mark_freevars a = a; 
109 

110 
fun ast_of_term trf no_freeTs show_types show_sorts tm = 

111 
let 

0  112 
fun prune_typs (t_seen as (Const _, _)) = t_seen 
113 
 prune_typs (t as Free (x, ty), seen) = 

114 
if ty = dummyT then (t, seen) 

5691  115 
else if no_freeTs orelse t mem seen then (Lexicon.free x, seen) 
0  116 
else (t, t :: seen) 
117 
 prune_typs (t as Var (xi, ty), seen) = 

118 
if ty = dummyT then (t, seen) 

5691  119 
else if no_freeTs orelse t mem seen then (Lexicon.var xi, seen) 
0  120 
else (t, t :: seen) 
121 
 prune_typs (t_seen as (Bound _, _)) = t_seen 

122 
 prune_typs (Abs (x, ty, t), seen) = 

123 
let val (t', seen') = prune_typs (t, seen); 

124 
in (Abs (x, ty, t'), seen') end 

125 
 prune_typs (t1 $ t2, seen) = 

126 
let 

127 
val (t1', seen') = prune_typs (t1, seen); 

128 
val (t2', seen'') = prune_typs (t2, seen'); 

129 
in 

130 
(t1' $ t2', seen'') 

131 
end; 

132 

2701  133 
fun ast_of tm = 
134 
(case strip_comb tm of 

5691  135 
(t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts) 
2701  136 
 ((c as Const ("_free", _)), Free (x, T) :: ts) => 
5691  137 
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) 
2701  138 
 ((c as Const ("_bound", _)), Free (x, T) :: ts) => 
5691  139 
Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts) 
2701  140 
 ((c as Const ("_var", _)), Var (xi, T) :: ts) => 
5691  141 
Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts) 
2701  142 
 (Const (c, T), ts) => trans c T ts 
5691  143 
 (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts)) 
0  144 

2384  145 
and trans a T args = 
5691  146 
ast_of (apply_trans "print translation" a (apply_typed show_sorts T (trf a)) args) 
147 
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args) 

0  148 

2701  149 
and constrain t T = 
150 
if show_types andalso T <> dummyT then 

5691  151 
Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t, 
152 
ast_of_termT trf (TypeExt.term_of_typ show_sorts T)] 

2701  153 
else simple_ast_of t 
0  154 
in 
2701  155 
tm 
5691  156 
> SynTrans.prop_tr' 
2701  157 
> (if show_types then #1 o prune_typs o rpair [] else I) 
158 
> mark_freevars 

159 
> ast_of 

0  160 
end; 
161 

162 
fun term_to_ast trf tm = 

2701  163 
ast_of_term trf (! show_no_free_types) (! show_types orelse ! show_sorts) 
164 
(! show_sorts) tm; 

0  165 

166 

167 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

168 
(** type prtabs **) 
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 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

177 
type prtabs = (string * ((symb list * int * int) list) Symtab.table) list; 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

178 

3816  179 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

180 
(*find tab for mode*) 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

181 
fun get_tab prtabs mode = 
4487  182 
if_none (assoc (prtabs, mode)) Symtab.empty; 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

183 

2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

184 
(*collect tabs for mode hierarchy (default "")*) 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

185 
fun tabs_of prtabs modes = 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

186 
mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]); 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

187 

2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

188 
(*find formats in tab hierarchy*) 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

189 
fun get_fmts [] _ = [] 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

190 
 get_fmts (tab :: tabs) a = Symtab.lookup_multi (tab, a) @ get_fmts tabs a; 
18  191 

192 

3816  193 
(* xprod_to_fmt *) 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

194 

5691  195 
fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = None 
196 
 xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) = 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

197 
let 
2384  198 
fun cons_str s (String s' :: syms) = String (s ^ s') :: syms 
199 
 cons_str s syms = String s :: syms; 

200 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

201 
fun arg (s, p) = 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

202 
(if s = "type" then TypArg else Arg) 
5691  203 
(if Lexicon.is_terminal s then SynExt.max_pri else p); 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

204 

5691  205 
fun xsyms_to_syms (SynExt.Delim s :: xsyms) = 
4699  206 
apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms) 
5691  207 
 xsyms_to_syms (SynExt.Argument s_p :: xsyms) = 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

208 
apfst (cons (arg s_p)) (xsyms_to_syms xsyms) 
5691  209 
 xsyms_to_syms (SynExt.Space s :: xsyms) = 
4699  210 
apfst (cons_str (Symbol.output s)) (xsyms_to_syms xsyms) 
5691  211 
 xsyms_to_syms (SynExt.Bg i :: xsyms) = 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

212 
let 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

213 
val (bsyms, xsyms') = xsyms_to_syms xsyms; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

214 
val (syms, xsyms'') = xsyms_to_syms xsyms'; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

215 
in 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

216 
(Block (i, bsyms) :: syms, xsyms'') 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

217 
end 
5691  218 
 xsyms_to_syms (SynExt.Brk i :: xsyms) = 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

219 
apfst (cons (Break i)) (xsyms_to_syms xsyms) 
5691  220 
 xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms) 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

221 
 xsyms_to_syms [] = ([], []); 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

222 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

223 
fun nargs (Arg _ :: syms) = nargs syms + 1 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

224 
 nargs (TypArg _ :: syms) = nargs syms + 1 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

225 
 nargs (String _ :: syms) = nargs syms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

226 
 nargs (Break _ :: syms) = nargs syms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

227 
 nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

228 
 nargs [] = 0; 
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 
(case xsyms_to_syms xsymbs of 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

231 
(symbs, []) => Some (const, (symbs, nargs symbs, pri)) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

232 
 _ => sys_error "xprod_to_fmt: unbalanced blocks") 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

233 
end; 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

234 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

235 

a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

236 
(* empty, extend, merge prtabs *) 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

237 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

238 
val empty_prtabs = []; 
18  239 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

240 
fun extend_prtabs prtabs mode xprods = 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

241 
let 
3816  242 
val fmts = rev (mapfilter xprod_to_fmt xprods); 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

243 
val tab = get_tab prtabs mode; 
3816  244 
val new_tab = 
245 
if null fmts then tab 

246 
else Symtab.make_multi (fmts @ Symtab.dest_multi tab) (*prefer new entries*) 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

247 
in overwrite (prtabs, (mode, new_tab)) end; 
0  248 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

249 
fun merge_prtabs prtabs1 prtabs2 = 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

250 
let 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

251 
val modes = distinct (map fst (prtabs1 @ prtabs2)); 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

252 
fun merge mode = 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

253 
(mode, 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

254 
generic_merge (op =) Symtab.dest_multi Symtab.make_multi 
3816  255 
(get_tab prtabs2 mode) (get_tab prtabs1 mode)); (*prefer 2nd over 1st*) 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

256 
in 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

257 
map merge modes 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

258 
end; 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

259 

0  260 

261 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

262 
(** pretty term or typ asts **) 
0  263 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

264 
fun is_chain [Block (_, pr)] = is_chain pr 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

265 
 is_chain [Arg _] = true 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

266 
 is_chain _ = false; 
506
e0ca460d6e51
improved show_brackets again  Trueprop does not create () any more.
nipkow
parents:
505
diff
changeset

267 

2701  268 
fun pretty tabs trf tokentrf type_mode curried ast0 p0 = 
0  269 
let 
18  270 
val trans = apply_trans "print ast translation"; 
271 

5691  272 
fun token_trans c [Ast.Variable x] = 
2701  273 
(case tokentrf c of 
274 
None => None 

275 
 Some f => Some (f x)) 

276 
 token_trans _ _ = None; 

277 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

278 
(*default applications: prefix / postfix*) 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

279 
val appT = 
5691  280 
if type_mode then TypeExt.tappl_ast_tr' 
281 
else if curried then SynTrans.applC_ast_tr' 

282 
else SynTrans.appl_ast_tr'; 

18  283 

0  284 
fun synT ([], args) = ([], args) 
285 
 synT (Arg p :: symbs, t :: args) = 

18  286 
let val (Ts, args') = synT (symbs, args); 
0  287 
in (astT (t, p) @ Ts, args') end 
288 
 synT (TypArg p :: symbs, t :: args) = 

237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

289 
let 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

290 
val (Ts, args') = synT (symbs, args); 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

291 
in 
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

292 
if type_mode then (astT (t, p) @ Ts, args') 
2701  293 
else (pretty tabs trf tokentrf true curried t p @ Ts, args') 
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset

294 
end 
0  295 
 synT (String s :: symbs, args) = 
18  296 
let val (Ts, args') = synT (symbs, args); 
0  297 
in (Pretty.str s :: Ts, args') end 
298 
 synT (Block (i, bsymbs) :: symbs, args) = 

299 
let 

300 
val (bTs, args') = synT (bsymbs, args); 

301 
val (Ts, args'') = synT (symbs, args'); 

302 
in (Pretty.blk (i, bTs) :: Ts, args'') end 

303 
 synT (Break i :: symbs, args) = 

18  304 
let val (Ts, args') = synT (symbs, args); 
305 
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

306 
 synT (_ :: _, []) = sys_error "synT" 
0  307 

554  308 
and parT (pr, args, p, p': int) = #1 (synT 
309 
(if p > p' orelse 

5691  310 
(! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr)) 
554  311 
then [Block (1, String "(" :: pr @ [String ")"])] 
312 
else pr, args)) 

0  313 

314 
and prefixT (_, a, [], _) = [Pretty.str a] 

2384  315 
 prefixT (c, _, args, p) = 
5691  316 
if c = Ast.Constant "_appl" orelse c = Ast.Constant "_applC" then 
2507  317 
error "Syntax insufficient for printing prefix applications!" 
2384  318 
else astT (appT (c, args), p) 
0  319 

18  320 
and splitT 0 ([x], ys) = (x, ys) 
5691  321 
 splitT 0 (rev_xs, ys) = (Ast.Appl (rev rev_xs), ys) 
18  322 
 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

323 
 splitT _ _ = sys_error "splitT" 
18  324 

0  325 
and combT (tup as (c, a, args, p)) = 
326 
let 

327 
val nargs = length args; 

18  328 

2701  329 
(*find matching table entry, or print as prefix / postfix*) 
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

330 
fun prnt [] = prefixT tup 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

331 
 prnt ((pr, n, p') :: prnps) = 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

332 
if nargs = n then parT (pr, args, p, p') 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

333 
else if nargs > n andalso not type_mode then 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

334 
astT (appT (splitT n ([c], args)), p) 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

335 
else prnt prnps; 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

336 
in 
2701  337 
(case token_trans a args of (*try token translation function*) 
338 
Some (s, len) => [Pretty.strlen s len] 

5691  339 
 None => (*try print translation functions*) 
340 
astT (trans a (trf a) args, p) handle Match => prnt (get_fmts tabs a)) 

2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

341 
end 
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset

342 

5691  343 
and astT (c as Ast.Constant a, p) = combT (c, a, [], p) 
344 
 astT (Ast.Variable x, _) = [Pretty.str x] 

345 
 astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = 

18  346 
combT (c, a, args, p) 
5691  347 
 astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) 
348 
 astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]); 

0  349 
in 
350 
astT (ast0, p0) 

351 
end; 

352 

353 

354 
(* pretty_term_ast *) 

355 

2701  356 
fun pretty_term_ast curried prtabs trf tokentrf ast = 
357 
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) 

358 
trf tokentrf false curried ast 0); 

0  359 

360 

361 
(* pretty_typ_ast *) 

362 

2701  363 
fun pretty_typ_ast _ prtabs trf tokentrf ast = 
364 
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) 

365 
trf tokentrf true false ast 0); 

0  366 

367 
end; 