1 (* Title: Tools/profiling.ML |
|
2 Author: Makarius |
|
3 |
|
4 Session profiling based on loaded ML image. |
|
5 *) |
|
6 |
|
7 signature PROFILING = |
|
8 sig |
|
9 val locales: theory -> string list |
|
10 val locale_thms: theory -> string -> thm list |
|
11 val locales_thms: theory -> thm list |
|
12 val global_thms: theory -> thm list |
|
13 val all_thms: theory -> thm list |
|
14 type session_statistics = |
|
15 {theories: int, |
|
16 garbage_theories: int, |
|
17 locales: int, |
|
18 locale_thms: int, |
|
19 global_thms: int, |
|
20 sizeof_thys_id: int, |
|
21 sizeof_thms_id: int, |
|
22 sizeof_terms: int, |
|
23 sizeof_types: int, |
|
24 sizeof_names: int, |
|
25 sizeof_spaces: int} |
|
26 val session_statistics: string list -> session_statistics |
|
27 val main: unit -> unit |
|
28 end; |
|
29 |
|
30 structure Profiling: PROFILING = |
|
31 struct |
|
32 |
|
33 (* theory content *) |
|
34 |
|
35 fun locales thy = |
|
36 let |
|
37 val parent_spaces = map Locale.locale_space (Theory.parents_of thy); |
|
38 fun add name = |
|
39 if exists (fn space => Name_Space.declared space name) parent_spaces then I |
|
40 else cons name; |
|
41 in fold add (Locale.get_locales thy) [] end; |
|
42 |
|
43 fun proper_thm thm = not (Thm.eq_thm_prop (Drule.dummy_thm, thm)); |
|
44 |
|
45 fun locale_thms thy loc = |
|
46 (Locale.locale_notes thy loc, []) |-> |
|
47 (fold (#2 #> fold (#2 #> (fold (#1 #> fold (fn thm => proper_thm thm ? cons thm )))))); |
|
48 |
|
49 fun locales_thms thy = |
|
50 maps (locale_thms thy) (locales thy); |
|
51 |
|
52 fun global_thms thy = |
|
53 Facts.dest_static true |
|
54 (map Global_Theory.facts_of (Theory.parents_of thy)) (Global_Theory.facts_of thy) |
|
55 |> maps #2; |
|
56 |
|
57 fun all_thms thy = locales_thms thy @ global_thms thy; |
|
58 |
|
59 |
|
60 (* session content *) |
|
61 |
|
62 fun session_content thys = |
|
63 let |
|
64 val thms = maps all_thms thys; |
|
65 val thys_id = map Context.theory_id thys; |
|
66 val thms_id = map Thm.theory_id thms; |
|
67 val terms = |
|
68 Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty); |
|
69 val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty); |
|
70 val spaces = |
|
71 maps (fn f => map f thys) |
|
72 [Sign.class_space, |
|
73 Sign.type_space, |
|
74 Sign.const_space, |
|
75 Theory.axiom_space, |
|
76 Thm.oracle_space, |
|
77 Global_Theory.fact_space, |
|
78 Locale.locale_space, |
|
79 Attrib.attribute_space o Context.Theory, |
|
80 Method.method_space o Context.Theory]; |
|
81 val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces)); |
|
82 in |
|
83 {thys_id = thys_id, thms_id = thms_id, terms = terms, |
|
84 types = types, names = names, spaces = spaces} |
|
85 end; |
|
86 |
|
87 fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b; |
|
88 fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b; |
|
89 fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b; |
|
90 |
|
91 |
|
92 (* session statistics *) |
|
93 |
|
94 type session_statistics = |
|
95 {theories: int, |
|
96 garbage_theories: int, |
|
97 locales: int, |
|
98 locale_thms: int, |
|
99 global_thms: int, |
|
100 sizeof_thys_id: int, |
|
101 sizeof_thms_id: int, |
|
102 sizeof_terms: int, |
|
103 sizeof_types: int, |
|
104 sizeof_names: int, |
|
105 sizeof_spaces: int}; |
|
106 |
|
107 fun session_statistics theories : session_statistics = |
|
108 let |
|
109 val theories_member = Symtab.defined (Symtab.make_set theories) o Context.theory_long_name; |
|
110 |
|
111 val context_thys = |
|
112 #contexts (Context.finish_tracing ()) |
|
113 |> map_filter (fn (Context.Theory thy, _) => SOME thy | _ => NONE); |
|
114 |
|
115 val loader_thys = map Thy_Info.get_theory (Thy_Info.get_names ()); |
|
116 val loaded_thys = filter theories_member loader_thys; |
|
117 val loaded_context_thys = filter theories_member context_thys; |
|
118 |
|
119 val all_thys = loader_thys @ context_thys; |
|
120 val base_thys = filter_out theories_member all_thys; |
|
121 |
|
122 val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms, |
|
123 types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys; |
|
124 val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms, |
|
125 types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys; |
|
126 |
|
127 val n = length loaded_thys; |
|
128 val m = (case length loaded_context_thys of 0 => 0 | l => l - n); |
|
129 in |
|
130 {theories = n, |
|
131 garbage_theories = m, |
|
132 locales = Integer.sum (map (length o locales) loaded_thys), |
|
133 locale_thms = Integer.sum (map (length o locales_thms) loaded_thys), |
|
134 global_thms = Integer.sum (map (length o global_thms) loaded_thys), |
|
135 sizeof_thys_id = |
|
136 sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) - |
|
137 sizeof_list_diff (all_thys_id, base_thys_id), |
|
138 sizeof_thms_id = |
|
139 sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) - |
|
140 sizeof_list_diff (all_thms_id, base_thms_id), |
|
141 sizeof_terms = |
|
142 sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) - |
|
143 sizeof_list_diff (all_terms, base_terms), |
|
144 sizeof_types = |
|
145 sizeof1_diff ((all_types, all_names), (base_types, all_names)) - |
|
146 sizeof_list_diff (all_types, base_types), |
|
147 sizeof_spaces = |
|
148 sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) - |
|
149 sizeof_list_diff (all_spaces, base_spaces), |
|
150 sizeof_names = sizeof_diff (all_names, base_names)} |
|
151 end; |
|
152 |
|
153 |
|
154 (* main entry point for external process *) |
|
155 |
|
156 local |
|
157 |
|
158 val decode_args : string list XML.Decode.T = |
|
159 let open XML.Decode in list string end; |
|
160 |
|
161 val encode_result : session_statistics XML.Encode.T = |
|
162 (fn {theories = a, |
|
163 garbage_theories = b, |
|
164 locales = c, |
|
165 locale_thms = d, |
|
166 global_thms = e, |
|
167 sizeof_thys_id = f, |
|
168 sizeof_thms_id = g, |
|
169 sizeof_terms = h, |
|
170 sizeof_types = i, |
|
171 sizeof_names = j, |
|
172 sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #> |
|
173 let open XML.Encode in |
|
174 pair int (pair int (pair int (pair int (pair int (pair int (pair int |
|
175 (pair int (pair int (pair int int))))))))) |
|
176 end; |
|
177 |
|
178 in |
|
179 |
|
180 fun main () = |
|
181 (case getenv "ISABELLE_PROFILING" of |
|
182 "" => () |
|
183 | dir_name => |
|
184 let |
|
185 val dir = Path.explode dir_name; |
|
186 val args = decode_args (YXML.parse_body (File.read (dir + \<^path>\<open>args.yxml\<close>))); |
|
187 val result = session_statistics args; |
|
188 in File.write (dir + \<^path>\<open>result.yxml\<close>) (YXML.string_of_body (encode_result result)) end); |
|
189 |
|
190 end; |
|
191 |
|
192 end; |
|