Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: timing.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/General/timing.ML
    Author:     Makarius

Basic support for time measurement.
*)

signature BASIC_TIMING =
sig
  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
  val timeit: (unit -> 'a) -> 'a
  val timeap: ('a -> 'b) -> 'a -> 'b
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
end

signature TIMING =
sig
  include BASIC_TIMING
  type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time}
  type start
  val start: unit -> start
  val result: start -> timing
  val timing: ('a -> 'b) -> 'a -> timing * 'b
  val is_relevant_time: Time.time -> bool
  val is_relevant: timing -> bool
  val message: timing -> string
  val protocol_message: string -> Position.T -> timing -> unit
  val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
end

structure Timing: TIMING =
struct

(* type timing *)

type timing = {elapsed: Time.time, cpu: Time.time, gc: Time.time};

(* timer control *)

abstype start = Start of
  Timer.real_timer * Time.time * Timer.cpu_timer *
    {gc: {sys: Time.time, usr: Time.time}, nongc: {sys: Time.time, usr: Time.time}}
with

fun start () =
  let
    val real_timer = Timer.startRealTimer ();
    val real_time = Timer.checkRealTimer real_timer;
    val cpu_timer = Timer.startCPUTimer ();
    val cpu_times = Timer.checkCPUTimes cpu_timer;
  in Start (real_timer, real_time, cpu_timer, cpu_times) end;

fun result (Start (real_timer, real_time, cpu_timer, cpu_times)) =
  let
    val real_time2 = Timer.checkRealTimer real_timer;
    val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
      Timer.checkCPUTimes cpu_timer;

    val elapsed = real_time2 - real_time;
    val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    val cpu = usr2 - usr + sys2 - sys + gc;
  in {elapsed = elapsed, cpu = cpu, gc = gc} end;

end;

fun timing f x =
  let
    val start = start ();
    val y = f x;
  in (result start, y) end;

(* timing messages *)

val min_time = Time.fromMilliseconds 1;

fun is_relevant_time time = time >= min_time;

fun is_relevant {elapsed, cpu, gc} =
  is_relevant_time elapsed orelse
  is_relevant_time cpu orelse
  is_relevant_time gc;

fun message {elapsed, cpu, gc} =
  Value.print_time elapsed ^ "s elapsed time, " ^
  Value.print_time cpu ^ "s cpu time, " ^
  Value.print_time gc ^ "s GC time" handle Time.Time => "";

fun cond_timeit enabled msg e =
  if enabled then
    let
      val (t, result) = timing (Exn.interruptible_capture e) ();
      val _ =
        if is_relevant t then
          let val end_msg = message t
          in warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg) end
        else ();
    in Exn.release result end
  else e ();

fun timeit e = cond_timeit true "" e;
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);

fun protocol_message name pos t =
  if is_relevant t then
    let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
    in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
  else ();

fun protocol name pos f x =
  let
    val (t, result) = timing (Exn.interruptible_capture f) x;
    val _ = protocol_message name pos t;
  in Exn.release result end;

end;

structure Basic_Timing: BASIC_TIMING = Timing;
open Basic_Timing;

¤ Dauer der Verarbeitung: 0.20 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.