Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Pure/ML/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 2 kB image not shown  

Quellcode-Bibliothek ml_profiling.ML   Sprache: SML

 
(*  Title:      Pure/ML/ml_profiling.ML
    Author:     Makarius

ML profiling (via Poly/ML run-time system).
*)


signature BASIC_ML_PROFILING =
sig
  val profile_time: ('a -> 'b) -> 'a -> 'b
  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
  val profile_allocations: ('a -> 'b) -> 'a -> 'b
end;

signature ML_PROFILING =
sig
  val check_mode: string -> unit
  val profile: string -> ('a -> 'b) -> 'a -> 'b
  include BASIC_ML_PROFILING
end;

structure ML_Profiling: ML_PROFILING =
struct

(* mode *)

val modes =
  Symtab.make
    [("time", PolyML.Profiling.ProfileTime),
     ("time_thread", PolyML.Profiling.ProfileTimeThisThread),
     ("allocations", PolyML.Profiling.ProfileAllocations)];

fun get_mode kind =
  (case Symtab.lookup modes kind of
    SOME mode => mode
  | NONE => error ("Bad profiling mode: " ^ quote kind));

fun check_mode "" = ()
  | check_mode kind = ignore (get_mode kind);


(* profile *)

fun print_entry count name =
  let
    val c = string_of_int count;
    val prefix = Symbol.spaces (Int.max (0, 12 - size c));
  in prefix ^ c ^ " " ^ name end;

fun profile "" f x = f x
  | profile kind f x =
      let
        val mode = get_mode kind;
        fun output entries =
          (case fold (curry (op +) o fst) entries 0 of
            0 => ()
          | total =>
              let
                val body = entries
                  |> sort (int_ord o apply2 fst)
                  |> map (fn (count, name) =>
                      let val markup = Markup.ML_profiling_entry {name = name, count = count}
                      in XML.Elem (markup, [XML.Text (print_entry count name ^ "\n")]) end);
                val head = XML.Text ("profile_" ^ kind ^ ":\n");
                val foot = XML.Text (print_entry total "TOTAL");
                val msg = XML.Elem (Markup.ML_profiling kind, head :: body @ [foot]);
              in tracing (YXML.string_of msg) end);
      in PolyML.Profiling.profileStream output mode f x end;

fun profile_time f = profile "time" f;
fun profile_time_thread f = profile "time_thread" f;
fun profile_allocations f = profile "allocations" f;

end;

structure Basic_ML_Profiling: BASIC_ML_PROFILING = ML_Profiling;
open Basic_ML_Profiling;

100%


¤ 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.0.14Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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:

sprechenden Kalenders