src/Pure/ML/ml_compiler_polyml-5.3.ML
author wenzelm
Mon Jun 01 23:28:06 2009 +0200 (2009-06-01)
changeset 31333 fcd010617e6c
child 31429 8a7c0899e0b1
permissions -rw-r--r--
added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
wenzelm@31333
     1
(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
wenzelm@31333
     2
    Author:     Makarius
wenzelm@31333
     3
wenzelm@31333
     4
Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
wenzelm@31333
     5
*)
wenzelm@31333
     6
wenzelm@31333
     7
signature ML_COMPILER =
wenzelm@31333
     8
sig
wenzelm@31333
     9
  val eval: bool -> Position.T -> ML_Lex.token list -> unit
wenzelm@31333
    10
end
wenzelm@31333
    11
wenzelm@31333
    12
structure ML_Compiler: ML_COMPILER =
wenzelm@31333
    13
struct
wenzelm@31333
    14
wenzelm@31333
    15
(* original source positions *)
wenzelm@31333
    16
wenzelm@31333
    17
fun position_of (SOME context) (loc: PolyML.location) =
wenzelm@31333
    18
      (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
wenzelm@31333
    19
        (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
wenzelm@31333
    20
      | (SOME pos, NONE) => pos
wenzelm@31333
    21
      | _ => Position.line_file (#startLine loc) (#file loc))
wenzelm@31333
    22
  | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
wenzelm@31333
    23
wenzelm@31333
    24
wenzelm@31333
    25
(* parse trees *)
wenzelm@31333
    26
wenzelm@31333
    27
fun report_parse_tree context depth space =
wenzelm@31333
    28
  let
wenzelm@31333
    29
    val pos_of = position_of context;
wenzelm@31333
    30
    fun report loc (PolyML.PTtype types) =
wenzelm@31333
    31
          PolyML.NameSpace.displayTypeExpression (types, depth, space)
wenzelm@31333
    32
          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
wenzelm@31333
    33
          |> Position.report_text Markup.ML_typing (pos_of loc)
wenzelm@31333
    34
      | report loc (PolyML.PTdeclaredAt decl) =
wenzelm@31333
    35
          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
wenzelm@31333
    36
          |> Position.report_text Markup.ML_ref (pos_of loc)
wenzelm@31333
    37
      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
wenzelm@31333
    38
      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
wenzelm@31333
    39
      | report _ _ = ()
wenzelm@31333
    40
    and report_tree (loc, props) = List.app (report loc) props;
wenzelm@31333
    41
  in report_tree end;
wenzelm@31333
    42
wenzelm@31333
    43
wenzelm@31333
    44
(* eval ML source tokens *)
wenzelm@31333
    45
wenzelm@31333
    46
fun eval verbose pos toks =
wenzelm@31333
    47
  let
wenzelm@31333
    48
    val _ = Secure.secure_mltext ();
wenzelm@31333
    49
    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
wenzelm@31333
    50
wenzelm@31333
    51
wenzelm@31333
    52
    (* input *)
wenzelm@31333
    53
wenzelm@31333
    54
    val input =
wenzelm@31333
    55
      if is_none (Context.thread_data ()) then map (pair 0) toks
wenzelm@31333
    56
      else Context.>>> (ML_Env.register_tokens toks);
wenzelm@31333
    57
    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
wenzelm@31333
    58
wenzelm@31333
    59
    val current_line = ref (the_default 1 (Position.line_of pos));
wenzelm@31333
    60
wenzelm@31333
    61
    fun get_index () =
wenzelm@31333
    62
      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
wenzelm@31333
    63
wenzelm@31333
    64
    fun get () =
wenzelm@31333
    65
      (case ! input_buffer of
wenzelm@31333
    66
        [] => NONE
wenzelm@31333
    67
      | (_, []) :: rest => (input_buffer := rest; get ())
wenzelm@31333
    68
      | (i, c :: cs) :: rest =>
wenzelm@31333
    69
          (input_buffer := (i, cs) :: rest;
wenzelm@31333
    70
           if c = #"\n" then current_line := ! current_line + 1 else ();
wenzelm@31333
    71
           SOME c));
wenzelm@31333
    72
wenzelm@31333
    73
wenzelm@31333
    74
    (* output *)
wenzelm@31333
    75
wenzelm@31333
    76
    val output_buffer = ref Buffer.empty;
wenzelm@31333
    77
    fun output () = Buffer.content (! output_buffer);
wenzelm@31333
    78
    fun put s = change output_buffer (Buffer.add s);
wenzelm@31333
    79
wenzelm@31333
    80
    fun put_message {message, hard, location, context = _} =
wenzelm@31333
    81
     (put (if hard then "Error: " else "Warning: ");
wenzelm@31333
    82
      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
wenzelm@31333
    83
      put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
wenzelm@31333
    84
wenzelm@31333
    85
wenzelm@31333
    86
    (* results *)
wenzelm@31333
    87
wenzelm@31333
    88
    val depth = get_print_depth ();
wenzelm@31333
    89
wenzelm@31333
    90
    fun apply_result {fixes, types, signatures, structures, functors, values} =
wenzelm@31333
    91
      let
wenzelm@31333
    92
        fun display disp x =
wenzelm@31333
    93
          if depth > 0 then
wenzelm@31333
    94
            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
wenzelm@31333
    95
          else ();
wenzelm@31333
    96
wenzelm@31333
    97
        fun apply_fix (a, b) =
wenzelm@31333
    98
          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
wenzelm@31333
    99
        fun apply_type (a, b) =
wenzelm@31333
   100
          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
wenzelm@31333
   101
        fun apply_sig (a, b) =
wenzelm@31333
   102
          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
wenzelm@31333
   103
        fun apply_struct (a, b) =
wenzelm@31333
   104
          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
wenzelm@31333
   105
        fun apply_funct (a, b) =
wenzelm@31333
   106
          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
wenzelm@31333
   107
        fun apply_val (a, b) =
wenzelm@31333
   108
          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
wenzelm@31333
   109
      in
wenzelm@31333
   110
        List.app apply_fix fixes;
wenzelm@31333
   111
        List.app apply_type types;
wenzelm@31333
   112
        List.app apply_sig signatures;
wenzelm@31333
   113
        List.app apply_struct structures;
wenzelm@31333
   114
        List.app apply_funct functors;
wenzelm@31333
   115
        List.app apply_val values
wenzelm@31333
   116
      end;
wenzelm@31333
   117
wenzelm@31333
   118
    fun result_fun (phase1, phase2) () =
wenzelm@31333
   119
     (case phase1 of NONE => ()
wenzelm@31333
   120
      | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
wenzelm@31333
   121
      case phase2 of NONE => err "Static Errors"
wenzelm@31333
   122
      | SOME code => apply_result (code ()));  (* FIXME Toplevel.program *)
wenzelm@31333
   123
wenzelm@31333
   124
wenzelm@31333
   125
    (* compiler invocation *)
wenzelm@31333
   126
wenzelm@31333
   127
    val parameters =
wenzelm@31333
   128
     [PolyML.Compiler.CPOutStream put,
wenzelm@31333
   129
      PolyML.Compiler.CPNameSpace space,
wenzelm@31333
   130
      PolyML.Compiler.CPErrorMessageProc put_message,
wenzelm@31333
   131
      PolyML.Compiler.CPLineNo (fn () => ! current_line),
wenzelm@31333
   132
      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
wenzelm@31333
   133
      PolyML.Compiler.CPLineOffset get_index,
wenzelm@31333
   134
      PolyML.Compiler.CPCompilerResultFun result_fun];
wenzelm@31333
   135
    val _ =
wenzelm@31333
   136
      (while not (List.null (! input_buffer)) do
wenzelm@31333
   137
        PolyML.compiler (get, parameters) ())
wenzelm@31333
   138
      handle exn =>
wenzelm@31333
   139
       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
wenzelm@31333
   140
        err (output ()); raise exn);
wenzelm@31333
   141
  in if verbose then print (output ()) else () end;
wenzelm@31333
   142
wenzelm@31333
   143
end;
wenzelm@31333
   144