src/Pure/General/timing.scala
author wenzelm
Sun, 30 Jan 2011 13:02:18 +0100
changeset 41648 6d736d983d5c
parent 40852 aee98c88c587
child 44699 5199ee17c7d7
permissions -rw-r--r--
clarified example settings for Proof General;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/timing.scala
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     3
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     4
Basic support for time measurement.
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     5
*/
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     6
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
     8
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
     9
object Time
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    10
{
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    11
  def seconds(s: Double): Time = new Time((s * 1000.0) round)
40393
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    12
}
2bb7ec08574a somewhat more uniform timing in ML vs. Scala;
wenzelm
parents:
diff changeset
    13
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    14
class Time(val ms: Long)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    15
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    16
  def seconds: Double = ms / 1000.0
40852
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    17
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    18
  def min(t: Time): Time = if (ms < t.ms) this else t
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    19
  def max(t: Time): Time = if (ms > t.ms) this else t
aee98c88c587 builtin time bounds (again);
wenzelm
parents: 40848
diff changeset
    20
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    21
  override def toString =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    22
    String.format(java.util.Locale.ROOT, "%.3f", seconds.asInstanceOf[AnyRef])
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    23
  def message: String = toString + "s"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    24
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    25
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    26
class Timing(val elapsed: Time, val cpu: Time, val gc: Time)
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    27
{
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    28
  def message: String =
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    29
    elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    30
  override def toString = message
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    31
}
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40393
diff changeset
    32