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