src/Pure/ML/ml_compiler_polyml.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 47980 c81801f881b3
child 48992 0518bf89c777
permissions -rw-r--r--
more official command specifications, including source position;
wenzelm@47980
     1
(*  Title:      Pure/ML/ml_compiler_polyml.ML
wenzelm@31333
     2
    Author:     Makarius
wenzelm@31333
     3
wenzelm@45147
     4
Advanced runtime compilation for Poly/ML 5.3.0 or later.
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@41483
    15
      endLine = _, endPosition = end_offset} = loc;
wenzelm@41484
    16
    val props =
wenzelm@31434
    17
      (case YXML.parse text of
wenzelm@45666
    18
        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
wenzelm@31434
    19
      | XML.Text s => Position.file_name s);
wenzelm@31429
    20
  in
wenzelm@43710
    21
    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
wenzelm@41484
    22
  end;
wenzelm@31429
    23
wenzelm@31477
    24
fun exn_position exn =
wenzelm@31429
    25
  (case PolyML.exceptionLocation exn of
wenzelm@31429
    26
    NONE => Position.none
wenzelm@31429
    27
  | SOME loc => position_of loc);
wenzelm@31333
    28
wenzelm@38874
    29
val exn_messages = Runtime.exn_messages exn_position;
wenzelm@31477
    30
val exn_message = Runtime.exn_message exn_position;
wenzelm@31477
    31
wenzelm@31333
    32
wenzelm@31333
    33
(* parse trees *)
wenzelm@31333
    34
wenzelm@31429
    35
fun report_parse_tree depth space =
wenzelm@31333
    36
  let
wenzelm@44737
    37
    val reported_text =
wenzelm@38720
    38
      (case Context.thread_data () of
wenzelm@44737
    39
        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
wenzelm@44737
    40
      | _ => Position.reported_text);
wenzelm@38720
    41
wenzelm@44737
    42
    fun reported_entity kind loc decl =
wenzelm@44737
    43
      reported_text (position_of loc)
