Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: timing.scala Sprache: Scala

Original von: Isabelle^©

/*  Title:      Pure/General/timing.scala
    Author:     Makarius

Support for time measurement.
*/

package isabelle

import java.util.Locale

object Timing
{
  val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)

  def timeit[A](
    message: String = "",
    enabled: Boolean = true,
    output: String => Unit = Output.warning(_))(e: => A): A =
  {
    if (enabled) {
      val start = Time.now()
      val result = Exn.capture(e)
      val stop = Time.now()

      val timing = stop - start
      if (timing.is_relevant) {
        output(
          (if (message == null || message == "") "" else message + ": ") +
            timing.message + " elapsed time")
      }

      Exn.release(result)
    }
    else e
  }

  def factor_format(f: Double): String =
    String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
}

sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
{
  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant

  def resources: Time = cpu + gc

  def factor: Option[Double] =
  {
    val t1 = elapsed.seconds
    val t2 = resources.seconds
    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
  }

  def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)

  def message: String =
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"

  def message_factor: String =
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" +
      Timing.factor_format(cpu.seconds / elapsed.seconds)

  def message_resources: String =
  {
    val factor_text =
      factor match {
        case Some(f) => Timing.factor_format(f)
        case None => ""
      }
    if (resources.seconds >= 3.0)
      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
    else
      elapsed.message_hms + " elapsed time" + factor_text
  }

  override def toString: String = message

  def json: JSON.Object.T =
    JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds)
}

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.