[m-rev.] for review: allow reporting of statistics to a stream for Java

[Julien Fischer]

For review by anyone.

A few things:

- we need to decide how I/O errors that occur when reporting statistics 
are handled (see XXXs below).
- the C implementation does not update the line number counter
associated with the (Mercury) stream.
- it would be nice to have a version of the statistics reporting code
that prints a user specified prefix at the beginning of each line.

NOTE: the Java (and probaby C#) versions of the report stats code
need to be defined in the standard library since that's where the
Java and C# definitions of Mercury file streams are.

--------------------------------------------------

Allow reporting of statistics to a stream for Java.

library/benchmarking.m:
     Generalise the Java implementations of report_stats so that they
     can write a specified text output stream, not just standard error.

library/io.m:
     Implement report_{standard,full_memory}_stats_2 for Java.

Julien.

diff --git a/library/benchmarking.m b/library/benchmarking.m
index 7f41143..846f4df 100644
--- a/library/benchmarking.m
+++ b/library/benchmarking.m
@@ -190,7 +190,7 @@
      report_stats,
      [may_call_mercury, terminates],
  "
-    MR_report_standard_stats();
+    ML_report_standard_stats(io.mercury_stderr);
  ").

  %---------------------%
@@ -213,7 +213,7 @@
      report_full_memory_stats,
      [will_not_call_mercury],
  "
-    MR_report_full_memory_stats();
+    ML_report_full_memory_stats(io.mercury_stderr);
  ").

  %---------------------------------------------------------------------------%
@@ -312,8 +312,8 @@ ML_initialise()
      real_time_at_last_stat = real_time_at_start;
  }

-private static void
-MR_report_standard_stats()
+public static void
+ML_report_standard_stats(jmercury.io.MR_TextOutputFile stream)
  {
      int user_time_at_prev_stat = user_time_at_last_stat;
      user_time_at_last_stat = ML_get_user_cpu_milliseconds();
@@ -321,36 +321,44 @@ MR_report_standard_stats()
      long real_time_at_prev_stat = real_time_at_last_stat;
      real_time_at_last_stat = System.currentTimeMillis();

-    System.err.print(
-        ""[User time: +"" +
-        ((user_time_at_last_stat - user_time_at_prev_stat) / 1000.0) +
-        ""s, "" +
-        ((user_time_at_last_stat - user_time_at_start) / 1000.0) +
-        ""s"");
-
-    System.err.print(
-        "" Real time: +"" +
-        ((real_time_at_last_stat - real_time_at_prev_stat) / 1000.0) +
-        ""s, "" +
-        ((real_time_at_last_stat - real_time_at_start) / 1000.0) +
-        ""s"");
-
-    // XXX At this point there should be a whole bunch of memory usage
-    // statistics. Unfortunately the Java back-end does not yet support
-    // this amount of profiling, so cpu time is all you get.
-
-    System.err.println(""]"");
+    try {
+        stream.write(
+            ""[User time: +"" +
+            ((user_time_at_last_stat - user_time_at_prev_stat) / 1000.0) +
+            ""s, "" +
+            ((user_time_at_last_stat - user_time_at_start) / 1000.0) +
+            ""s"");
+
+        stream.write(
+            "" Real time: +"" +
+            ((real_time_at_last_stat - real_time_at_prev_stat) / 1000.0) +
+            ""s, "" +
+            ((real_time_at_last_stat - real_time_at_start) / 1000.0) +
+            ""s"");
+
+        // XXX At this point there should be a whole bunch of memory usage
+        // statistics. Unfortunately the Java back-end does not yet support
+        // this amount of profiling, so cpu time is all you get.
+
+        stream.write(""]\\n"");
+    } catch (java.io.IOException e) {
+        // XXX how should we handle I/O errors when printing statistics?
+    }
  }

-private static void
-MR_report_full_memory_stats()
+public static void
+ML_report_full_memory_stats(jmercury.io.MR_TextOutputFile stream)
  {
      // XXX The support for this predicate is even worse. Since we don't have
      // access to memory usage statistics, all you get here is an apology.
      // But at least it doesn't just crash with an error.

-    System.err.println(""Sorry, report_full_memory_stats is not yet "" +
-        ""implemented for the Java back-end."");
+    try {
+        stream.write(""Sorry, report_full_memory_stats is not yet "" +
+            ""implemented for the Java back-end."");
+    } catch (java.io.IOException e) {
+        // XXX how should we handle I/O errors when printing statistics?
+    }
  }
  ").

diff --git a/library/io.m b/library/io.m
index bbe8be2..b6b69da 100644
--- a/library/io.m
+++ b/library/io.m
@@ -12131,6 +12131,14 @@ report_standard_stats(!IO) :-
      MR_report_standard_stats(MR_file(*Stream));
  ").

+:- pragma foreign_proc("Java",
+    report_standard_stats_2(Stream::in, _IO0::di, _IO::uo),
+    [promise_pure, will_not_call_mercury],
+"
+    jmercury.benchmarking.ML_report_standard_stats(
+        (jmercury.io.MR_TextOutputFile) Stream);
+").
+
  report_standard_stats_2(_Stream, !IO) :-
      private_builtin.sorry("report_standard_stats").

@@ -12152,6 +12160,14 @@ report_full_memory_stats(!IO) :-
      MR_report_full_memory_stats(MR_file(*Stream));
  ").

+:- pragma foreign_proc("Java",
+    report_full_memory_stats_2(Stream::in, _IO0::di, _IO::uo),
+    [promise_pure, will_not_call_mercury],
+"
+    jmercury.benchmarking.ML_report_full_memory_stats(
+        (jmercury.io.MR_TextOutputFile) Stream);
+").
+
  report_full_memory_stats_2(_Stream, !IO) :-
      private_builtin.sorry("report_full_memory_stats").