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