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