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