<commit_before>(*  Title:      Pure/ML/ml_compiler_polyml.ML
    Author:     Makarius

Advanced runtime compilation for Poly/ML.
*)

structure ML_Compiler: ML_COMPILER =
struct

(* source locations *)

fun position_of (loc: PolyML.location) =
  let
    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
    val props = Exn_Properties.of_location loc;
  in
    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
  end;


(* exn_info *)

fun exn_position exn =
  (case PolyML.exceptionLocation exn of
    NONE => Position.none
  | SOME loc => position_of loc);

fun pretty_exn (exn: exn) =
  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));

val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};


(* exn_message *)

val exn_messages_ids = Runtime.exn_messages_ids exn_info;
val exn_messages = Runtime.exn_messages exn_info;
val exn_message = Runtime.exn_message exn_info;

val exn_error_message = Output.error_message o exn_message;
fun exn_trace e = print_exception_trace exn_message e;


(* parse trees *)

fun report_parse_tree depth space =
  let
    val reported_text =
      (case Context.thread_data () of
        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
      | _ => Position.reported_text);

    fun reported_entity kind loc decl =
      reported_text (position_of loc)
        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";

    fun reported loc (PolyML.PTtype types) =
          cons
            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
              |> reported_text (position_of loc) Markup.ML_typing)
      | reported loc (PolyML.PTdeclaredAt decl) =
          cons (reported_entity Markup.ML_defN loc decl)
      | reported loc (PolyML.PTopenedAt decl) =
          cons (reported_entity Markup.ML_openN loc decl)
      | reported loc (PolyML.PTstructureAt decl) =
          cons (reported_entity Markup.ML_structN loc decl)
      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
      | reported _ _ = I
    and reported_tree (loc, props) = fold (reported loc) props;
  in fn tree => Output.report (implode (reported_tree tree [])) end;


(* eval ML source tokens *)

fun eval verbose pos toks =
  let
    val _ = Secure.secure_mltext ();
    val space = ML_Env.name_space;


    (* input *)

    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));

    val input_buffer =
      Unsynchronized.ref (toks |> map
        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));

    fun get () =
      (case ! input_buffer of
        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
      | [] => NONE);

    fun get_pos () =
      (case ! input_buffer of
        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
      | ([], tok) :: _ => ML_Lex.end_pos_of tok
      | [] => Position.none);


    (* output channels *)

    val writeln_buffer = Unsynchronized.ref Buffer.empty;
    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));

    val warnings = Unsynchronized.ref ([]: string list);
    fun warn msg = Unsynchronized.change warnings (cons msg);
    fun output_warnings () = List.app warning (rev (! warnings));

    val error_buffer = Unsynchronized.ref Buffer.empty;
    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
    fun flush_error () = writeln (Buffer.content (! error_buffer));
    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));

    fun message {message = msg, hard, location = loc, context = _} =
      let
        val pos = position_of loc;
        val txt =
          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
      in if hard then err txt else warn txt end;

<commit_msg>tuned message;<commit_after>(*  Title:      Pure/ML/ml_compiler_polyml.ML
    Author:     Makarius

Advanced runtime compilation for Poly/ML.
*)

structure ML_Compiler: ML_COMPILER =
struct

(* source locations *)

fun position_of (loc: PolyML.location) =
  let
    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
    val props = Exn_Properties.of_location loc;
  in
    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
  end;


(* exn_info *)

fun exn_position exn =
  (case PolyML.exceptionLocation exn of
    NONE => Position.none
  | SOME loc => position_of loc);

fun pretty_exn (exn: exn) =
  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));

val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};


(* exn_message *)

val exn_messages_ids = Runtime.exn_messages_ids exn_info;
val exn_messages = Runtime.exn_messages exn_info;
val exn_message = Runtime.exn_message exn_info;

val exn_error_message = Output.error_message o exn_message;
fun exn_trace e = print_exception_trace exn_message e;


(* parse trees *)

fun report_parse_tree depth space =
  let
    val reported_text =
      (case Context.thread_data () of
        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
      | _ => Position.reported_text);

    fun reported_entity kind loc decl =
      reported_text (position_of loc)
        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";

    fun reported loc (PolyML.PTtype types) =
          cons
            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
              |> reported_text (position_of loc) Markup.ML_typing)
      | reported loc (PolyML.PTdeclaredAt decl) =
          cons (reported_entity Markup.ML_defN loc decl)
      | reported loc (PolyML.PTopenedAt decl) =
          cons (reported_entity Markup.ML_openN loc decl)
      | reported loc (PolyML.PTstructureAt decl) =
          cons (reported_entity Markup.ML_structN loc decl)
      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
      | reported _ _ = I
    and reported_tree (loc, props) = fold (reported loc) props;
  in fn tree => Output.report (implode (reported_tree tree [])) end;


(* eval ML source tokens *)

fun eval verbose pos toks =
  let
    val _ = Secure.secure_mltext ();
    val space = ML_Env.name_space;


    (* input *)

    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));

    val input_buffer =
      Unsynchronized.ref (toks |> map
        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));

    fun get () =
      (case ! input_buffer of
        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
      | [] => NONE);

    fun get_pos () =
      (case ! input_buffer of
        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
      | ([], tok) :: _ => ML_Lex.end_pos_of tok
      | [] => Position.none);


    (* output channels *)

    val writeln_buffer = Unsynchronized.ref Buffer.empty;
    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
    fun output_writeln () = writeln (trim_line (Buffer.content (! writeln_buffer)));

    val warnings = Unsynchronized.ref ([]: string list);
    fun warn msg = Unsynchronized.change warnings (cons msg);
    fun output_warnings () = List.app warning (rev (! warnings));

    val error_buffer = Unsynchronized.ref Buffer.empty;
    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
    fun flush_error () = writeln (Buffer.content (! error_buffer));
    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));

    fun message {message = msg, hard, location = loc, context = _} =
      let
        val pos = position_of loc;
        val txt =
          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
      in if hard then err txt else warn txt end;


{'fraction_non_alphanumeric': 0.11460410557184751, 'fraction_numerical': 0.0, 'mean_word_length': 3.1128798842257597, 'pattern_counts': {'":': 4, '<': 3, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4208002', 'n_tokens_mistral': 2791, 'n_tokens_neox': 2697, 'n_words': 744}