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