1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11signature PROOF_METRICS =
12sig
13
14type metric_head = {proof_bottom : string list ,
15                    proof_top : string list,
16                    spec_theories : string list,
17                    toplevel_facts : string list,
18                    name  : string
19                   }
20
21type metric_configs = {min_proof_size : int,
22                       filter_locale_consts : bool,
23                       filter_kinds : Proof_Count.lemmaT list,
24                       thy_deps : (string * string list) Symtab.table,
25                       full_spec : Spec_Graph.entry Int_Graph.T,
26                       proof_spec : Proof_Graph.proof_entry String_Graph.T,
27                       base_path : string
28                      }
29
30
31val get_root_theories_of : (string * string list) Symtab.table -> (string -> string -> bool) -> string list
32
33val get_theories_from_range : (string * string list) Symtab.table -> string list * string list -> string list
34
35val compute_and_write_metrics : (metric_head * metric_configs) -> unit
36
37end
38
39structure Proof_Metrics : PROOF_METRICS =
40struct
41
42(*Truncate graphs to only discuss constants in mentioned theories*)
43
44fun theory_of (e : Spec_Graph.entry) = (Long_Name.explode #> hd) (#name e)
45
46fun filter_contains (spec : Spec_Graph.entry Int_Graph.T) theories =
47  Proof_Graph.map_contains (filter (fn id => (member (op =) theories) (theory_of (Int_Graph.get_node spec id))))
48
49(* Connect child and parent nodes before removing them, preserving connectedness. *)
50
51fun truncate_proof_spec spec_theories proof_theories spec proof_spec = proof_spec
52|> Proof_Graph.restrict_subgraph (fn (nm,e) =>
53  (member (op =) proof_theories ((Long_Name.explode #> hd) nm))
54  andalso (not (#lines e = (~1,~1))))
55|> String_Graph.map (K(filter_contains spec spec_theories))
56
57
58fun get_proof_metrics (proof_spec : Proof_Graph.proof_entry String_Graph.T) =
59let
60
61  fun all_sucs i  = String_Graph.all_succs proof_spec [i]
62
63(*Avoid double-counting multi-lemmas*)
64  fun get_proper_deps i = fold (fn j => let val e = String_Graph.get_node proof_spec j in Symtab.insert_list (op =) (#file e,#lines e) end) (all_sucs i) Symtab.empty
65    |> Symtab.dest_list
66    |> map (fn (_,(a,b)) => (b - a) + 1)
67
68  fun collate_metrics i = (i,{total_size = get_proper_deps i |> Integer.sum})
69
70in map collate_metrics (String_Graph.keys proof_spec) |> Symtab.make end
71
72fun filter_all_deps thy_deps (thys as (_ :: _)) =
73  let
74    val all_deps = fold (fn thy => union (op =) (Symtab.lookup thy_deps thy |> the |> snd)) thys []
75  in
76    filter (member (op =) all_deps)
77  end
78  | filter_all_deps _ [] = I
79
80fun get_theories_from_range thy_deps (bottom_theories as _ :: _,top_theories) = Proof_Graph.proper_theory_list thy_deps bottom_theories
81    |> filter_out (member (op =) (Proof_Graph.proper_theory_list thy_deps top_theories))
82    |> (filter_all_deps thy_deps top_theories)
83    |> union (op =) top_theories
84  | get_theories_from_range thy_deps ([],_) = Symtab.dest thy_deps |> map fst
85
86fun toplevel_parent g nm =
87let
88  val preds = String_Graph.all_preds g [nm]
89  val ppreds = map (fn i => `(String_Graph.immediate_preds g) i) preds
90in
91  find_first (null o fst) ppreds |> Option.map snd end
92
93
94
95(* Note if the top of a spec or proof range is empty, this will encompass
96   all known theories which depend on the bottom of the range *)
97
98type metric_head = {proof_bottom : string list ,
99                    proof_top : string list,
100                    spec_theories : string list,
101                    toplevel_facts : string list,
102                    name  : string
103                   }
104
105type metric_configs = {min_proof_size : int,
106                       filter_locale_consts : bool,
107                       filter_kinds : Proof_Count.lemmaT list,
108                       thy_deps : (string * string list) Symtab.table,
109                       full_spec : Spec_Graph.entry Int_Graph.T,
110                       proof_spec : Proof_Graph.proof_entry String_Graph.T,
111                       base_path : string
112                      }
113
114
115(* toplevel_facts are those whose dependencies actually show up in the final data.
116   If it is empty then all facts are included *)
117
118fun compute_and_write_metrics (header : metric_head,(args : metric_configs)) =
119let
120
121  val toplevel_facts = #toplevel_facts header
122  val name = #name header
123  val proof_spec' = #proof_spec args
124  val full_spec = #full_spec args
125  val base_path = #base_path args
126  val thy_deps = #thy_deps args
127
128  val _ =  (#spec_theories header) @ (#proof_bottom header) @ (#proof_top header)
129    |> map (fn s => Symtab.defined thy_deps s orelse error ("Unknown theory: " ^ s))
130
131  val _ = tracing "Truncating proof spec..."
132
133  val spec_theories = get_theories_from_range thy_deps ((#spec_theories header,[]))
134  val proof_theories = get_theories_from_range thy_deps (#proof_bottom header,#proof_top header)
135
136
137  val proof_spec = (truncate_proof_spec spec_theories proof_theories full_spec proof_spec')
138
139  val all_deps = case toplevel_facts of [] => String_Graph.keys proof_spec
140  | _ => String_Graph.all_succs proof_spec toplevel_facts handle String_Graph.UNDEF x =>
141    error ("Couldn't find fact " ^ x ^ " in known facts.\n" ^ (@{make_string} proof_theories))
142
143  val _ = tracing "Calculating spec metrics..."
144
145  val all_defs = Int_Graph.fold (fn (_,(e,_)) => (case (#def_name e) of SOME d => Symtab.update (d,()) | NONE => I)) full_spec Symtab.empty
146
147  val _ = tracing "Calculating proof metrics..."
148
149  val proof_metrics = get_proof_metrics proof_spec
150
151  val lemma_defs = String_Graph.fold (fn (nm,_) =>
152    Symtab.update (nm,String_Graph.all_succs proof_spec' [nm] |> filter (Symtab.defined all_defs))) proof_spec Symtab.empty
153
154  val _ = tracing "done"
155
156type metric_entry = {
157                      spec_size : int,
158                      ideal_spec_size : int,
159                      fact_size : int,
160                      consts : int list,
161                      use_consts : int list
162                    }
163
164
165fun write_metrics measure_name =
166  let
167    fun filter_deps (nm,_) = if toplevel_facts = [] then true else member (op =) all_deps nm
168
169    fun filter_kinds (nm,_) =  ((member (op =) (map SOME (#filter_kinds args)) (#kind (String_Graph.get_node proof_spec nm))))
170
171    fun filter_size (_,t) = (#total_size t) > (#min_proof_size args)
172
173    fun is_used fact_defs i =
174        let
175          val e = (Int_Graph.get_node full_spec i)
176        in
177          case (#def_name e) of NONE => true |
178          SOME d => (case (#spec_type e) of
179            Spec_Graph.Constructor => true
180            | Spec_Graph.Case => true
181            | _ =>  (member (op =) fact_defs d))
182        end
183
184
185   fun is_in_theory i = member (op =) spec_theories (Int_Graph.get_node full_spec i |> theory_of)
186
187   fun is_locale i = Int_Graph.get_node full_spec i |> #spec_type
188    |> (fn Spec_Graph.Locale => true | _ => false)
189
190     fun final_entry (fact_id,metric_entry) =
191      let
192        val proof_entry = String_Graph.get_node proof_spec fact_id
193
194        val fact_defs = Symtab.lookup lemma_defs fact_id |> the
195
196      val prems = flat (#prems proof_entry)
197      |> (#filter_locale_consts args) ? filter (not o is_locale)
198
199       val consts = #concl proof_entry @ prems
200
201        fun proper_sucs spec consts = consts
202          |> Int_Graph.all_succs spec
203          |> filter is_in_theory
204
205
206        val all_consts = proper_sucs full_spec consts
207
208        val all_used_consts = filter (is_used fact_defs) all_consts
209
210        val result = {
211                       spec_size = length all_consts,
212                       ideal_spec_size = length all_used_consts,
213                       fact_size = #total_size metric_entry,
214                       consts = all_consts,
215                       ideal_consts = all_used_consts
216                     }
217      in
218        (fact_id,result) end
219
220
221    val filtered =
222    let
223    in
224      proof_metrics |> Symtab.dest
225      |> filter filter_deps
226      |> filter filter_kinds
227      |> filter filter_size
228       end
229
230    val paired = Par_List.map final_entry filtered
231
232    fun mk_string (fact_id,{spec_size,ideal_spec_size,fact_size,...}) = fact_id ^ " " ^
233      (Int.toString spec_size) ^ " " ^
234      (Int.toString ideal_spec_size) ^
235      " " ^ (Int.toString fact_size) ^  "\n"
236
237    val buf = Buffer.empty
238    |> fold (fn e => Buffer.add (mk_string e)) paired
239
240  in
241    (File.write_buffer (Path.explode (base_path ^ "/metrics_" ^ name ^ "_" ^ measure_name ^ ".txt")) buf;(filtered,paired)) end
242
243
244val (filtered_num_deps,paired_num_deps) = write_metrics "num_deps";
245
246val _ = not (null filtered_num_deps) orelse error "No facts were counted. Check theory ranges."
247
248fun add_top_report thm buf =
249let
250  val {fact_size, spec_size, ideal_spec_size, consts,ideal_consts,...} = AList.lookup (op =) paired_num_deps thm |> the
251
252  val redundant_consts = subtract (op =) ideal_consts consts
253    |> map (fn i => Int_Graph.get_node full_spec i |> #name)
254in
255  buf
256  |> Buffer.add ("Toplevel lemma: " ^ thm ^ " with " ^ (Int.toString fact_size)
257                  ^ " lines of proof, " ^ Int.toString spec_size ^ " specification size and "
258                  ^ Int.toString ideal_spec_size ^ " ideal specification size\n")
259  |> Buffer.add ("Redundant Toplevel Constants: " ^ (String.concatWith "\n" redundant_consts) ^ "\n")
260 end
261
262  val (largestp,_) = fold (fn (id,e) => fn (id',e') => if (#total_size e) > (#total_size e') then (id,e) else (id',e')) filtered_num_deps (filtered_num_deps |> hd)
263
264fun add_top_reports buf = buf
265    |> Buffer.add "Giving largest measured proof.\n"
266    |> add_top_report largestp
267
268(* Total number of unique lines from all dependencies. *)
269val full_size = fold (fn j => let val e = String_Graph.get_node proof_spec j in Symtab.insert_list (op =) (#file e,#lines e) end) all_deps Symtab.empty
270    |> Symtab.dest_list
271    |> map (fn (_,(a,b)) => (b - a) + 1)
272    |> Integer.sum
273
274fun toString_commas i=
275  Int.toString i
276    |> String.explode
277    |> rev
278    |> chop_groups 3
279    |> map (String.implode o rev)
280    |> rev
281    |> String.concatWith ","
282
283fun latex_report thm =
284  let
285    val {spec_size,ideal_spec_size,fact_size,...} = AList.lookup (op =) paired_num_deps thm |> the
286    fun mk_command inm i = Buffer.add ("\\newcommand{\\" ^ name ^ inm ^ "}{" ^ i ^ "\\xspace}\n")
287 in
288    Buffer.empty
289    |> mk_command "NumDeps" (toString_commas spec_size)
290    |> mk_command "IdealNumDeps" (toString_commas ideal_spec_size)
291    |> mk_command "Lines" (toString_commas fact_size)
292    |> mk_command "AllLines" (toString_commas full_size)
293 end
294
295val orphaned = subtract (op =) all_deps (String_Graph.keys proof_spec)
296val parents = map (the_default "" o toplevel_parent proof_spec) orphaned
297
298val buf = fold2 (fn or => fn p => Buffer.add (or ^ " -> " ^ p ^ "\n")) orphaned parents Buffer.empty
299
300val _ = (File.write_buffer (Path.explode (base_path ^ "/" ^ name ^ "_orphans.txt")) buf)
301
302
303  val buf = Buffer.empty
304  |> Buffer.add ("Total number of facts plotted: " ^ (toString_commas (length paired_num_deps)) ^ "\n")
305  |> Buffer.add ("Total size of all facts: \n")
306  |> Buffer.add (Int.toString full_size)
307  |> Buffer.add ("\n")
308  |> add_top_reports
309  |> Buffer.add ("Unused lemmas: " ^ (toString_commas (length orphaned)) ^ "\n")
310  |> Buffer.add ("Proof Theories: \n")
311  |> fold (Buffer.add "\n" oo Buffer.add) proof_theories
312  |> Buffer.add "\n"
313  |> Buffer.add ("Spec Theories: \n")
314  |> fold (Buffer.add "\n" oo Buffer.add) spec_theories
315  |> Buffer.add "\n"
316
317val _ = File.write_buffer (Path.explode (base_path ^ "/" ^ name ^ "_report.txt")) buf
318
319val _ = File.write_buffer (Path.explode (base_path ^ "/" ^ name ^ "_summary.tex")) (latex_report largestp)
320
321val _ = (proof_spec,proof_metrics,filtered_num_deps,paired_num_deps,lemma_defs)
322
323in () end
324
325fun get_root_theories_of thy_deps f =
326let
327  val thy_graph = thy_deps
328  |> Symtab.dest
329  |> map (fn (nm,(i,es)) => ((nm,i),es))
330  |> String_Graph.make
331  |> (fn g => String_Graph.restrict (fn k => f k (String_Graph.get_node g k)) g)
332  |> String_Graph.dest
333  |> map_filter (fn ((nm,_),es) => if es = [nm] then SOME nm else NONE)
334in
335  thy_graph
336end
337
338end
339