src/Pure/ML/ml_profiling.scala
author wenzelm
Tue, 08 Jun 2021 16:32:57 +0200
changeset 73836 690fdc14f7fb
child 73839 0638fa8c01bc
permissions -rw-r--r--
add missing file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
73836
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/ML/ml_profiling.scala
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     3
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     4
ML profiling.
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     5
*/
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     6
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     7
package isabelle
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     8
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
     9
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    10
import java.util.Locale
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    11
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    12
import scala.collection.immutable.SortedMap
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    13
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    14
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    15
object ML_Profiling
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    16
{
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    17
  sealed case class Entry(name: String, count: Long)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    18
  {
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    19
    def clean_name: Entry = copy(name = """-?\(\d+\).*$""".r.replaceAllIn(name, ""))
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    20
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    21
    def print: String =
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    22
      String.format(Locale.ROOT, "%10d %s",
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    23
        count.asInstanceOf[AnyRef], name.asInstanceOf[AnyRef])
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    24
  }
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    25
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    26
  sealed case class Report(kind: String, entries: List[Entry])
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    27
  {
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    28
    def clean_name: Report = copy(entries = entries.map(_.clean_name))
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    29
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    30
    def total: Entry = Entry("TOTAL", entries.iterator.map(_.count).sum)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    31
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    32
    def print: String =
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    33
    {
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    34
      (if (kind == "time_thread") "time profile (single thread)" else kind + " profile") +
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    35
        (entries ::: List(total)).map(_.print).mkString(":\n", "\n", "\n")
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    36
    }
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    37
  }
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    38
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    39
  def account(reports: List[Report]): List[Report] =
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    40
  {
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    41
    val empty = SortedMap.empty[String, Long].withDefaultValue(0L)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    42
    var results = SortedMap.empty[String, SortedMap[String, Long]].withDefaultValue(empty)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    43
    for (report <- reports) {
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    44
      val kind = report.kind
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    45
      val map = report.entries.foldLeft(results(kind))(
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    46
        (m, e) => m + (e.name -> (e.count + m(e.name))))
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    47
      results = results + (kind -> map)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    48
    }
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    49
    for ((kind, map) <- results.toList)
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    50
      yield Report(kind, for ((name, count) <- map.toList.sortBy(_._2)) yield Entry(name, count))
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    51
  }
690fdc14f7fb add missing file;
wenzelm
parents:
diff changeset
    52
}