src/Pure/ML/ml_compiler_polyml-5.3.ML
author wenzelm
Mon Nov 09 21:30:54 2009 +0100 (2009-11-09)
changeset 33538 edf497b5b5d2
parent 32738 15bb09ca0378
child 33603 3713a5208671
permissions -rw-r--r--
setup for official Poly/ML 5.3.0, which is now the default;
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
signature ML_COMPILER =
wenzelm@31333
     8
sig
wenzelm@31477
     9
  val exn_position: exn -> Position.T
wenzelm@31477
    10
  val exn_message: exn -> string
wenzelm@31333
    11
  val eval: bool -> Position.T -> ML_Lex.token list -> unit
wenzelm@31333
    12
end
wenzelm@31333
    13
wenzelm@31333
    14
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
    15
struct
wenzelm@31333
    16
wenzelm@31429
    17
(* source locations *)
wenzelm@31429
    18
wenzelm@31429
    19
fun position_of (loc: PolyML.location) =
wenzelm@31429
    20
  let
wenzelm@31429
    21
    val {file = text, startLine = line, startPosition = offset,
wenzelm@31429
    22
      endLine = end_line, endPosition = end_offset} = loc;
wenzelm@31429
    23
    val loc_props =
wenzelm@31434
    24
      (case YXML.parse text of
wenzelm@31434
    25
        XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []
wenzelm@31434
    26
      | XML.Text s => Position.file_name s);
wenzelm@31429
    27
  in
wenzelm@31429
    28
    Position.value Markup.lineN line @
wenzelm@31429
    29
    Position.value Markup.offsetN offset @
wenzelm@31429
    30
    Position.value Markup.end_lineN end_line @
wenzelm@31429
    31
    Position.value Markup.end_offsetN end_offset @
wenzelm@31429
    32
    loc_props
wenzelm@31429
    33
  end |> Position.of_properties;
wenzelm@31429
    34
wenzelm@31477
    35
fun exn_position exn =
wenzelm@31429
    36
  (case PolyML.exceptionLocation exn of
wenzelm@31429
    37
    NONE => Position.none
wenzelm@31429
    38
  | SOME loc => position_of loc);
wenzelm@31333
    39
wenzelm@31477
    40
val exn_message = Runtime.exn_message exn_position;
wenzelm@31477
    41
wenzelm@31333
    42
wenzelm@31333
    43
(* parse trees *)
wenzelm@31333
    44
wenzelm@31429
    45
fun report_parse_tree depth space =
wenzelm@31333
    46
  let
wenzelm@31475
    47
    fun report_decl markup loc decl =
wenzelm@31475
    48
      Position.report_text Markup.ML_ref (position_of loc)
wenzelm@31475
    49
        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
wenzelm@31333
    50
    fun report loc (PolyML.PTtype types) =
wenzelm@31333
    51
          PolyML.NameSpace.displayTypeExpression (types, depth, space)
wenzelm@31333
    52
          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
wenzelm@31429
    53
          |> Position.report_text Markup.ML_typing (position_of loc)
wenzelm@31475
    54
      | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
wenzelm@31475
    55
      | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
wenzelm@31475
    56
      | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
wenzelm@31333
    57
      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
wenzelm@31333
    58
      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
wenzelm@31333
    59
      | report _ _ = ()
wenzelm@31333
    60
    and report_tree (loc, props) = List.app (report loc) props;
wenzelm@31333
    61
  in report_tree end;
wenzelm@31333
    62
wenzelm@31333
    63
wenzelm@31333
    64
(* eval ML source tokens *)
wenzelm@31333
    65
wenzelm@31756
    66
val offset_of = the_default 0 o Position.offset_of;
wenzelm@31756
    67
wenzelm@31333
    68
fun eval verbose pos toks =
wenzelm@31333
    69
  let
wenzelm@31333
    70
    val _ = Secure.secure_mltext ();
wenzelm@31333
    71
    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
wenzelm@31333
    72
wenzelm@31333
    73
wenzelm@31333
    74
    (* input *)
wenzelm@31333
    75
wenzelm@31437
    76
    val location_props =
wenzelm@32492
    77
      op ^ (YXML.output_markup (Markup.position |> Markup.properties
wenzelm@32492
    78
            (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))));
wenzelm@31437
    79
wenzelm@31429
    80
    val input = toks |> maps (fn tok =>
wenzelm@31429
    81
      let
wenzelm@31429
    82
        val syms = Symbol.explode (ML_Lex.check_content_of tok);
wenzelm@31437
    83
        val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms
wenzelm@31437
    84
          (Position.reset_range (ML_Lex.pos_of tok));
wenzelm@31756
    85
      in
wenzelm@31756
    86
        (ps ~~ syms) |> maps (fn (p, sym) =>
wenzelm@31756
    87
          map (pair (offset_of p)) (String.explode (Symbol.esc sym)))
wenzelm@31756
    88
      end);
wenzelm@31333
    89
wenzelm@31475
    90
    val end_pos =
