src/Pure/ML/ml_compiler_polyml-5.3.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 39231 25c345302a17
child 39240 a0c0698e56c0
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm@31333
     1
(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
wenzelm@31333
     2
    Author:     Makarius
wenzelm@31333
     3
wenzelm@33538
     4
Advanced runtime compilation for Poly/ML 5.3.0.
wenzelm@31333
     5
*)
wenzelm@31333
     6
wenzelm@31333
     7
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
     8
struct
wenzelm@31333
     9
wenzelm@31429
    10
(* source locations *)
wenzelm@31429
    11
wenzelm@31429
    12
fun position_of (loc: PolyML.location) =
wenzelm@31429
    13
  let
wenzelm@31429
    14
    val {file = text, startLine = line, startPosition = offset,
wenzelm@31429
    15
      endLine = end_line, endPosition = end_offset} = loc;
wenzelm@31429
    16
    val loc_props =
wenzelm@31434
    17
      (case YXML.parse text of
wenzelm@38228
    18
        XML.Elem ((e, atts), _) => if e = Markup.positionN then atts else []
wenzelm@31434
    19
      | XML.Text s => Position.file_name s);
wenzelm@31429
    20
  in
wenzelm@31429
    21
    Position.value Markup.lineN line @
wenzelm@31429
    22
    Position.value Markup.offsetN offset @
wenzelm@31429
    23
    Position.value Markup.end_lineN end_line @
wenzelm@31429
    24
    Position.value Markup.end_offsetN end_offset @
wenzelm@31429
    25
    loc_props
wenzelm@31429
    26
  end |> Position.of_properties;
wenzelm@31429
    27
wenzelm@31477
    28
fun exn_position exn =
wenzelm@31429
    29
  (case PolyML.exceptionLocation exn of
wenzelm@31429
    30
    NONE => Position.none
wenzelm@31429
    31
  | SOME loc => position_of loc);
wenzelm@31333
    32
wenzelm@38874
    33
val exn_messages = Runtime.exn_messages exn_position;
wenzelm@31477
    34
val exn_message = Runtime.exn_message exn_position;
wenzelm@31477
    35
wenzelm@31333
    36
wenzelm@31333
    37
(* parse trees *)
wenzelm@31333
    38
wenzelm@31429
    39
fun report_parse_tree depth space =
wenzelm@31333
    40
  let
wenzelm@38720
    41
    val report_text =
wenzelm@38720
    42
      (case Context.thread_data () of
wenzelm@38720
    43
        SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
wenzelm@38720
    44
      | _ => Position.report_text);
wenzelm@38720
    45
wenzelm@31475
    46
    fun report_decl markup loc decl =
wenzelm@38720
    47
      report_text Markup.ML_ref (position_of loc)
wenzelm@31475
    48
        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
wenzelm@31333
    49
    fun report loc (PolyML.PTtype types) =
wenzelm@31333
    50
          PolyML.NameSpace.displayTypeExpression (types, depth, space)
wenzelm@31333
    51
          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
wenzelm@38720
    52
          |> report_text Markup.ML_typing (position_of loc)
wenzelm@31475
    53
      | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
wenzelm@31475
    54
      | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
wenzelm@31475
    55
      | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
wenzelm@31333
    56
      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
wenzelm@31333
    57
      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
wenzelm@31333
    58
      | report _ _ = ()
wenzelm@31333
    59
    and report_tree (loc, props) = List.app (report loc) props;
wenzelm@31333
    60
  in report_tree end;
wenzelm@31333
    61
wenzelm@31333
    62
wenzelm@31333
    63
(* eval ML source tokens *)
wenzelm@31333
    64
wenzelm@31756
    65
val offset_of = the_default 0 o Position.offset_of;
wenzelm@31756
    66
wenzelm@31333
    67
fun eval verbose pos toks =
wenzelm@31333
    68
  let
wenzelm@31333
    69
    val _ = Secure.secure_mltext ();
