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