1 (* Title: Pure/ML/ml_compiler_polyml.ML |
|
2 Author: Makarius |
|
3 |
|
4 Runtime compilation and evaluation -- Poly/ML version. |
|
5 *) |
|
6 |
|
7 signature ML_COMPILER = |
|
8 sig |
|
9 type flags = |
|
10 {SML: bool, exchange: bool, redirect: bool, verbose: bool, |
|
11 debug: bool option, writeln: string -> unit, warning: string -> unit} |
|
12 val flags: flags |
|
13 val verbose: bool -> flags -> flags |
|
14 val eval: flags -> Position.T -> ML_Lex.token list -> unit |
|
15 end |
|
16 |
|
17 |
|
18 structure ML_Compiler: ML_COMPILER = |
|
19 struct |
|
20 |
|
21 (* flags *) |
|
22 |
|
23 type flags = |
|
24 {SML: bool, exchange: bool, redirect: bool, verbose: bool, |
|
25 debug: bool option, writeln: string -> unit, warning: string -> unit}; |
|
26 |
|
27 val flags: flags = |
|
28 {SML = false, exchange = false, redirect = false, verbose = false, |
|
29 debug = NONE, writeln = writeln, warning = warning}; |
|
30 |
|
31 fun verbose b (flags: flags) = |
|
32 {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, |
|
33 verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags}; |
|
34 |
|
35 |
|
36 (* parse trees *) |
|
37 |
|
38 fun breakpoint_position loc = |
|
39 let val pos = Position.reset_range (Exn_Properties.position_of loc) in |
|
40 (case Position.offset_of pos of |
|
41 NONE => pos |
|
42 | SOME 1 => pos |
|
43 | SOME j => |
|
44 Position.properties_of pos |
|
45 |> Properties.put (Markup.offsetN, Markup.print_int (j - 1)) |
|
46 |> Position.of_properties) |
|
47 end; |
|
48 |
|
49 fun report_parse_tree redirect depth space parse_tree = |
|
50 let |
|
51 val is_visible = |
|
52 (case Context.thread_data () of |
|
53 SOME context => Context_Position.is_visible_generic context |
|
54 | NONE => true); |
|
55 fun is_reported pos = is_visible andalso Position.is_reported pos; |
|
56 |
|
57 |
|
58 (* syntax reports *) |
|
59 |
|
60 fun reported_types loc types = |
|
61 let val pos = Exn_Properties.position_of loc in |
|
62 is_reported pos ? |
|
63 let |
|
64 val xml = |
|
65 ML_Name_Space.displayTypeExpression (types, depth, space) |
|
66 |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |
|
67 |> Output.output |> YXML.parse_body; |
|
68 in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end |
|
69 end; |
|
70 |
|
71 fun reported_entity kind loc decl = |
|
72 let |
|
73 val pos = Exn_Properties.position_of loc; |
|
74 val def_pos = Exn_Properties.position_of decl; |
|
75 in |
|
76 (is_reported pos andalso pos <> def_pos) ? |
|
77 let |
|
78 fun markup () = |
|
79 (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos); |
|
80 in cons (pos, markup, fn () => "") end |
|
81 end; |
|
82 |
|
83 fun reported_completions loc names = |
|
84 let val pos = Exn_Properties.position_of loc in |
|
85 if is_reported pos andalso not (null names) then |
|
86 let |
|
87 val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names); |
|
88 val xml = Completion.encode completion; |
|
89 in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end |
|
90 else I |
|
91 end; |
|
92 |
|
93 fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ()) |
|
94 | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ()) |
|
95 | reported loc (PolyML.PTtype types) = reported_types loc types |
|
96 | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl |
|
97 | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl |
|
98 | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl |
|
99 | reported loc pt = |
|
100 (case ML_Parse_Tree.completions pt of |
|
101 SOME names => reported_completions loc names |
|
102 | NONE => I) |
|
103 and reported_tree (loc, props) = fold (reported loc) props; |
|
104 |
|
105 val persistent_reports = reported_tree parse_tree []; |
|
106 |
|
107 fun output () = |
|
108 persistent_reports |
|
109 |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ())) |
|
110 |> Output.report; |
|
111 val _ = |
|
112 if not (null persistent_reports) andalso redirect andalso Multithreading.enabled () |
|
113 then |
|
114 Execution.print |
|
115 {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri} |
|
116 output |
|
117 else output (); |
|
118 |
|
119 |
|
120 (* breakpoints *) |
|
121 |
|
122 fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ()) |
|
123 | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ()) |
|
124 | breakpoints loc pt = |
|
125 (case ML_Parse_Tree.breakpoint pt of |
|
126 SOME b => |
|
127 let val pos = breakpoint_position loc in |
|
128 if is_reported pos then |
|
129 let val id = serial (); |
|
130 in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end |
|
131 else I |
|
132 end |
|
133 | NONE => I) |
|
134 and breakpoints_tree (loc, props) = fold (breakpoints loc) props; |
|
135 |
|
136 val all_breakpoints = rev (breakpoints_tree parse_tree []); |
|
137 val _ = Position.reports (map #1 all_breakpoints); |
|
138 val _ = |
|
139 if is_some (Context.thread_data ()) then |
|
140 Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints) |
|
141 else (); |
|
142 in () end; |
|
143 |
|
144 |
|
145 (* eval ML source tokens *) |
|
146 |
|
147 fun eval (flags: flags) pos toks = |
|
148 let |
|
149 val _ = Secure.secure_mltext (); |
|
150 val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}; |
|
151 val opt_context = Context.thread_data (); |
|
152 |
|
153 |
|
154 (* input *) |
|
155 |
|
156 val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos))); |
|
157 |
|
158 val input_explode = |
|
159 if #SML flags then String.explode |
|
160 else maps (String.explode o Symbol.esc) o Symbol.explode; |
|
161 |
|
162 val input_buffer = |
|
163 Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of))); |
|
164 |
|
165 fun get () = |
|
166 (case ! input_buffer of |
|
167 (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c) |
|
168 | ([], _) :: rest => (input_buffer := rest; SOME #" ") |
|
169 | [] => NONE); |
|
170 |
|
171 fun get_pos () = |
|
172 (case ! input_buffer of |
|
173 (_ :: _, tok) :: _ => ML_Lex.pos_of tok |
|
174 | ([], tok) :: _ => ML_Lex.end_pos_of tok |
|
175 | [] => Position.none); |
|
176 |
|
177 |
|
178 (* output *) |
|
179 |
|
180 val writeln_buffer = Unsynchronized.ref Buffer.empty; |
|
181 fun write s = Unsynchronized.change writeln_buffer (Buffer.add s); |
|
182 fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer))); |
|
183 |
|
184 val warnings = Unsynchronized.ref ([]: string list); |
|
185 fun warn msg = Unsynchronized.change warnings (cons msg); |
|
186 fun output_warnings () = List.app (#warning flags) (rev (! warnings)); |
|
187 |
|
188 val error_buffer = Unsynchronized.ref Buffer.empty; |
|
189 fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n"); |
|
190 fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer))); |
|
191 fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer)))); |
|
192 |
|
193 fun message {message = msg, hard, location = loc, context = _} = |
|
194 let |
|
195 val pos = Exn_Properties.position_of loc; |
|
196 val txt = |
|
197 (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ |
|
198 Pretty.string_of (Pretty.from_ML (pretty_ml msg)); |
|
199 in if hard then err txt else warn txt end; |
|
200 |
|
201 |
|
202 (* results *) |
|
203 |
|
204 val depth = ML_Options.get_print_depth (); |
|
205 |
|
206 fun apply_result {fixes, types, signatures, structures, functors, values} = |
|
207 let |
|
208 fun display disp x = |
|
209 if depth > 0 then |
|
210 (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n") |
|
211 else (); |
|
212 |
|
213 fun apply_fix (a, b) = |
|
214 (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b)); |
|
215 fun apply_type (a, b) = |
|
216 (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space)); |
|
217 fun apply_sig (a, b) = |
|
218 (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space)); |
|
219 fun apply_struct (a, b) = |
|
220 (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space)); |
|
221 fun apply_funct (a, b) = |
|
222 (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space)); |
|
223 fun apply_val (a, b) = |
|
224 (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space)); |
|
225 in |
|
226 List.app apply_fix fixes; |
|
227 List.app apply_type types; |
|
228 List.app apply_sig signatures; |
|
229 List.app apply_struct structures; |
|
230 List.app apply_funct functors; |
|
231 List.app apply_val values |
|
232 end; |
|
233 |
|
234 exception STATIC_ERRORS of unit; |
|
235 |
|
236 fun result_fun (phase1, phase2) () = |
|
237 ((case phase1 of |
|
238 NONE => () |
|
239 | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree); |
|
240 (case phase2 of |
|
241 NONE => raise STATIC_ERRORS () |
|
242 | SOME code => |
|
243 apply_result |
|
244 ((code |
|
245 |> Runtime.debugging opt_context |
|
246 |> Runtime.toplevel_error (err o Runtime.exn_message)) ()))); |
|
247 |
|
248 |
|
249 (* compiler invocation *) |
|
250 |
|
251 val debug = |
|
252 (case #debug flags of |
|
253 SOME debug => debug |
|
254 | NONE => ML_Options.debugger_enabled opt_context); |
|
255 |
|
256 val parameters = |
|
257 [PolyML.Compiler.CPOutStream write, |
|
258 PolyML.Compiler.CPNameSpace space, |
|
259 PolyML.Compiler.CPErrorMessageProc message, |
|
260 PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos), |
|
261 PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos), |
|
262 PolyML.Compiler.CPFileName location_props, |
|
263 PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth, |
|
264 PolyML.Compiler.CPCompilerResultFun result_fun, |
|
265 PolyML.Compiler.CPPrintInAlphabeticalOrder false] @ |
|
266 ML_Compiler_Parameters.debug debug; |
|
267 |
|
268 val _ = |
|
269 (while not (List.null (! input_buffer)) do |
|
270 PolyML.compiler (get, parameters) ()) |
|
271 handle exn => |
|
272 if Exn.is_interrupt exn then reraise exn |
|
273 else |
|
274 let |
|
275 val exn_msg = |
|
276 (case exn of |
|
277 STATIC_ERRORS () => "" |
|
278 | Runtime.TOPLEVEL_ERROR => "" |
|
279 | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised"); |
|
280 val _ = output_warnings (); |
|
281 val _ = output_writeln (); |
|
282 in raise_error exn_msg end; |
|
283 in |
|
284 if #verbose flags then (output_warnings (); flush_error (); output_writeln ()) |
|
285 else () |
|
286 end; |
|
287 |
|
288 end; |
|