(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML

     Author:     Makarius

 Advanced runtime compilation for Poly/ML 5.3 (SVN 762).

 *)

 signature ML_COMPILER =

 sig

   val exception_position: exn -> Position.T

   val eval: bool -> Position.T -> ML_Lex.token list -> unit

 end

 structure ML_Compiler: ML_COMPILER =

 struct

 (* source locations *)

 fun position_of (loc: PolyML.location) =

   let

     val {file = text, startLine = line, startPosition = offset,

       endLine = end_line, endPosition = end_offset} = loc;

     val loc_props =

       (case YXML.parse text of

         XML.Elem (e, atts, _) => if e = Markup.positionN then atts else []

       | XML.Text s => Position.file_name s);

   in

     Position.value Markup.lineN line @

     Position.value Markup.offsetN offset @

     Position.value Markup.end_lineN end_line @

     Position.value Markup.end_offsetN end_offset @

     loc_props

   end |> Position.of_properties;

 fun exception_position exn =

   (case PolyML.exceptionLocation exn of

     NONE => Position.none

   | SOME loc => position_of loc);

 (* parse trees *)

 fun report_parse_tree depth space =

   let

     fun report loc (PolyML.PTtype types) =

           PolyML.NameSpace.displayTypeExpression (types, depth, space)

           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of

           |> Position.report_text Markup.ML_typing (position_of loc)

       | report loc (PolyML.PTdeclaredAt decl) =

           Markup.markup

             (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) ""

           |> Position.report_text Markup.ML_ref (position_of loc)

       | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())

       | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())

       | report _ _ = ()

     and report_tree (loc, props) = List.app (report loc) props;

   in report_tree end;

 (* eval ML source tokens *)

 fun eval verbose pos toks =

   let

     val _ = Secure.secure_mltext ();

     val {name_space = space, print, error = err, ...} = ML_Env.local_context;

     (* input *)

     val location_props =

       Markup.markup (Markup.position |> Markup.properties

           (filter (member (op =) [Markup.idN, Markup.fileN] o #1) (Position.properties_of pos))) "";

     val input = toks |> maps (fn tok =>

       let

         val syms = Symbol.explode (ML_Lex.check_content_of tok);

         val (ps, _) = fold_map (fn s => fn p => (p, Position.advance s p)) syms

           (Position.reset_range (ML_Lex.pos_of tok));

       in ps ~~ map (String.explode o Symbol.esc) syms end);

     val input_buffer = ref input;

     val line = ref (the_default 1 (Position.line_of pos));

     fun get_offset () =

       the_default 0

         (get_first (fn (_, []) => NONE | (p, _) => Position.offset_of p) (! input_buffer));

     fun get () =

       (case ! input_buffer of

         [] => NONE

       | (_, []) :: rest => (input_buffer := rest; get ())

       | (p, c :: cs) :: rest =>

           (input_buffer := (p, cs) :: rest;

            if c = #"\n" then line := ! line + 1 else ();

            SOME c));

     (* output *)

     val output_buffer = ref Buffer.empty;

     fun output () = Buffer.content (! output_buffer);

     fun put s = change output_buffer (Buffer.add s);

     fun put_message {message, hard, location, context = _} =

      (put (if hard then "Error: " else "Warning: ");

       put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));

       put (Position.str_of (position_of location) ^ "\n"));

     (* results *)

     val depth = get_print_depth ();

     fun apply_result {fixes, types, signatures, structures, functors, values} =

       let

         fun display disp x =

           if depth > 0 then

             (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")

           else ();

         fun apply_fix (a, b) =

           (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));

         fun apply_type (a, b) =

           (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));

         fun apply_sig (a, b) =

           (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));

         fun apply_struct (a, b) =

           (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));

         fun apply_funct (a, b) =

           (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));

         fun apply_val (a, b) =

           (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));

       in

         List.app apply_fix fixes;

         List.app apply_type types;

         List.app apply_sig signatures;

         List.app apply_struct structures;

         List.app apply_funct functors;

         List.app apply_val values

       end;

     fun result_fun (phase1, phase2) () =

      (case phase1 of NONE => ()

       | SOME parse_tree => report_parse_tree depth space parse_tree;

       case phase2 of NONE => err "Static Errors"

       | SOME code => apply_result (code ()));  (* FIXME cf. Toplevel.program *)

     (* compiler invocation *)

     val parameters =

      [PolyML.Compiler.CPOutStream put,

       PolyML.Compiler.CPNameSpace space,

       PolyML.Compiler.CPErrorMessageProc put_message,

       PolyML.Compiler.CPLineNo (fn () => ! line),

       PolyML.Compiler.CPFileName location_props,

       PolyML.Compiler.CPLineOffset get_offset,

       PolyML.Compiler.CPCompilerResultFun result_fun];

     val _ =

       (while not (List.null (! input_buffer)) do

         PolyML.compiler (get, parameters) ())

       handle exn =>

        (put ("Exception- " ^ General.exnMessage exn ^ " raised");

         err (output ()); raise exn);

   in if verbose then print (output ()) else () end;

 end;