more accurate output of Thm_Name.T wrt. facts name space;
(* Title: Tools/profiling.ML
Author: Makarius
Session profiling based on loaded ML image.
*)
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 getenv "ISABELLE_PROFILING" 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;