src/Pure/ML/ml_compiler_polyml.ML
author wenzelm
Sat Apr 19 17:23:05 2014 +0200 (2014-04-19)
changeset 56618 874bdedb2313
parent 56333 38f1422ef473
child 58991 92b6f4e68c5a
permissions -rw-r--r--
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
     1 (*  Title:      Pure/ML/ml_compiler_polyml.ML
     2     Author:     Makarius
     3 
     4 Runtime compilation and evaluation -- Poly/ML version.
     5 *)
     6 
     7 structure ML_Compiler: ML_COMPILER =
     8 struct
     9 
    10 open ML_Compiler;
    11 
    12 
    13 (* parse trees *)
    14 
    15 fun report_parse_tree redirect depth space parse_tree =
    16   let
    17     val is_visible =
    18       (case Context.thread_data () of
    19         SOME context => Context_Position.is_visible_generic context
    20       | NONE => true);
    21     fun is_reported pos = is_visible andalso Position.is_reported pos;
    22 
    23     fun reported_types loc types =
    24       let val pos = Exn_Properties.position_of loc in
    25         is_reported pos ?
    26           let
    27             val xml =
    28               PolyML.NameSpace.displayTypeExpression (types, depth, space)
    29               |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    30               |> Output.output |> YXML.parse_body;
    31           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
    32       end;
    33 
    34     fun reported_entity kind loc decl =
    35       let val pos = Exn_Properties.position_of loc in
    36         is_reported pos ?
    37           let
    38             val def_pos = Exn_Properties.position_of decl;
    39             fun markup () =
    40               (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    41           in cons (pos, markup, fn () => "") end
    42       end;
    43 
    44     fun reported loc (PolyML.PTtype types) = reported_types loc types
    45       | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
    46       | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
    47       | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
    48       | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    49       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    50       | reported _ _ = I
    51     and reported_tree (loc, props) = fold (reported loc) props;
    52 
    53     val persistent_reports = reported_tree parse_tree [];
    54 
    55     fun output () =
    56       persistent_reports
    57       |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
    58       |> Output.report;
    59   in
    60     if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
    61     then
    62       Execution.print
    63         {name = "ML_Compiler.report", pos = Position.thread_data (), pri = 1} output
    64     else output ()
    65   end;
    66 
    67 
    68 (* eval ML source tokens *)
    69 
    70 fun eval (flags: flags) pos toks =
    71   let
    72     val _ = Secure.secure_mltext ();
    73     val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}
    74     val opt_context = Context.thread_data ();
    75 
    76 
    77     (* input *)
    78 
    79     val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    80 
    81     val input_buffer =
    82       Unsynchronized.ref (toks |> map
    83         (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
    84 
    85     fun get () =
    86       (case ! input_buffer of
    87         (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
    88       | ([], _) :: rest => (input_buffer := rest; SOME #" ")
    89       | [] => NONE);
    90 
    91     fun get_pos () =
    92       (case ! input_buffer of
    93         (_ :: _, tok) :: _ => ML_Lex.pos_of tok
    94       | ([], tok) :: _ => ML_Lex.end_pos_of tok
    95       | [] => Position.none);
    96 
    97 
    98     (* output channels *)
    99 
   100     val writeln_buffer = Unsynchronized.ref Buffer.empty;
   101     fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
   102     fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));
   103 
   104     val warnings = Unsynchronized.ref ([]: string list);
   105     fun warn msg = Unsynchronized.change warnings (cons msg);
   106     fun output_warnings () = List.app warning (rev (! warnings));
   107 
   108     val error_buffer = Unsynchronized.ref Buffer.empty;
   109     fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
   110     fun flush_error () = writeln (Buffer.content (! error_buffer));
   111     fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
   112 
   113     fun message {message = msg, hard, location = loc, context = _} =
   114       let
   115         val pos = Exn_Properties.position_of loc;
   116         val txt =
   117           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   118           Pretty.string_of (Pretty.from_ML (pretty_ml msg));
   119       in if hard then err txt else warn txt end;
   120 
   121 
   122     (* results *)
   123 
   124     val depth = ML_Options.get_print_depth ();
   125 
   126     fun apply_result {fixes, types, signatures, structures, functors, values} =
   127       let
   128         fun display disp x =
   129           if depth > 0 then
   130             (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
   131           else ();
   132 
   133         fun apply_fix (a, b) =
   134           (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
   135         fun apply_type (a, b) =
   136           (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
   137         fun apply_sig (a, b) =
   138           (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
   139         fun apply_struct (a, b) =
   140           (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
   141         fun apply_funct (a, b) =
   142           (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
   143         fun apply_val (a, b) =
   144           (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
   145       in
   146         List.app apply_fix fixes;
   147         List.app apply_type types;
   148         List.app apply_sig signatures;
   149         List.app apply_struct structures;
   150         List.app apply_funct functors;
   151         List.app apply_val values
   152       end;
   153 
   154     exception STATIC_ERRORS of unit;
   155 
   156     fun result_fun (phase1, phase2) () =
   157      ((case phase1 of
   158         NONE => ()
   159       | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
   160       (case phase2 of
   161         NONE => raise STATIC_ERRORS ()
   162       | SOME code =>
   163           apply_result
   164             ((code
   165               |> Runtime.debugging opt_context
   166               |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
   167 
   168 
   169     (* compiler invocation *)
   170 
   171     val parameters =
   172      [PolyML.Compiler.CPOutStream write,
   173       PolyML.Compiler.CPNameSpace space,
   174       PolyML.Compiler.CPErrorMessageProc message,
   175       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
   176       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
   177       PolyML.Compiler.CPFileName location_props,
   178       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
   179       PolyML.Compiler.CPCompilerResultFun result_fun,
   180       PolyML.Compiler.CPPrintInAlphabeticalOrder false];
   181     val _ =
   182       (while not (List.null (! input_buffer)) do
   183         PolyML.compiler (get, parameters) ())
   184       handle exn =>
   185         if Exn.is_interrupt exn then reraise exn
   186         else
   187           let
   188             val exn_msg =
   189               (case exn of
   190                 STATIC_ERRORS () => ""
   191               | Runtime.TOPLEVEL_ERROR => ""
   192               | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
   193             val _ = output_warnings ();
   194             val _ = output_writeln ();
   195           in raise_error exn_msg end;
   196   in
   197     if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
   198     else ()
   199   end;
   200 
   201 end;
   202