1/*  Title:      Pure/General/timing.scala
2    Author:     Makarius
3
4Support for time measurement.
5*/
6
7package isabelle
8
9
10import java.util.Locale
11
12
13object Timing
14{
15  val zero: Timing = Timing(Time.zero, Time.zero, Time.zero)
16
17  def timeit[A](
18    message: String = "",
19    enabled: Boolean = true,
20    output: String => Unit = Output.warning(_))(e: => A): A =
21  {
22    if (enabled) {
23      val start = Time.now()
24      val result = Exn.capture(e)
25      val stop = Time.now()
26
27      val timing = stop - start
28      if (timing.is_relevant) {
29        output(
30          (if (message == null || message == "") "" else message + ": ") +
31            timing.message + " elapsed time")
32      }
33
34      Exn.release(result)
35    }
36    else e
37  }
38}
39
40sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
41{
42  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
43  def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
44
45  def resources: Time = cpu + gc
46
47  def factor: Option[Double] =
48  {
49    val t1 = elapsed.seconds
50    val t2 = resources.seconds
51    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
52  }
53
54  def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
55
56  def message: String =
57    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
58
59  def message_resources: String =
60  {
61    val factor_text =
62      factor match {
63        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
64        case None => ""
65      }
66    if (resources.seconds >= 3.0)
67      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
68    else
69      elapsed.message_hms + " elapsed time" + factor_text
70  }
71
72  override def toString: String = message
73
74  def json: JSON.Object.T =
75    JSON.Object("elapsed" -> elapsed.seconds, "cpu" -> cpu.seconds, "gc" -> gc.seconds)
76}
77