wenzelm@39227
    70
    val space = ML_Env.name_space;
wenzelm@31333
    71
wenzelm@31333
    72
wenzelm@31333
    73
    (* input *)
wenzelm@31333
    74
wenzelm@31437
    75
    val location_props =
wenzelm@32492
    76
      op ^ (YXML.output_markup (Markup.position |> Markup.properties
wenzelm@32492
    77
            (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
wenzelm@31437
    78
wenzelm@31429
    79
    val input = toks |> maps (fn tok =>
wenzelm@31429
    80
      let
wenzelm@31429
    81
        val syms = Symbol.explode (ML_Lex.check_content_of tok);
wenzelm@31437
    82
        val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms
wenzelm@31437
    83
          (Position.reset_range (ML_Lex.pos_of tok));
wenzelm@31756
    84
      in
wenzelm@31756
    85
        (ps ~~ syms) |> maps (fn (p, sym) =>
wenzelm@31756
    86
          map (pair (offset_of p)) (String.explode (Symbol.esc sym)))
wenzelm@31756
    87
      end);
wenzelm@31333
    88
wenzelm@37209
    89
    val input_buffer = Unsynchronized.ref input;
wenzelm@32738
    90
    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
wenzelm@31333
    91
wenzelm@31756
    92
    fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
wenzelm@31333
    93
    fun get () =
wenzelm@31333
    94
      (case ! input_buffer of
wenzelm@31333
    95
        [] => NONE
wenzelm@31756
    96
      | (_, c) :: rest =>
wenzelm@31756
    97
          (input_buffer := rest;
wenzelm@31429
    98
           if c = #"\n" then line := ! line + 1 else ();
wenzelm@31333
    99
           SOME c));
wenzelm@31333
   100
wenzelm@31333
   101
wenzelm@39228
   102
    (* output channels *)
wenzelm@39228
   103
wenzelm@39228
   104
    val writeln_buffer = Unsynchronized.ref Buffer.empty;
wenzelm@39228
   105
    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
wenzelm@39228
   106
    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
wenzelm@39228
   107
wenzelm@39228
   108
    val warnings = Unsynchronized.ref ([]: string list);
wenzelm@39231
   109
    fun warn msg = Unsynchronized.change warnings (cons msg);
wenzelm@39228
   110
    fun output_warnings () = List.app warning (rev (! warnings));
wenzelm@39228
   111
wenzelm@39228
   112
    val error_buffer = Unsynchronized.ref Buffer.empty;
wenzelm@39231
   113
    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
wenzelm@39228
   114
    fun flush_error () = writeln (Buffer.content (! error_buffer));
wenzelm@39228
   115
    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
wenzelm@31333
   116
wenzelm@39228
   117
    fun message {message = msg, hard, location = loc, context = _} =
wenzelm@39228
   118
      let
wenzelm@39228
   119
        val pos = position_of loc;
wenzelm@39228
   120
        val txt =
wenzelm@39228
   121
          Markup.markup Markup.location
wenzelm@39228
   122
            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
wenzelm@39228
   123
          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
wenzelm@39228
   124
          Markup.markup (Position.report_markup pos) "";
wenzelm@39231
   125
      in if hard then err txt else warn txt end;
wenzelm@31333
   126
wenzelm@31333
   127
wenzelm@31333
   128
    (* results *)
wenzelm@31333
   129
wenzelm@31333
   130
    val depth = get_print_depth ();
wenzelm@31333
   131
wenzelm@31333
   132
    fun apply_result {fixes, types, signatures, structures, functors, values} =
wenzelm@31333
   133
      let
wenzelm@31333
   134
        fun display disp x =
wenzelm@31333
   135
          if depth > 0 then
wenzelm@39228
   136
            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
wenzelm@31333
   137
          else ();
wenzelm@31333
   138
wenzelm@31333
   139
        fun apply_fix (a, b) =
wenzelm@31333
   140
          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
wenzelm@31333
   141
        fun apply_type (a, b) =
wenzelm@31333
   142
          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
wenzelm@31333
   143
        fun apply_sig (a, b) =
wenzelm@31333
   144
          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
wenzelm@31333
   145
        fun apply_struct (a, b) =
wenzelm@31333
   146
          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
wenzelm@31333
   147
        fun apply_funct (a, b) =
wenzelm@31333
   148
          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
wenzelm@31333
   149
        fun apply_val (a, b) =
wenzelm@31333
   150
          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
wenzelm@31333
   151
      in
wenzelm@31333
   152
        List.app apply_fix fixes;
wenzelm@31333
   153
        List.app apply_type types;
wenzelm@31333
   154
        List.app apply_sig signatures;
wenzelm@31333
   155
        List.app apply_struct structures;
wenzelm@31333
   156
        List.app apply_funct functors;
wenzelm@31333
   157
        List.app apply_val values
wenzelm@31333
   158
      end;
wenzelm@31333
   159
wenzelm@39231
   160
    exception STATIC_ERRORS of unit;
wenzelm@39230
   161
wenzelm@31333
   162
    fun result_fun (phase1, phase2) () =
wenzelm@31477
   163
     ((case phase1 of
wenzelm@31477
   164
        NONE => ()
wenzelm@31477
   165
      | SOME parse_tree => report_parse_tree depth space parse_tree);
wenzelm@31477
   166
      (case phase2 of
wenzelm@39231
   167
        NONE => raise STATIC_ERRORS ()
wenzelm@31477
   168
      | SOME code =>
wenzelm@33603
   169
          apply_result
wenzelm@33603
   170
            ((code
wenzelm@33603
   171
              |> Runtime.debugging
wenzelm@39231
   172
              |> Runtime.toplevel_error (err o exn_message)) ())));
wenzelm@31333
   173
wenzelm@31333
   174
wenzelm@31333
   175
    (* compiler invocation *)
wenzelm@31333
   176
wenzelm@31333
   177
    val parameters =
wenzelm@39228
   178
     [PolyML.Compiler.CPOutStream write,
wenzelm@31333
   179
      PolyML.Compiler.CPNameSpace space,
wenzelm@39228
   180
      PolyML.Compiler.CPErrorMessageProc message,
wenzelm@31429
   181
      PolyML.Compiler.CPLineNo (fn () => ! line),
wenzelm@31475
   182
      PolyML.Compiler.CPLineOffset get_offset,
wenzelm@31437
   183
      PolyML.Compiler.CPFileName location_props,
wenzelm@31475
   184
      PolyML.Compiler.CPCompilerResultFun result_fun,
wenzelm@31475
   185
      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
wenzelm@31333
   186
    val _ =
wenzelm@31333
   187
      (while not (List.null (! input_buffer)) do
wenzelm@31333
   188
        PolyML.compiler (get, parameters) ())
wenzelm@39232
   189
      handle exn =>
wenzelm@39232
   190
        if Exn.is_interrupt exn then reraise exn
wenzelm@39232
   191
        else
wenzelm@39232
   192
          let
wenzelm@39232
   193
            val exn_msg =
wenzelm@39232
   194
              (case exn of
wenzelm@39232
   195
                STATIC_ERRORS () => ""
wenzelm@39232
   196
              | Runtime.TOPLEVEL_ERROR => ""
wenzelm@39232
   197
              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
wenzelm@39232
   198
            val _ = output_warnings ();
wenzelm@39232
   199
            val _ = output_writeln ();
wenzelm@39232
   200
          in raise_error exn_msg end;
wenzelm@39228
   201
  in
wenzelm@39228
   202
    if verbose then (output_warnings (); flush_error (); output_writeln ())
wenzelm@39228
   203
    else ()
wenzelm@39228
   204
  end;
wenzelm@31333
   205
wenzelm@31333
   206
end;
wenzelm@31333
   207