# HG changeset patch # User nipkow # Date 1255875959 -7200 # Node ID b6ba8adc14c270a1c17b94003eb10c70f76b5d7c # Parent c28279b29ff1c71819f94ff1c1517138b88ac2cb# Parent 717680b140418ab051879c40485ff764b0195d3a merged diff -r c28279b29ff1 -r b6ba8adc14c2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Oct 18 12:07:56 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun Oct 18 16:25:59 2009 +0200 @@ -35,8 +35,7 @@ proofs: int, time: int, timeout: int, - lemmas: int, - max_lems: int, + lemmas: int * int * int, posns: Position.T list } @@ -59,15 +58,15 @@ fun make_min_data (succs, ab_ratios, it_ratios) = MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios} -fun make_me_data (calls,success,proofs,time,timeout,lemmas,max_lems,posns) = +fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) = MeData{calls=calls, success=success, proofs=proofs, time=time, - timeout=timeout, lemmas=lemmas, max_lems=max_lems, posns=posns} + timeout=timeout, lemmas=lemmas, posns=posns} val empty_data = Data(make_sh_data (0, 0, 0, 0, 0, 0, 0), - make_me_data(0, 0, 0, 0, 0, 0, 0, []), + make_me_data(0, 0, 0, 0, 0, (0,0,0), []), MinData{succs=0, ab_ratios=0, it_ratios=0}, - make_me_data(0, 0, 0, 0, 0, 0, 0, [])) + make_me_data(0, 0, 0, 0, 0, (0,0,0), [])) fun map_sh_data f (Data(ShData{calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail}, @@ -80,11 +79,13 @@ (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) = Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda) -fun map_me_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,max_lems,posns}, minda, meda)) = - Data(shda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,max_lems,posns)), minda, meda) +fun map_me_data0 f (Data (shda, MeData{calls,success,proofs,time,timeout,lemmas,posns}, minda, meda)) = + Data(shda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns)), minda, meda) -fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,max_lems,posns})) = - Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,max_lems,posns))) +fun map_me_data f (Data (shda, meda0, minda, MeData{calls,success,proofs,time,timeout,lemmas,posns})) = + Data(shda, meda0, minda, make_me_data(f (calls,success,proofs,time,timeout,lemmas,posns))) + +fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n)); val inc_sh_calls = map_sh_data (fn (calls, success, lemmas,max_lems, time_isa, time_atp, time_atp_fail) @@ -124,68 +125,60 @@ (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) val inc_metis_calls = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls + 1, success, proofs, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls + 1, success, proofs, time, timeout, lemmas,posns)) val inc_metis_success = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success + 1, proofs, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success + 1, proofs, time, timeout, lemmas,posns)) val inc_metis_proofs = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs + 1, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs + 1, time, timeout, lemmas,posns)) fun inc_metis_time t = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time + t, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time + t, timeout, lemmas,posns)) val inc_metis_timeout = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout + 1, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout + 1, lemmas,posns)) fun inc_metis_lemmas n = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout, lemmas+n, max_lems, posns)) - -fun inc_metis_max_lems n = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls,success,proofs,time,timeout,lemmas,Int.max(max_lems,n), posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_metis_posns pos = map_me_data - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout, lemmas,max_lems, pos::posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, lemmas, pos::posns)) val inc_metis_calls0 = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls + 1, success, proofs, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls + 1, success, proofs, time, timeout, lemmas,posns)) val inc_metis_success0 = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success + 1, proofs, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success + 1, proofs, time, timeout, lemmas,posns)) val inc_metis_proofs0 = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs + 1, time, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs + 1, time, timeout, lemmas,posns)) fun inc_metis_time0 t = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time + t, timeout, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time + t, timeout, lemmas,posns)) val inc_metis_timeout0 = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout + 1, lemmas,max_lems,posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout + 1, lemmas,posns)) fun inc_metis_lemmas0 n = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout, lemmas+n, max_lems, posns)) - -fun inc_metis_max_lems0 n = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls,success,proofs,time,timeout,lemmas,Int.max(max_lems,n), posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, inc_max n lemmas, posns)) fun inc_metis_posns0 pos = map_me_data0 - (fn (calls,success,proofs,time,timeout,lemmas,max_lems,posns) - => (calls, success, proofs, time, timeout, lemmas,max_lems, pos::posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, lemmas, pos::posns)) local @@ -219,15 +212,16 @@ in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time - metis_timeout metis_lemmas metis_max_lems metis_posns = + metis_timeout (lemmas, lems_sos, lems_max) metis_posns = (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success ^ " (proof: " ^ str metis_proofs ^ ")"); log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout); log ("Success rate: " ^ percentage metis_success sh_calls ^ "%"); - log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas); - log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str metis_max_lems); - log ("Total time for successful metis calls: " ^ str3 (time metis_time)); + log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str lemmas); + log ("SOS of successful " ^ tag ^ "metis lemmas: " ^ str lems_sos); + log ("Max number of successful " ^ tag ^ "metis lemmas: " ^ str lems_max); + log ("Total time for successful " ^ tag ^ "metis calls: " ^ str3 (time metis_time)); log ("Average time for successful metis calls: " ^ str3 (avg_time metis_time metis_success)); if tag="" @@ -248,23 +242,23 @@ time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0, proofs=metis_proofs0, success=metis_success0, time=metis_time0, timeout=metis_timeout0, - lemmas=metis_lemmas0,max_lems=metis_max_lems0,posns=metis_posns0}, + lemmas=metis_lemmas0, posns=metis_posns0}, MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios}, MeData{calls=metis_calls, proofs=metis_proofs, success=metis_success, time=metis_time, timeout=metis_timeout, - lemmas=metis_lemmas,max_lems=metis_max_lems,posns=metis_posns})) = + lemmas=metis_lemmas, posns=metis_posns})) = if sh_calls > 0 then (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n"); log_sh_data log sh_calls sh_success sh_lemmas sh_max_lems sh_time_isa sh_time_atp sh_time_atp_fail; log ""; if metis_calls > 0 then log_metis_data log "" sh_calls sh_success metis_calls - metis_success metis_proofs metis_time metis_timeout metis_lemmas metis_max_lems metis_posns else (); + metis_success metis_proofs metis_time metis_timeout metis_lemmas metis_posns else (); log ""; if metis_calls0 > 0 then (log_min_data log min_succs ab_ratios it_ratios; log ""; log_metis_data log "unminimized " sh_calls sh_success metis_calls0 - metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_max_lems0 metis_posns0) + metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0) else () ) else () @@ -392,7 +386,7 @@ fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout, - inc_metis_lemmas, inc_metis_max_lems, inc_metis_posns) args name named_thms id + inc_metis_lemmas, inc_metis_posns) args name named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let fun metis thms ctxt = MetisTools.metis_tac ctxt thms @@ -401,7 +395,6 @@ fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data id inc_metis_success; change_data id (inc_metis_lemmas (length named_thms)); - change_data id (inc_metis_max_lems (length named_thms)); change_data id (inc_metis_time t); change_data id (inc_metis_posns pos); if name = "proof" then change_data id inc_metis_proofs else (); @@ -424,9 +417,9 @@ then () else let val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, - inc_metis_timeout, inc_metis_lemmas, inc_metis_max_lems, inc_metis_posns) + inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0, - inc_metis_timeout0, inc_metis_lemmas0, inc_metis_max_lems0, inc_metis_posns0) + inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0) val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option) val minimize = AList.defined (op =) args minimizeK in