author | wenzelm |
Tue, 10 Dec 1996 13:00:52 +0100 | |
changeset 2365 | 38295260a740 |
parent 2229 | 64acb485ecce |
child 2384 | d360b395766e |
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 = |
|
1509 | 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 |
1509 | 15 |
end; |
0 | 16 |
|
17 |
signature PRINTER = |
|
1509 | 18 |
sig |
0 | 19 |
include PRINTER0 |
1509 | 20 |
val term_to_ast: (string -> (term list -> term) option) -> term -> Ast.ast |
21 |
val typ_to_ast: (string -> (term list -> term) option) -> typ -> Ast.ast |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
22 |
type prtabs |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
23 |
val prmodes_of: prtabs -> string list |
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 |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
28 |
-> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
29 |
val pretty_typ_ast: bool -> prtabs |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
30 |
-> (string -> (Ast.ast list -> Ast.ast) option) -> Ast.ast -> Pretty.T |
2365 | 31 |
val chartrans_of: prtabs -> (string * string) list |
1509 | 32 |
end; |
0 | 33 |
|
2365 | 34 |
structure Printer: PRINTER = |
0 | 35 |
struct |
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
36 |
|
1509 | 37 |
open Lexicon Ast SynExt TypeExt SynTrans; |
0 | 38 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
39 |
|
0 | 40 |
(** options for printing **) |
41 |
||
42 |
val show_types = ref false; |
|
43 |
val show_sorts = ref false; |
|
504
a4f09493d929
added flag show_brackets for printinmg fully bracketed terms.
nipkow
parents:
381
diff
changeset
|
44 |
val show_brackets = ref false; |
617 | 45 |
val show_no_free_types = ref false; |
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
46 |
val print_mode = ref ([]:string list); |
617 | 47 |
|
0 | 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 |
|
617 | 60 |
val no_freeTs = ! show_no_free_types; |
61 |
||
0 | 62 |
fun prune_typs (t_seen as (Const _, _)) = t_seen |
63 |
| prune_typs (t as Free (x, ty), seen) = |
|
64 |
if ty = dummyT then (t, seen) |
|
617 | 65 |
else if no_freeTs orelse t mem seen then (free x, seen) |
0 | 66 |
else (t, t :: seen) |
67 |
| prune_typs (t as Var (xi, ty), seen) = |
|
68 |
if ty = dummyT then (t, seen) |
|
617 | 69 |
else if no_freeTs orelse t mem seen then (var xi, seen) |
0 | 70 |
else (t, t :: seen) |
71 |
| prune_typs (t_seen as (Bound _, _)) = t_seen |
|
72 |
| prune_typs (Abs (x, ty, t), seen) = |
|
73 |
let val (t', seen') = prune_typs (t, seen); |
|
74 |
in (Abs (x, ty, t'), seen') end |
|
75 |
| prune_typs (t1 $ t2, seen) = |
|
76 |
let |
|
77 |
val (t1', seen') = prune_typs (t1, seen); |
|
78 |
val (t2', seen'') = prune_typs (t2, seen'); |
|
79 |
in |
|
80 |
(t1' $ t2', seen'') |
|
81 |
end; |
|
82 |
||
83 |
||
84 |
fun ast_of (Const (a, _)) = trans a [] |
|
554 | 85 |
| ast_of (Free (x, ty)) = constrain x (free x) ty |
86 |
| ast_of (Var (xi, ty)) = constrain (string_of_vname xi) (var xi) ty |
|
0 | 87 |
| ast_of (Bound i) = Variable ("B." ^ string_of_int i) |
88 |
| ast_of (t as Abs _) = ast_of (abs_tr' t) |
|
89 |
| ast_of (t as _ $ _) = |
|
90 |
(case strip_comb t of |
|
91 |
(Const (a, _), args) => trans a args |
|
92 |
| (f, args) => Appl (map ast_of (f :: args))) |
|
93 |
||
94 |
and trans a args = |
|
95 |
(case trf a of |
|
18 | 96 |
Some f => ast_of (apply_trans "print translation" a f args) |
0 | 97 |
| None => raise Match) |
98 |
handle Match => mk_appl (Constant a) (map ast_of args) |
|
99 |
||
100 |
and constrain x t ty = |
|
101 |
if show_types andalso ty <> dummyT then |
|
554 | 102 |
ast_of (const constrainC $ t $ term_of_typ show_sorts ty) |
0 | 103 |
else Variable x; |
104 |
in |
|
381 | 105 |
if show_types then |
106 |
ast_of (#1 (prune_typs (prop_tr' show_sorts tm, []))) |
|
107 |
else ast_of (prop_tr' show_sorts tm) |
|
0 | 108 |
end; |
109 |
||
110 |
||
111 |
(* term_to_ast *) |
|
112 |
||
113 |
fun term_to_ast trf tm = |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
114 |
ast_of_term trf (! show_types orelse ! show_sorts) (! show_sorts) tm; |
0 | 115 |
|
116 |
||
117 |
(* typ_to_ast *) |
|
118 |
||
119 |
fun typ_to_ast trf ty = |
|
120 |
ast_of_term trf false false (term_of_typ (! show_sorts) ty); |
|
121 |
||
122 |
||
123 |
||
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
124 |
(** type prtabs **) |
0 | 125 |
|
126 |
datatype symb = |
|
127 |
Arg of int | |
|
128 |
TypArg of int | |
|
129 |
String of string | |
|
130 |
Break of int | |
|
131 |
Block of int * symb list; |
|
132 |
||
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
133 |
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
|
134 |
|
2365 | 135 |
fun prmodes_of prtabs = filter_out (equal "") (map fst prtabs); |
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
136 |
|
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
137 |
(*find tab for mode*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
138 |
fun get_tab prtabs mode = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
139 |
if_none (assoc (prtabs, mode)) Symtab.null; |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
140 |
|
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
141 |
(*collect tabs for mode hierarchy (default "")*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
142 |
fun tabs_of prtabs modes = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
143 |
mapfilter (fn mode => assoc (prtabs, mode)) (modes @ [""]); |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
144 |
|
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
145 |
(*find formats in tab hierarchy*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
146 |
fun get_fmts [] _ = [] |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
147 |
| get_fmts (tab :: tabs) a = Symtab.lookup_multi (tab, a) @ get_fmts tabs a; |
18 | 148 |
|
149 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
150 |
(* xprods_to_fmts *) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
151 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
152 |
fun xprod_to_fmt (XProd (_, _, "", _)) = None |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
153 |
| xprod_to_fmt (XProd (_, xsymbs, const, pri)) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
154 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
155 |
fun arg (s, p) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
156 |
(if s = "type" then TypArg else Arg) |
506
e0ca460d6e51
improved show_brackets again - Trueprop does not create () any more.
nipkow
parents:
505
diff
changeset
|
157 |
(if is_terminal s then max_pri else p); |
237
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 xsyms_to_syms (Delim s :: xsyms) = |
2365 | 160 |
apfst (cons (String s)) (xsyms_to_syms xsyms) |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
161 |
| xsyms_to_syms (Argument s_p :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
162 |
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
|
163 |
| xsyms_to_syms (Space s :: xsyms) = |
2365 | 164 |
apfst (cons (String s)) (xsyms_to_syms xsyms) |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
165 |
| xsyms_to_syms (Bg i :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
166 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
167 |
val (bsyms, xsyms') = xsyms_to_syms xsyms; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
168 |
val (syms, xsyms'') = xsyms_to_syms xsyms'; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
169 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
170 |
(Block (i, bsyms) :: syms, xsyms'') |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
171 |
end |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
172 |
| xsyms_to_syms (Brk i :: xsyms) = |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
173 |
apfst (cons (Break i)) (xsyms_to_syms xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
174 |
| xsyms_to_syms (En :: xsyms) = ([], xsyms) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
175 |
| xsyms_to_syms [] = ([], []); |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
176 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
177 |
fun nargs (Arg _ :: syms) = nargs syms + 1 |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
178 |
| nargs (TypArg _ :: syms) = nargs syms + 1 |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
179 |
| nargs (String _ :: syms) = nargs syms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
180 |
| nargs (Break _ :: syms) = nargs syms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
181 |
| nargs (Block (_, bsyms) :: syms) = nargs syms + nargs bsyms |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
182 |
| nargs [] = 0; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
183 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
184 |
(case xsyms_to_syms xsymbs of |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
185 |
(symbs, []) => Some (const, (symbs, nargs symbs, pri)) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
186 |
| _ => sys_error "xprod_to_fmt: unbalanced blocks") |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
187 |
end; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
188 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
189 |
fun xprods_to_fmts xprods = mapfilter xprod_to_fmt xprods; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
190 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
191 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
192 |
(* empty, extend, merge prtabs *) |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
193 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
194 |
val empty_prtabs = []; |
18 | 195 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
196 |
fun extend_prtabs prtabs mode xprods = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
197 |
let |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
198 |
val fmts = xprods_to_fmts xprods; |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
199 |
val tab = get_tab prtabs mode; |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
200 |
val new_tab = generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab fmts; |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
201 |
in overwrite (prtabs, (mode, new_tab)) end; |
0 | 202 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
203 |
fun merge_prtabs prtabs1 prtabs2 = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
204 |
let |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
205 |
val modes = distinct (map fst (prtabs1 @ prtabs2)); |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
206 |
fun merge mode = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
207 |
(mode, |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
208 |
generic_merge (op =) Symtab.dest_multi Symtab.make_multi |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
209 |
(get_tab prtabs1 mode) (get_tab prtabs2 mode)); |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
210 |
in |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
211 |
map merge modes |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
212 |
end; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
213 |
|
0 | 214 |
|
215 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
216 |
(** pretty term or typ asts **) |
0 | 217 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
218 |
fun is_chain [Block (_, pr)] = is_chain pr |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
219 |
| is_chain [Arg _] = true |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
220 |
| is_chain _ = false; |
506
e0ca460d6e51
improved show_brackets again - Trueprop does not create () any more.
nipkow
parents:
505
diff
changeset
|
221 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
222 |
fun pretty tabs trf type_mode curried ast0 p0 = |
0 | 223 |
let |
18 | 224 |
val trans = apply_trans "print ast translation"; |
225 |
||
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
226 |
(*default applications: prefix / postfix*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
227 |
val appT = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
228 |
if type_mode then tappl_ast_tr' |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
229 |
else if curried then applC_ast_tr' |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
230 |
else appl_ast_tr'; |
18 | 231 |
|
0 | 232 |
fun synT ([], args) = ([], args) |
233 |
| synT (Arg p :: symbs, t :: args) = |
|
18 | 234 |
let val (Ts, args') = synT (symbs, args); |
0 | 235 |
in (astT (t, p) @ Ts, args') end |
236 |
| synT (TypArg p :: symbs, t :: args) = |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
237 |
let |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
238 |
val (Ts, args') = synT (symbs, args); |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
239 |
in |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
240 |
if type_mode then (astT (t, p) @ Ts, args') |
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
241 |
else (pretty tabs trf true curried t p @ Ts, args') |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
62
diff
changeset
|
242 |
end |
0 | 243 |
| synT (String s :: symbs, args) = |
18 | 244 |
let val (Ts, args') = synT (symbs, args); |
0 | 245 |
in (Pretty.str s :: Ts, args') end |
246 |
| synT (Block (i, bsymbs) :: symbs, args) = |
|
247 |
let |
|
248 |
val (bTs, args') = synT (bsymbs, args); |
|
249 |
val (Ts, args'') = synT (symbs, args'); |
|
250 |
in (Pretty.blk (i, bTs) :: Ts, args'') end |
|
251 |
| synT (Break i :: symbs, args) = |
|
18 | 252 |
let val (Ts, args') = synT (symbs, args); |
253 |
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
|
254 |
| synT (_ :: _, []) = sys_error "synT" |
0 | 255 |
|
554 | 256 |
and parT (pr, args, p, p': int) = #1 (synT |
257 |
(if p > p' orelse |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
258 |
(! show_brackets andalso p' <> max_pri andalso not (is_chain pr)) |
554 | 259 |
then [Block (1, String "(" :: pr @ [String ")"])] |
260 |
else pr, args)) |
|
0 | 261 |
|
262 |
and prefixT (_, a, [], _) = [Pretty.str a] |
|
263 |
| prefixT (c, _, args, p) = astT (appT (c, args), p) |
|
264 |
||
18 | 265 |
and splitT 0 ([x], ys) = (x, ys) |
266 |
| splitT 0 (rev_xs, ys) = (Appl (rev rev_xs), ys) |
|
267 |
| 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
|
268 |
| splitT _ _ = sys_error "splitT" |
18 | 269 |
|
0 | 270 |
and combT (tup as (c, a, args, p)) = |
271 |
let |
|
272 |
val nargs = length args; |
|
18 | 273 |
|
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
274 |
(*find matching table entry, or print as prefix/postfix*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
275 |
fun prnt [] = prefixT tup |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
276 |
| prnt ((pr, n, p') :: prnps) = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
astT (appT (splitT n ([c], args)), p) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
280 |
else prnt prnps; |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
281 |
in |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
282 |
(*try translation function first*) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
283 |
(case trf a of |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
284 |
None => prnt (get_fmts tabs a) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
285 |
| Some f => (astT (trans a f args, p) handle Match => prnt (get_fmts tabs a))) |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
286 |
end |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
287 |
|
0 | 288 |
and astT (c as Constant a, p) = combT (c, a, [], p) |
289 |
| astT (Variable x, _) = [Pretty.str x] |
|
18 | 290 |
| astT (Appl ((c as Constant a) :: (args as _ :: _)), p) = |
291 |
combT (c, a, args, p) |
|
0 | 292 |
| astT (Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p) |
18 | 293 |
| astT (ast as Appl _, _) = raise_ast "pretty: malformed ast" [ast]; |
0 | 294 |
in |
295 |
astT (ast0, p0) |
|
296 |
end; |
|
297 |
||
298 |
||
299 |
(* pretty_term_ast *) |
|
300 |
||
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
301 |
fun pretty_term_ast curried prtabs trf ast = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
302 |
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) trf false curried ast 0); |
0 | 303 |
|
304 |
||
305 |
(* pretty_typ_ast *) |
|
306 |
||
2200
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
307 |
fun pretty_typ_ast _ prtabs trf ast = |
2538977e94fa
added print_mode: string list ref (order of printer tables);
wenzelm
parents:
1509
diff
changeset
|
308 |
Pretty.blk (0, pretty (tabs_of prtabs (! print_mode)) trf true false ast 0); |
0 | 309 |
|
310 |
||
2365 | 311 |
|
312 |
(** character translations - generated from "symbols" syntax **) |
|
313 |
||
314 |
(* match_symbs *) |
|
315 |
||
316 |
(*match with symbs pattern, ignoring spaces, breaks, blocks*) |
|
317 |
||
318 |
local |
|
319 |
exception NO_MATCH; |
|
320 |
||
321 |
fun strip ((sym as Arg _) :: syms) = sym :: strip syms |
|
322 |
| strip (TypArg p :: syms) = Arg p :: strip syms |
|
323 |
| strip ((sym as String s) :: syms) = |
|
324 |
if forall is_blank (explode s) then strip syms |
|
325 |
else sym :: strip syms |
|
326 |
| strip (Break _ :: syms) = strip syms |
|
327 |
| strip (Block (_, bsyms) :: syms) = strip bsyms @ strip syms |
|
328 |
| strip [] = []; |
|
329 |
||
330 |
fun match (Arg p :: syms) (Arg p' :: syms') tr = |
|
331 |
if p = p' then match syms syms' tr |
|
332 |
else raise NO_MATCH |
|
333 |
| match (String s :: syms) (String s' :: syms') tr = |
|
334 |
if s = s' then match syms syms' tr |
|
335 |
else if size s = 1 then match syms syms' ((s, s') :: tr) |
|
336 |
else raise NO_MATCH |
|
337 |
| match [] [] tr = tr |
|
338 |
| match _ _ _ = raise NO_MATCH; |
|
339 |
in |
|
340 |
fun match_symbs (syms, n, p) (syms', n', p') = |
|
341 |
if n = n' andalso p = p' then |
|
342 |
match (strip syms) (strip syms') [] handle NO_MATCH => [] |
|
343 |
else [] |
|
0 | 344 |
end; |
2365 | 345 |
|
346 |
||
347 |
(* chartrans_of *) |
|
348 |
||
349 |
fun chartrans_of prtabs = |
|
350 |
let |
|
351 |
val def_tab = get_tab prtabs ""; |
|
352 |
val sym_tab = get_tab prtabs "symbols"; |
|
353 |
||
354 |
fun trans_of (c, symb) = |
|
355 |
flat (map (match_symbs symb) (Symtab.lookup_multi (def_tab, c))); |
|
356 |
in |
|
357 |
distinct (flat (map trans_of (Symtab.dest_multi sym_tab))) |
|
358 |
(* FIXME Symtab.make tr handle Symtab.DUPS cs |
|
359 |
=> error ("Ambiguous printer syntax of symbols: " ^ commas cs) *) |
|
360 |
end; |
|
361 |
||
362 |
||
363 |
end; |