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