# HG changeset patch
# User wenzelm
# Date 1495052853 -7200
# Node ID 9418a9fad8359e775497becdb82761963b112712
# Parent  5d29d93766ef30f7a168457d3ebfccf07a5e5637
more systematic maximum and average;
tuned;

diff -r 5d29d93766ef -r 9418a9fad835 src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed May 17 21:24:16 2017 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Wed May 17 22:27:33 2017 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.{SortedSet, SortedMap}
 import scala.swing.{Frame, Component}
@@ -26,6 +27,8 @@
 
   /* standard fields */
 
+  val HEAP_SIZE = "size_heap"
+
   type Fields = (String, Iterable[String])
 
   val tasks_fields: Fields =
@@ -39,7 +42,7 @@
     ("GCs", List("partial_GCs", "full_GCs"))
 
   val heap_fields: Fields =
-    ("Heap", List("size_heap", "size_allocation", "size_allocation_free",
+    ("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
       "size_heap_free_last_full_GC", "size_heap_free_last_GC"))
 
   val threads_fields: Fields =
@@ -65,7 +68,7 @@
 
   final case class Entry(time: Double, data: Map[String, Double])
   {
-    def heap_size: Long = data.getOrElse("size_heap", 0.0).toLong
+    def get(field: String): Double = data.getOrElse(field, 0.0)
   }
 
   val empty: ML_Statistics = apply(Nil)
@@ -123,8 +126,29 @@
   val time_start: Double,
   val duration: Double)
 {
-  def heap_size_max: Long =
-    (0L /: content)({ case (m, entry) => m max entry.heap_size })
+  /* content */
+
+  def maximum(field: String): Double =
+    (0.0 /: content)({ case (m, e) => m max e.get(field) })
+
+  def average(field: String): Double =
+  {
+    @tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
+      list match {
+        case Nil => acc
+        case e :: es =>
+          val t = e.time
+          sum(t, es, (t - t0) * e.get(field) + acc)
+      }
+    content match {
+      case Nil => 0.0
+      case List(e) => e.get(field)
+      case e :: es => sum(e.time, es, 0.0) / duration
+    }
+  }
+
+  def maximum_heap_size: Long = maximum(ML_Statistics.HEAP_SIZE).toLong
+  def average_heap_size: Long = average(ML_Statistics.HEAP_SIZE).toLong
 
 
   /* charts */