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