wenzelm@31475
    91
      if null toks then Position.none
wenzelm@31475
    92
      else ML_Lex.end_pos_of (List.last toks);
wenzelm@31475
    93
wenzelm@32738
    94
    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
wenzelm@32738
    95
    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
wenzelm@31333
    96
wenzelm@31756
    97
    fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
wenzelm@31333
    98
    fun get () =
wenzelm@31333
    99
      (case ! input_buffer of
wenzelm@31333
   100
        [] => NONE
wenzelm@31756
   101
      | (_, c) :: rest =>
wenzelm@31756
   102
          (input_buffer := rest;
wenzelm@31429
   103
           if c = #"\n" then line := ! line + 1 else ();
wenzelm@31333
   104
           SOME c));
wenzelm@31333
   105
wenzelm@31333
   106
wenzelm@31333
   107
    (* output *)
wenzelm@31333
   108
wenzelm@32738
   109
    val output_buffer = Unsynchronized.ref Buffer.empty;
wenzelm@31333
   110
    fun output () = Buffer.content (! output_buffer);
wenzelm@32738
   111
    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
wenzelm@31333
   112
wenzelm@31333
   113
    fun put_message {message, hard, location, context = _} =
wenzelm@32490
   114
     (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");
wenzelm@32490
   115
      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)) ^ "\n"));
wenzelm@31333
   116
wenzelm@31333
   117
wenzelm@31333
   118
    (* results *)
wenzelm@31333
   119
wenzelm@31333
   120
    val depth = get_print_depth ();
wenzelm@31333
   121
wenzelm@31333
   122
    fun apply_result {fixes, types, signatures, structures, functors, values} =
wenzelm@31333
   123
      let
wenzelm@31333
   124
        fun display disp x =
wenzelm@31333
   125
          if depth > 0 then
wenzelm@31333
   126
            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
wenzelm@31333
   127
          else ();
wenzelm@31333
   128
wenzelm@31333
   129
        fun apply_fix (a, b) =
wenzelm@31333
   130
          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
wenzelm@31333
   131
        fun apply_type (a, b) =
wenzelm@31333
   132
          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
wenzelm@31333
   133
        fun apply_sig (a, b) =
wenzelm@31333
   134
          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
wenzelm@31333
   135
        fun apply_struct (a, b) =
wenzelm@31333
   136
          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
wenzelm@31333
   137
        fun apply_funct (a, b) =
wenzelm@31333
   138
          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
wenzelm@31333
   139
        fun apply_val (a, b) =
wenzelm@31333
   140
          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
wenzelm@31333
   141
      in
wenzelm@31333
   142
        List.app apply_fix fixes;
wenzelm@31333
   143
        List.app apply_type types;
wenzelm@31333
   144
        List.app apply_sig signatures;
wenzelm@31333
   145
        List.app apply_struct structures;
wenzelm@31333
   146
        List.app apply_funct functors;
wenzelm@31333
   147
        List.app apply_val values
wenzelm@31333
   148
      end;
wenzelm@31333
   149
wenzelm@31333
   150
    fun result_fun (phase1, phase2) () =
wenzelm@31477
   151
     ((case phase1 of
wenzelm@31477
   152
        NONE => ()
wenzelm@31477
   153
      | SOME parse_tree => report_parse_tree depth space parse_tree);
wenzelm@31477
   154
      (case phase2 of
wenzelm@31477
   155
        NONE => err "Static Errors"
wenzelm@31477
   156
      | SOME code =>
wenzelm@31477
   157
          apply_result ((code |> Runtime.debugging |> Runtime.toplevel_error exn_message) ())));
wenzelm@31333
   158
wenzelm@31333
   159
wenzelm@31333
   160
    (* compiler invocation *)
wenzelm@31333
   161
wenzelm@31333
   162
    val parameters =
wenzelm@31333
   163
     [PolyML.Compiler.CPOutStream put,
wenzelm@31333
   164
      PolyML.Compiler.CPNameSpace space,
wenzelm@31333
   165
      PolyML.Compiler.CPErrorMessageProc put_message,
wenzelm@31429
   166
      PolyML.Compiler.CPLineNo (fn () => ! line),
wenzelm@31475
   167
      PolyML.Compiler.CPLineOffset get_offset,
wenzelm@31437
   168
      PolyML.Compiler.CPFileName location_props,
wenzelm@31475
   169
      PolyML.Compiler.CPCompilerResultFun result_fun,
wenzelm@31475
   170
      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
wenzelm@31333
   171
    val _ =
wenzelm@31333
   172
      (while not (List.null (! input_buffer)) do
wenzelm@31333
   173
        PolyML.compiler (get, parameters) ())
wenzelm@31333
   174
      handle exn =>
wenzelm@31333
   175
       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
wenzelm@31480
   176
        err (output ()); reraise exn);
wenzelm@31333
   177
  in if verbose then print (output ()) else () end;
wenzelm@31333
   178
wenzelm@31333
   179
end;
wenzelm@31333
   180