src/Pure/ML/ml_compiler.ML
author wenzelm
Fri Dec 23 11:21:38 2016 +0100 (2016-12-23)
changeset 64660 ef85bb6491b3
parent 63806 c54a53ef1873
child 64661 84aea854dc3c
permissions -rw-r--r--
omit unused markup;
     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: 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: 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 = 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 = #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 
    40 fun 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 
    51 fun 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 ?
    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 Multithreading.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 
   152 fun 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     val input_buffer =
   177       Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
   178 
   179     fun get () =
   180       (case ! input_buffer of
   181         (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   182       | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   183       | [] => NONE);
   184 
   185     fun get_pos () =
   186       (case ! input_buffer of
   187         (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   188       | ([], tok) :: _ => ML_Lex.end_pos_of tok
   189       | [] => Position.none);
   190 
   191 
   192     (* output *)
   193 
   194     val writeln_buffer = Unsynchronized.ref Buffer.empty;
   195     fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
   196     fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
   197 
   198     val warnings = Unsynchronized.ref ([]: string list);
   199     fun warn msg = Unsynchronized.change warnings (cons msg);
   200     fun output_warnings () = List.app (#warning flags) (rev (! warnings));
   201 
   202     val error_buffer = Unsynchronized.ref Buffer.empty;
   203     fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
   204     fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
   205     fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
   206 
   207     fun message {message = msg, hard, location = loc, context = _} =
   208       let
   209         val pos = Exn_Properties.position_of_polyml_location loc;
   210         val txt =
   211           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   212           Pretty.string_of (Pretty.from_polyml msg);
   213       in if hard then err txt else warn txt end;
   214 
   215 
   216     (* results *)
   217 
   218     val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
   219 
   220     fun apply_result {fixes, types, signatures, structures, functors, values} =
   221       let
   222         fun display disp x =
   223           if depth > 0 then
   224             (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
   225           else ();
   226 
   227         fun apply_fix (a, b) =
   228           (#enterFix name_space (a, b);
   229             display PolyML.NameSpace.Infixes.print b);
   230         fun apply_type (a, b) =
   231           (#enterType name_space (a, b);
   232             display PolyML.NameSpace.TypeConstrs.print (b, depth, SOME name_space));
   233         fun apply_sig (a, b) =
   234           (#enterSig name_space (a, b);
   235             display PolyML.NameSpace.Signatures.print (b, depth, SOME name_space));
   236         fun apply_struct (a, b) =
   237           (#enterStruct name_space (a, b);
   238             display PolyML.NameSpace.Structures.print (b, depth, SOME name_space));
   239         fun apply_funct (a, b) =
   240           (#enterFunct name_space (a, b);
   241             display PolyML.NameSpace.Functors.print (b, depth, SOME name_space));
   242         fun apply_val (a, b) =
   243           (#enterVal name_space (a, b);
   244             display PolyML.NameSpace.Values.printWithType (b, depth, SOME name_space));
   245       in
   246         List.app apply_fix fixes;
   247         List.app apply_type types;
   248         List.app apply_sig signatures;
   249         List.app apply_struct structures;
   250         List.app apply_funct functors;
   251         List.app apply_val values
   252       end;
   253 
   254     exception STATIC_ERRORS of unit;
   255 
   256     fun result_fun (phase1, phase2) () =
   257      ((case phase1 of
   258         NONE => ()
   259       | SOME parse_tree =>
   260           add_breakpoints (report_parse_tree (#redirect flags) depth name_space parse_tree));
   261       (case phase2 of
   262         NONE => raise STATIC_ERRORS ()
   263       | SOME code =>
   264           apply_result
   265             ((code
   266               |> Runtime.debugging opt_context
   267               |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
   268 
   269 
   270     (* compiler invocation *)
   271 
   272     val parameters =
   273      [PolyML.Compiler.CPOutStream write,
   274       PolyML.Compiler.CPNameSpace name_space,
   275       PolyML.Compiler.CPErrorMessageProc message,
   276       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
   277       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
   278       PolyML.Compiler.CPFileName location_props,
   279       PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
   280       PolyML.Compiler.CPCompilerResultFun result_fun,
   281       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
   282       PolyML.Compiler.CPDebug debug,
   283       PolyML.Compiler.CPBindingSeq serial];
   284 
   285     val _ =
   286       (while not (List.null (! input_buffer)) do
   287         ML_Recursive.recursive env (fn () => PolyML.compiler (get, parameters) ()))
   288       handle exn =>
   289         if Exn.is_interrupt exn then Exn.reraise exn
   290         else
   291           let
   292             val exn_msg =
   293               (case exn of
   294                 STATIC_ERRORS () => ""
   295               | Runtime.TOPLEVEL_ERROR => ""
   296               | _ => "Exception- " ^ Pretty.string_of (Runtime.pretty_exn exn) ^ " raised");
   297             val _ = output_warnings ();
   298             val _ = output_writeln ();
   299           in raise_error exn_msg end;
   300   in
   301     if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   302     else ()
   303   end;
   304 
   305 end;