Quelle Profiling.thy Sprache: Isabelle

(*  Title:      Tools/profiling.thy
    Author:     Makarius

Session profiling based on loaded ML image.
*)

theory Profiling
  imports Pure
begin

ML \<open>
signature PROFILING =
sig
  val locales: theory -> string list
  val locale_thms: theory -> string -> thm list
  val locales_thms: theory -> thm list
  val global_thms: theory -> thm list
  val all_thms: theory -> thm list
  type session_statistics =
   {theories: int,
    garbage_theories: int,
    locales: int,
    locale_thms: int,
    global_thms: int,
    sizeof_thys_id: int,
    sizeof_thms_id: int,
    sizeof_terms: int,
    sizeof_types: int,
    sizeof_names: int,
    sizeof_spaces: int}
  val session_statistics: string list -> session_statistics
  val main: unit -> unit
end;

structure Profiling: PROFILING =
struct

(* theory content *)

fun locales thy =
  let
    val parent_spaces = map Locale.locale_space (Theory.parents_of thy);
    fun add name =
      if exists (fn space => Name_Space.declared space name) parent_spaces then I
      else cons name;
  in fold add (Locale.get_locales thy) [] end;

fun proper_thm thm = not (Thm.eq_thm_prop (Drule.dummy_thm, thm));

fun locale_thms thy loc =
  (Locale.locale_notes thy loc, []) |->
    (fold (#2 #> fold (#2 #> (fold (#1 #> fold (fn thm => proper_thm thm ? cons thm ))))));

fun locales_thms thy =
  maps (locale_thms thy) (locales thy);

fun global_thms thy =
  Facts.dest_static true
    (map Global_Theory.facts_of (Theory.parents_of thy)) (Global_Theory.facts_of thy)
  |> maps #2;

fun all_thms thy = locales_thms thy @ global_thms thy;

(* session content *)

fun session_content thys =
  let
    val thms = maps all_thms thys;
    val thys_id = map Context.theory_id thys;
    val thms_id = map Thm.theory_id thms;
    val terms =
      Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty);
    val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty);
    val spaces =
      maps (fn f => map f thys)
       [Sign.class_space,
        Sign.type_space,
        Sign.const_space,
        Theory.axiom_space,
        Thm.oracle_space,
        Global_Theory.fact_space,
        Locale.locale_space,
        Attrib.attribute_space o Context.Theory,
        Method.method_space o Context.Theory];
     val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces));
  in
    {thys_id = thys_id, thms_id = thms_id, terms = terms,
      types = types, names = names, spaces = spaces}
  end;

fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b;
fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b;
fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b;

(* session statistics *)

type session_statistics =
{theories: int,
  garbage_theories: int,
  locales: int,
  locale_thms: int,
  global_thms: int,
  sizeof_thys_id: int,
  sizeof_thms_id: int,
  sizeof_terms: int,
  sizeof_types: int,
  sizeof_names: int,
  sizeof_spaces: int};

fun session_statistics theories : session_statistics =
  let
    val theories_member = Symtab.defined (Symtab.make_set theories) o Context.theory_long_name;

    val context_thys =
      #contexts (Context.finish_tracing ())
      |> map_filter (fn (Context.Theory thy, _) => SOME thy | _ => NONE);

    val loader_thys = map Thy_Info.get_theory (Thy_Info.get_names ());
    val loaded_thys = filter theories_member loader_thys;
    val loaded_context_thys = filter theories_member context_thys;

    val all_thys = loader_thys @ context_thys;
    val base_thys = filter_out theories_member all_thys;

    val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms,
          types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys;
    val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms,
          types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys;

    val n = length loaded_thys;
    val m = (case length loaded_context_thys of 0 => 0 | l => l - n);
  in
    {theories = n,
     garbage_theories = m,
     locales = Integer.sum (map (length o locales) loaded_thys),
     locale_thms = Integer.sum (map (length o locales_thms) loaded_thys),
     global_thms = Integer.sum (map (length o global_thms) loaded_thys),
     sizeof_thys_id =
      sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) -
        sizeof_list_diff (all_thys_id, base_thys_id),
     sizeof_thms_id =
      sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) -
        sizeof_list_diff (all_thms_id, base_thms_id),
     sizeof_terms =
      sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) -
        sizeof_list_diff (all_terms, base_terms),
     sizeof_types =
      sizeof1_diff ((all_types, all_names), (base_types, all_names)) -
        sizeof_list_diff (all_types, base_types),
     sizeof_spaces =
      sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) -
        sizeof_list_diff (all_spaces, base_spaces),
     sizeof_names = sizeof_diff (all_names, base_names)}
  end;

(* main entry point for external process *)

local

val decode_args : string list XML.Decode.T =
  let open XML.Decode in list string end;

val encode_result : session_statistics XML.Encode.T =
  (fn {theories = a,
       garbage_theories = b,
       locales = c,
       locale_thms = d,
       global_thms = e,
       sizeof_thys_id = f,
       sizeof_thms_id = g,
       sizeof_terms = h,
       sizeof_types = i,
       sizeof_names = j,
       sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #>
  let open XML.Encode in
    pair int (pair int (pair int (pair int (pair int (pair int (pair int
      (pair int (pair int (pair int int)))))))))
  end;

in

fun main () =
  (case Options.default_string \<^system_option>\<open>profiling_dir\<close> of
    "" => ()
  | dir_name =>
      let
        val dir = Path.explode dir_name;
        val args = decode_args (YXML.parse_body (File.read (dir + \<^path>\<open>args.yxml\<close>)));
        val result = session_statistics args;
      in File.write (dir + \<^path>\<open>result.yxml\<close>) (YXML.string_of_body (encode_result result)) end);

end;

end;
\<close>

ML_command \<open>Profiling.main ()\<close>

end

quality99%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

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:

Die farbliche Syntaxdarstellung ist noch experimentell.