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