wenzelm@45666
    44
        (Isabelle_Markup.entityN,
wenzelm@45666
    45
          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
wenzelm@41503
    46
wenzelm@44737
    47
    fun reported loc (PolyML.PTtype types) =
wenzelm@44737
    48
          cons
wenzelm@44737
    49
            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
wenzelm@44737
    50
              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
wenzelm@45666
    51
              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
wenzelm@44737
    52
      | reported loc (PolyML.PTdeclaredAt decl) =
wenzelm@45666
    53
          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
wenzelm@44737
    54
      | reported loc (PolyML.PTopenedAt decl) =
wenzelm@45666
    55
          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
wenzelm@44737
    56
      | reported loc (PolyML.PTstructureAt decl) =
wenzelm@45666
    57
          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
wenzelm@44737
    58
      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
wenzelm@44737
    59
      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
wenzelm@44737
    60
      | reported _ _ = I
wenzelm@44737
    61
    and reported_tree (loc, props) = fold (reported loc) props;
wenzelm@44737
    62
  in fn tree => Output.report (implode (reported_tree tree [])) end;
wenzelm@31333
    63
wenzelm@31333
    64
wenzelm@31333
    65
(* eval ML source tokens *)
wenzelm@31333
    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@45666
    76
      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
wenzelm@45666
    77
            (filter (member (op =)
wenzelm@45666
    78
              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
wenzelm@31437
    79
wenzelm@41501
    80
    val input_buffer =
wenzelm@41501
    81
      Unsynchronized.ref (toks |> map
wenzelm@41501
    82
        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
wenzelm@31333
    83
wenzelm@31333
    84
    fun get () =
wenzelm@31333
    85
      (case ! input_buffer of
wenzelm@41501
    86
        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
wenzelm@41501
    87
      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
wenzelm@41501
    88
      | [] => NONE);
wenzelm@41501
    89
wenzelm@41501
    90
    fun get_pos () =
wenzelm@41501
    91
      (case ! input_buffer of
wenzelm@41501
    92
        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
wenzelm@41501
    93
      | ([], tok) :: _ => ML_Lex.end_pos_of tok
wenzelm@41501
    94
      | [] => Position.none);
wenzelm@31333
    95
wenzelm@31333
    96
wenzelm@39228
    97
    (* output channels *)
wenzelm@39228
    98
wenzelm@39228
    99
    val writeln_buffer = Unsynchronized.ref Buffer.empty;
wenzelm@39228
   100
    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
wenzelm@39228
   101
    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
wenzelm@39228
   102
wenzelm@39228
   103
    val warnings = Unsynchronized.ref ([]: string list);
wenzelm@39231
   104
    fun warn msg = Unsynchronized.change warnings (cons msg);
wenzelm@39228
   105
    fun output_warnings () = List.app warning (rev (! warnings));
wenzelm@39228
   106
wenzelm@39228
   107
    val error_buffer = Unsynchronized.ref Buffer.empty;
wenzelm@39231
   108
    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
wenzelm@39228
   109
    fun flush_error () = writeln (Buffer.content (! error_buffer));
wenzelm@39228
   110
    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
wenzelm@31333
   111
wenzelm@39228
   112
    fun message {message = msg, hard, location = loc, context = _} =
wenzelm@39228
   113
      let
wenzelm@41504
   114
        val pos = position_of loc;
wenzelm@39228
   115
        val txt =
wenzelm@45666
   116
          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
wenzelm@41504
   117
            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
wenzelm@39228
   118
          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
wenzelm@45666
   119
          Position.reported_text pos Isabelle_Markup.report "";
wenzelm@39231
   120
      in if hard then err txt else warn txt end;
wenzelm@31333
   121
wenzelm@31333
   122
wenzelm@31333
   123
    (* results *)
wenzelm@31333
   124
wenzelm@31333
   125
    val depth = get_print_depth ();
wenzelm@31333
   126
wenzelm@31333
   127
    fun apply_result {fixes, types, signatures, structures, functors, values} =
wenzelm@31333
   128
      let
wenzelm@31333
   129
        fun display disp x =
wenzelm@31333
   130
          if depth > 0 then
wenzelm@39228
   131
            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
wenzelm@31333
   132
          else ();
wenzelm@31333
   133
wenzelm@31333
   134
        fun apply_fix (a, b) =
wenzelm@40799
   135
          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
wenzelm@31333
   136
        fun apply_type (a, b) =
wenzelm@40799
   137
          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
wenzelm@31333
   138
        fun apply_sig (a, b) =
wenzelm@40799
   139
          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
wenzelm@31333
   140
        fun apply_struct (a, b) =
wenzelm@40799
   141
          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
wenzelm@31333
   142
        fun apply_funct (a, b) =
wenzelm@40799
   143
          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
wenzelm@31333
   144
        fun apply_val (a, b) =
wenzelm@40799
   145
          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
wenzelm@31333
   146
      in
wenzelm@31333
   147
        List.app apply_fix fixes;
wenzelm@31333
   148
        List.app apply_type types;
wenzelm@31333
   149
        List.app apply_sig signatures;
wenzelm@31333
   150
        List.app apply_struct structures;
wenzelm@31333
   151
        List.app apply_funct functors;
wenzelm@31333
   152
        List.app apply_val values
wenzelm@31333
   153
      end;
wenzelm@31333
   154
wenzelm@39231
   155
    exception STATIC_ERRORS of unit;
wenzelm@39230
   156
wenzelm@31333
   157
    fun result_fun (phase1, phase2) () =
wenzelm@31477
   158
     ((case phase1 of
wenzelm@31477
   159
        NONE => ()
wenzelm@31477
   160
      | SOME parse_tree => report_parse_tree depth space parse_tree);
wenzelm@31477
   161
      (case phase2 of
wenzelm@39231
   162
        NONE => raise STATIC_ERRORS ()
wenzelm@31477
   163
      | SOME code =>
wenzelm@33603
   164
          apply_result
wenzelm@33603
   165
            ((code
wenzelm@33603
   166
              |> Runtime.debugging
wenzelm@39231
   167
              |> Runtime.toplevel_error (err o exn_message)) ())));
wenzelm@31333
   168
wenzelm@31333
   169
wenzelm@31333
   170
    (* compiler invocation *)
wenzelm@31333
   171
wenzelm@31333
   172
    val parameters =
wenzelm@39228
   173
     [PolyML.Compiler.CPOutStream write,
wenzelm@31333
   174
      PolyML.Compiler.CPNameSpace space,
wenzelm@39228
   175
      PolyML.Compiler.CPErrorMessageProc message,
wenzelm@41501
   176
      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
wenzelm@41501
   177
      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
wenzelm@31437
   178
      PolyML.Compiler.CPFileName location_props,
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@39232
   192
              | _ => "Exception- " ^ General.exnMessage 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@39228
   197
    if verbose 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