haftmann@28060
|
1 |
(* Title: Tools/code/code_printer.ML
|
haftmann@28060
|
2 |
Author: Florian Haftmann, TU Muenchen
|
haftmann@28060
|
3 |
|
haftmann@28060
|
4 |
Generic operations for pretty printing of target language code.
|
haftmann@28060
|
5 |
*)
|
haftmann@28060
|
6 |
|
haftmann@28060
|
7 |
signature CODE_PRINTER =
|
haftmann@28060
|
8 |
sig
|
haftmann@32908
|
9 |
type itype = Code_Thingol.itype
|
haftmann@32908
|
10 |
type iterm = Code_Thingol.iterm
|
haftmann@32908
|
11 |
type const = Code_Thingol.const
|
haftmann@32908
|
12 |
type dict = Code_Thingol.dict
|
haftmann@32908
|
13 |
|
haftmann@35228
|
14 |
val eqn_error: thm option -> string -> 'a
|
haftmann@28060
|
15 |
|
haftmann@28060
|
16 |
val @@ : 'a * 'a -> 'a list
|
haftmann@28060
|
17 |
val @| : 'a list * 'a -> 'a list
|
haftmann@28060
|
18 |
val str: string -> Pretty.T
|
haftmann@28060
|
19 |
val concat: Pretty.T list -> Pretty.T
|
haftmann@28060
|
20 |
val brackets: Pretty.T list -> Pretty.T
|
haftmann@34178
|
21 |
val enclose: string -> string -> Pretty.T list -> Pretty.T
|
haftmann@34178
|
22 |
val enum: string -> string -> string -> Pretty.T list -> Pretty.T
|
haftmann@34178
|
23 |
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
|
haftmann@28060
|
24 |
val semicolon: Pretty.T list -> Pretty.T
|
haftmann@33986
|
25 |
val doublesemicolon: Pretty.T list -> Pretty.T
|
haftmann@34178
|
26 |
val indent: int -> Pretty.T -> Pretty.T
|
haftmann@34071
|
27 |
val string_of_pretty: int -> Pretty.T -> string
|
haftmann@34071
|
28 |
val writeln_pretty: int -> Pretty.T -> unit
|
haftmann@28060
|
29 |
|
haftmann@30636
|
30 |
val first_upper: string -> string
|
haftmann@30636
|
31 |
val first_lower: string -> string
|
haftmann@30636
|
32 |
type var_ctxt
|
haftmann@30636
|
33 |
val make_vars: string list -> var_ctxt
|
haftmann@30636
|
34 |
val intro_vars: string list -> var_ctxt -> var_ctxt
|
haftmann@30636
|
35 |
val lookup_var: var_ctxt -> string -> string
|
haftmann@32913
|
36 |
val intro_base_names: (string -> bool) -> (string -> string)
|
haftmann@32913
|
37 |
-> string list -> var_ctxt -> var_ctxt
|
haftmann@32908
|
38 |
val aux_params: var_ctxt -> iterm list list -> string list
|
haftmann@30636
|
39 |
|
haftmann@31056
|
40 |
type literals
|
haftmann@31056
|
41 |
val Literals: { literal_char: string -> string, literal_string: string -> string,
|
haftmann@34931
|
42 |
literal_numeral: int -> string, literal_positive_numeral: int -> string,
|
haftmann@34931
|
43 |
literal_naive_numeral: int -> string,
|
haftmann@31056
|
44 |
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
|
haftmann@31056
|
45 |
-> literals
|
haftmann@31056
|
46 |
val literal_char: literals -> string -> string
|
haftmann@31056
|
47 |
val literal_string: literals -> string -> string
|
haftmann@34931
|
48 |
val literal_numeral: literals -> int -> string
|
haftmann@34931
|
49 |
val literal_positive_numeral: literals -> int -> string
|
haftmann@34931
|
50 |
val literal_naive_numeral: literals -> int -> string
|
haftmann@31056
|
51 |
val literal_list: literals -> Pretty.T list -> Pretty.T
|
haftmann@31056
|
52 |
val infix_cons: literals -> int * string
|
haftmann@31056
|
53 |
|
haftmann@28060
|
54 |
type lrx
|
haftmann@28060
|
55 |
val L: lrx
|
haftmann@28060
|
56 |
val R: lrx
|
haftmann@28060
|
57 |
val X: lrx
|
haftmann@28060
|
58 |
type fixity
|
haftmann@28060
|
59 |
val BR: fixity
|
haftmann@28060
|
60 |
val NOBR: fixity
|
haftmann@28060
|
61 |
val INFX: int * lrx -> fixity
|
haftmann@28060
|
62 |
val APP: fixity
|
haftmann@28060
|
63 |
val brackify: fixity -> Pretty.T list -> Pretty.T
|
haftmann@37239
|
64 |
val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
|
haftmann@31665
|
65 |
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
|
haftmann@34242
|
66 |
val applify: string -> string -> fixity -> Pretty.T -> Pretty.T list -> Pretty.T
|
haftmann@28060
|
67 |
|
haftmann@28060
|
68 |
type tyco_syntax
|
haftmann@34141
|
69 |
type simple_const_syntax
|
haftmann@34141
|
70 |
type proto_const_syntax
|
haftmann@28060
|
71 |
type const_syntax
|
haftmann@28060
|
72 |
val parse_infix: ('a -> 'b) -> lrx * int -> string
|
haftmann@28663
|
73 |
-> int * ((fixity -> 'b -> Pretty.T)
|
haftmann@28663
|
74 |
-> fixity -> 'a list -> Pretty.T)
|
wenzelm@36969
|
75 |
val parse_syntax: ('a -> 'b) -> Token.T list
|
haftmann@28663
|
76 |
-> (int * ((fixity -> 'b -> Pretty.T)
|
wenzelm@36969
|
77 |
-> fixity -> 'a list -> Pretty.T)) option * Token.T list
|
haftmann@34141
|
78 |
val simple_const_syntax: simple_const_syntax -> proto_const_syntax
|
haftmann@31056
|
79 |
val activate_const_syntax: theory -> literals
|
haftmann@31056
|
80 |
-> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
|
haftmann@35228
|
81 |
val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
|
haftmann@35228
|
82 |
-> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
|
haftmann@31056
|
83 |
-> (string -> const_syntax option)
|
haftmann@35228
|
84 |
-> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
|
haftmann@35228
|
85 |
val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
|
haftmann@35228
|
86 |
-> thm option -> fixity
|
haftmann@31889
|
87 |
-> iterm -> var_ctxt -> Pretty.T * var_ctxt
|
haftmann@28060
|
88 |
|
haftmann@30636
|
89 |
val mk_name_module: Name.context -> string option -> (string -> string option)
|
haftmann@30636
|
90 |
-> 'a Graph.T -> string -> string
|
haftmann@30636
|
91 |
val dest_name: string -> string * string
|
haftmann@28060
|
92 |
end;
|
haftmann@28060
|
93 |
|
haftmann@28060
|
94 |
structure Code_Printer : CODE_PRINTER =
|
haftmann@28060
|
95 |
struct
|
haftmann@28060
|
96 |
|
haftmann@28060
|
97 |
open Code_Thingol;
|
haftmann@28060
|
98 |
|
haftmann@35228
|
99 |
fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
|
haftmann@35228
|
100 |
| eqn_error NONE s = error s;
|
haftmann@28060
|
101 |
|
haftmann@34071
|
102 |
(** assembling and printing text pieces **)
|
haftmann@28060
|
103 |
|
haftmann@28060
|
104 |
infixr 5 @@;
|
haftmann@28060
|
105 |
infixr 5 @|;
|
haftmann@28060
|
106 |
fun x @@ y = [x, y];
|
haftmann@28060
|
107 |
fun xs @| y = xs @ [y];
|
wenzelm@37154
|
108 |
val str = Print_Mode.setmp [] Pretty.str;
|
haftmann@28060
|
109 |
val concat = Pretty.block o Pretty.breaks;
|
wenzelm@37154
|
110 |
fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
|
haftmann@34178
|
111 |
val brackets = enclose "(" ")" o Pretty.breaks;
|
wenzelm@37154
|
112 |
fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
|
haftmann@34178
|
113 |
fun enum_default default sep l r [] = str default
|
haftmann@34178
|
114 |
| enum_default default sep l r xs = enum sep l r xs;
|
haftmann@28060
|
115 |
fun semicolon ps = Pretty.block [concat ps, str ";"];
|
haftmann@33986
|
116 |
fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
|
wenzelm@37154
|
117 |
fun indent i = Print_Mode.setmp [] (Pretty.indent i);
|
haftmann@28060
|
118 |
|
wenzelm@37154
|
119 |
fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
|
wenzelm@37154
|
120 |
fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
|
haftmann@34071
|
121 |
|
haftmann@28060
|
122 |
|
haftmann@30636
|
123 |
(** names and variable name contexts **)
|
haftmann@30636
|
124 |
|
haftmann@30636
|
125 |
type var_ctxt = string Symtab.table * Name.context;
|
haftmann@30636
|
126 |
|
haftmann@30636
|
127 |
fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
|
haftmann@30636
|
128 |
Name.make_context names);
|
haftmann@30636
|
129 |
|
haftmann@30636
|
130 |
fun intro_vars names (namemap, namectxt) =
|
haftmann@30636
|
131 |
let
|
haftmann@30636
|
132 |
val (names', namectxt') = Name.variants names namectxt;
|
haftmann@30636
|
133 |
val namemap' = fold2 (curry Symtab.update) names names' namemap;
|
haftmann@30636
|
134 |
in (namemap', namectxt') end;
|
haftmann@30636
|
135 |
|
haftmann@30636
|
136 |
fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
|
haftmann@30636
|
137 |
of SOME name' => name'
|
haftmann@30636
|
138 |
| NONE => error ("Invalid name in context: " ^ quote name);
|
haftmann@30636
|
139 |
|
haftmann@30636
|
140 |
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
|
haftmann@30636
|
141 |
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
|
haftmann@30636
|
142 |
|
haftmann@32908
|
143 |
fun aux_params vars lhss =
|
haftmann@32908
|
144 |
let
|
haftmann@32908
|
145 |
fun fish_param _ (w as SOME _) = w
|
haftmann@32908
|
146 |
| fish_param (IVar (SOME v)) NONE = SOME v
|
haftmann@32908
|
147 |
| fish_param _ NONE = NONE;
|
haftmann@32908
|
148 |
fun fillup_param _ (_, SOME v) = v
|
haftmann@32908
|
149 |
| fillup_param x (i, NONE) = x ^ string_of_int i;
|
haftmann@32908
|
150 |
val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
|
haftmann@32908
|
151 |
val x = Name.variant (map_filter I fished1) "x";
|
haftmann@32908
|
152 |
val fished2 = map_index (fillup_param x) fished1;
|
haftmann@32908
|
153 |
val (fished3, _) = Name.variants fished2 Name.context;
|
haftmann@32908
|
154 |
val vars' = intro_vars fished3 vars;
|
haftmann@32908
|
155 |
in map (lookup_var vars') fished3 end;
|
haftmann@32908
|
156 |
|
haftmann@32913
|
157 |
fun intro_base_names no_syntax deresolve names = names
|
haftmann@32913
|
158 |
|> map_filter (fn name => if no_syntax name then
|
haftmann@32913
|
159 |
let val name' = deresolve name in
|
haftmann@32913
|
160 |
if Long_Name.is_qualified name' then NONE else SOME name'
|
haftmann@32913
|
161 |
end else NONE)
|
haftmann@32913
|
162 |
|> intro_vars;
|
haftmann@32913
|
163 |
|
haftmann@30636
|
164 |
|
haftmann@31056
|
165 |
(** pretty literals **)
|
haftmann@31056
|
166 |
|
haftmann@31056
|
167 |
datatype literals = Literals of {
|
haftmann@31056
|
168 |
literal_char: string -> string,
|
haftmann@31056
|
169 |
literal_string: string -> string,
|
haftmann@34931
|
170 |
literal_numeral: int -> string,
|
haftmann@34931
|
171 |
literal_positive_numeral: int -> string,
|
haftmann@34931
|
172 |
literal_naive_numeral: int -> string,
|
haftmann@31056
|
173 |
literal_list: Pretty.T list -> Pretty.T,
|
haftmann@31056
|
174 |
infix_cons: int * string
|
haftmann@31056
|
175 |
};
|
haftmann@31056
|
176 |
|
haftmann@31056
|
177 |
fun dest_Literals (Literals lits) = lits;
|
haftmann@31056
|
178 |
|
haftmann@31056
|
179 |
val literal_char = #literal_char o dest_Literals;
|
haftmann@31056
|
180 |
val literal_string = #literal_string o dest_Literals;
|
haftmann@31056
|
181 |
val literal_numeral = #literal_numeral o dest_Literals;
|
haftmann@34931
|
182 |
val literal_positive_numeral = #literal_positive_numeral o dest_Literals;
|
haftmann@34931
|
183 |
val literal_naive_numeral = #literal_naive_numeral o dest_Literals;
|
haftmann@31056
|
184 |
val literal_list = #literal_list o dest_Literals;
|
haftmann@31056
|
185 |
val infix_cons = #infix_cons o dest_Literals;
|
haftmann@31056
|
186 |
|
haftmann@31056
|
187 |
|
haftmann@28060
|
188 |
(** syntax printer **)
|
haftmann@28060
|
189 |
|
haftmann@28060
|
190 |
(* binding priorities *)
|
haftmann@28060
|
191 |
|
haftmann@28060
|
192 |
datatype lrx = L | R | X;
|
haftmann@28060
|
193 |
|
haftmann@28060
|
194 |
datatype fixity =
|
haftmann@28060
|
195 |
BR
|
haftmann@28060
|
196 |
| NOBR
|
haftmann@28060
|
197 |
| INFX of (int * lrx);
|
haftmann@28060
|
198 |
|
haftmann@28060
|
199 |
val APP = INFX (~1, L);
|
haftmann@28060
|
200 |
|
haftmann@28060
|
201 |
fun fixity_lrx L L = false
|
haftmann@28060
|
202 |
| fixity_lrx R R = false
|
haftmann@28060
|
203 |
| fixity_lrx _ _ = true;
|
haftmann@28060
|
204 |
|
haftmann@28060
|
205 |
fun fixity NOBR _ = false
|
haftmann@28060
|
206 |
| fixity _ NOBR = false
|
haftmann@33986
|
207 |
| fixity (INFX (pr, lr)) (INFX (print_ctxt, lr_ctxt)) =
|
haftmann@33986
|
208 |
pr < print_ctxt
|
haftmann@33986
|
209 |
orelse pr = print_ctxt
|
haftmann@28060
|
210 |
andalso fixity_lrx lr lr_ctxt
|
haftmann@33986
|
211 |
orelse print_ctxt = ~1
|
haftmann@28060
|
212 |
| fixity BR (INFX _) = false
|
haftmann@28060
|
213 |
| fixity _ _ = true;
|
haftmann@28060
|
214 |
|
haftmann@28060
|
215 |
fun gen_brackify _ [p] = p
|
haftmann@34178
|
216 |
| gen_brackify true (ps as _::_) = enclose "(" ")" ps
|
haftmann@28060
|
217 |
| gen_brackify false (ps as _::_) = Pretty.block ps;
|
haftmann@28060
|
218 |
|
haftmann@28060
|
219 |
fun brackify fxy_ctxt =
|
haftmann@28060
|
220 |
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
|
haftmann@28060
|
221 |
|
haftmann@37239
|
222 |
fun brackify_infix infx fxy_ctxt (l, m, r) =
|
haftmann@37239
|
223 |
(if fixity (INFX infx) fxy_ctxt then enclose "(" ")" else Pretty.block)
|
haftmann@37239
|
224 |
([l, str " ", m, Pretty.brk 1, r]);
|
haftmann@28060
|
225 |
|
haftmann@31665
|
226 |
fun brackify_block fxy_ctxt p1 ps p2 =
|
haftmann@31665
|
227 |
let val p = Pretty.block_enclose (p1, p2) ps
|
haftmann@31665
|
228 |
in if fixity BR fxy_ctxt
|
haftmann@34178
|
229 |
then enclose "(" ")" [p]
|
haftmann@31665
|
230 |
else p
|
haftmann@31665
|
231 |
end;
|
haftmann@31665
|
232 |
|
haftmann@34242
|
233 |
fun applify opn cls fxy_ctxt p [] = p
|
haftmann@34242
|
234 |
| applify opn cls fxy_ctxt p ps =
|
haftmann@34242
|
235 |
(if (fixity BR fxy_ctxt) then enclose "(" ")" else Pretty.block)
|
haftmann@34242
|
236 |
(p @@ enum "," opn cls ps);
|
haftmann@34242
|
237 |
|
haftmann@28060
|
238 |
|
haftmann@28060
|
239 |
(* generic syntax *)
|
haftmann@28060
|
240 |
|
haftmann@28060
|
241 |
type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
|
haftmann@28060
|
242 |
-> fixity -> itype list -> Pretty.T);
|
haftmann@34141
|
243 |
|
haftmann@34141
|
244 |
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
|
haftmann@34141
|
245 |
-> fixity -> (iterm * itype) list -> Pretty.T);
|
haftmann@31056
|
246 |
type proto_const_syntax = int * (string list * (literals -> string list
|
haftmann@31056
|
247 |
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
|
haftmann@35228
|
248 |
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
|
haftmann@34141
|
249 |
type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
|
haftmann@35228
|
250 |
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
|
haftmann@28060
|
251 |
|
haftmann@34163
|
252 |
fun simple_const_syntax syn =
|
haftmann@34163
|
253 |
apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
|
haftmann@28060
|
254 |
|
haftmann@31056
|
255 |
fun activate_const_syntax thy literals (n, (cs, f)) naming =
|
haftmann@31056
|
256 |
fold_map (Code_Thingol.ensure_declared_const thy) cs naming
|
haftmann@31056
|
257 |
|-> (fn cs' => pair (n, f literals cs'));
|
haftmann@31056
|
258 |
|
haftmann@37424
|
259 |
fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, function_typs)), ts)) =
|
haftmann@28060
|
260 |
case syntax_const c
|
haftmann@33986
|
261 |
of NONE => brackify fxy (print_app_expr thm vars app)
|
haftmann@33986
|
262 |
| SOME (k, print) =>
|
haftmann@28060
|
263 |
let
|
haftmann@37424
|
264 |
fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k function_typs);
|
haftmann@28060
|
265 |
in if k = length ts
|
haftmann@33986
|
266 |
then print' fxy ts
|
haftmann@28060
|
267 |
else if k < length ts
|
haftmann@28060
|
268 |
then case chop k ts of (ts1, ts2) =>
|
haftmann@33986
|
269 |
brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2)
|
haftmann@33986
|
270 |
else print_term thm vars fxy (Code_Thingol.eta_expand k app)
|
haftmann@28060
|
271 |
end;
|
haftmann@28060
|
272 |
|
haftmann@33986
|
273 |
fun gen_print_bind print_term thm (fxy : fixity) pat vars =
|
haftmann@28060
|
274 |
let
|
haftmann@31889
|
275 |
val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
|
haftmann@31873
|
276 |
val vars' = intro_vars vs vars;
|
haftmann@33986
|
277 |
in (print_term thm vars' fxy pat, vars') end;
|
haftmann@28060
|
278 |
|
haftmann@28060
|
279 |
|
haftmann@28060
|
280 |
(* mixfix syntax *)
|
haftmann@28060
|
281 |
|
haftmann@28060
|
282 |
datatype 'a mixfix =
|
haftmann@28060
|
283 |
Arg of fixity
|
haftmann@28060
|
284 |
| Pretty of Pretty.T;
|
haftmann@28060
|
285 |
|
haftmann@28060
|
286 |
fun mk_mixfix prep_arg (fixity_this, mfx) =
|
haftmann@28060
|
287 |
let
|
haftmann@28060
|
288 |
fun is_arg (Arg _) = true
|
haftmann@28060
|
289 |
| is_arg _ = false;
|
haftmann@28060
|
290 |
val i = (length o filter is_arg) mfx;
|
haftmann@28060
|
291 |
fun fillin _ [] [] =
|
haftmann@28060
|
292 |
[]
|
haftmann@33986
|
293 |
| fillin print (Arg fxy :: mfx) (a :: args) =
|
haftmann@33986
|
294 |
(print fxy o prep_arg) a :: fillin print mfx args
|
haftmann@33986
|
295 |
| fillin print (Pretty p :: mfx) args =
|
haftmann@33986
|
296 |
p :: fillin print mfx args;
|
haftmann@28060
|
297 |
in
|
haftmann@33986
|
298 |
(i, fn print => fn fixity_ctxt => fn args =>
|
haftmann@33986
|
299 |
gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
|
haftmann@28060
|
300 |
end;
|
haftmann@28060
|
301 |
|
haftmann@28060
|
302 |
fun parse_infix prep_arg (x, i) s =
|
haftmann@28060
|
303 |
let
|
haftmann@28060
|
304 |
val l = case x of L => INFX (i, L) | _ => INFX (i, X);
|
haftmann@28060
|
305 |
val r = case x of R => INFX (i, R) | _ => INFX (i, X);
|
haftmann@28060
|
306 |
in
|
haftmann@28060
|
307 |
mk_mixfix prep_arg (INFX (i, x),
|
haftmann@37239
|
308 |
[Arg l, (Pretty o str) " ", (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
|
haftmann@28060
|
309 |
end;
|
haftmann@28060
|
310 |
|
haftmann@28060
|
311 |
fun parse_mixfix prep_arg s =
|
haftmann@28060
|
312 |
let
|
haftmann@28060
|
313 |
val sym_any = Scan.one Symbol.is_regular;
|
haftmann@28060
|
314 |
val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
|
haftmann@28060
|
315 |
($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
|
haftmann@28060
|
316 |
|| ($$ "_" >> K (Arg BR))
|
haftmann@28060
|
317 |
|| ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
|
haftmann@28060
|
318 |
|| (Scan.repeat1
|
haftmann@28060
|
319 |
( $$ "'" |-- sym_any
|
haftmann@28060
|
320 |
|| Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
|
haftmann@28060
|
321 |
sym_any) >> (Pretty o str o implode)));
|
haftmann@28060
|
322 |
in case Scan.finite Symbol.stopper parse (Symbol.explode s)
|
haftmann@28060
|
323 |
of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
|
haftmann@28060
|
324 |
| ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
|
haftmann@28060
|
325 |
| _ => Scan.!!
|
haftmann@28060
|
326 |
(the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
|
haftmann@28060
|
327 |
end;
|
haftmann@28060
|
328 |
|
haftmann@28060
|
329 |
val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
|
haftmann@28060
|
330 |
|
haftmann@28060
|
331 |
fun parse_syntax prep_arg xs =
|
haftmann@28060
|
332 |
Scan.option ((
|
wenzelm@36970
|
333 |
((Parse.$$$ infixK >> K X)
|
wenzelm@36970
|
334 |
|| (Parse.$$$ infixlK >> K L)
|
wenzelm@36970
|
335 |
|| (Parse.$$$ infixrK >> K R))
|
wenzelm@36970
|
336 |
-- Parse.nat >> parse_infix prep_arg
|
haftmann@28060
|
337 |
|| Scan.succeed (parse_mixfix prep_arg))
|
wenzelm@36970
|
338 |
-- Parse.string
|
haftmann@28060
|
339 |
>> (fn (parse, s) => parse s)) xs;
|
haftmann@28060
|
340 |
|
wenzelm@36970
|
341 |
val _ = List.app Keyword.keyword [infixK, infixlK, infixrK];
|
haftmann@28060
|
342 |
|
haftmann@28064
|
343 |
|
haftmann@30636
|
344 |
(** module name spaces **)
|
haftmann@30636
|
345 |
|
haftmann@30636
|
346 |
val dest_name =
|
haftmann@30636
|
347 |
apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
|
haftmann@30636
|
348 |
|
haftmann@32924
|
349 |
fun mk_name_module reserved module_prefix module_alias program =
|
haftmann@30636
|
350 |
let
|
haftmann@30636
|
351 |
fun mk_alias name = case module_alias name
|
haftmann@30636
|
352 |
of SOME name' => name'
|
haftmann@30636
|
353 |
| NONE => name
|
haftmann@30636
|
354 |
|> Long_Name.explode
|
haftmann@32924
|
355 |
|> map (fn name => (the_single o fst) (Name.variants [name] reserved))
|
haftmann@30636
|
356 |
|> Long_Name.implode;
|
haftmann@30636
|
357 |
fun mk_prefix name = case module_prefix
|
haftmann@30636
|
358 |
of SOME module_prefix => Long_Name.append module_prefix name
|
haftmann@30636
|
359 |
| NONE => name;
|
haftmann@30636
|
360 |
val tab =
|
haftmann@30636
|
361 |
Symtab.empty
|
haftmann@30636
|
362 |
|> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
|
haftmann@30636
|
363 |
o fst o dest_name o fst)
|
haftmann@30636
|
364 |
program
|
haftmann@30636
|
365 |
in the o Symtab.lookup tab end;
|
haftmann@30636
|
366 |
|
haftmann@28060
|
367 |
end; (*struct*)
|