# HG changeset patch # User nipkow # Date 1253805965 -7200 # Node ID 8854e892cf3eaa308c0f5837c6bcbc3af114846d # Parent 5fe601aff9bec26a770cf942310edeb659c00d8f# Parent b1c85a117dec706f372158e1f96bd6872014ebcb merged diff -r 5fe601aff9be -r 8854e892cf3e src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 24 15:00:17 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Sep 24 17:26:05 2009 +0200 @@ -16,7 +16,7 @@ type done_args = {last: Toplevel.state, log: string -> unit} type done_action = int -> done_args -> unit type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T} + timeout: Time.time, log: string -> unit, pos: Position.T, name: string} type run_action = int -> run_args -> unit type action = init_action * run_action * done_action val catch : (int -> string) -> run_action -> run_action @@ -56,7 +56,7 @@ type done_args = {last: Toplevel.state, log: string -> unit} type done_action = int -> done_args -> unit type run_args = {pre: Proof.state, post: Toplevel.state option, - timeout: Time.time, log: string -> unit, pos: Position.T} + timeout: Time.time, log: string -> unit, pos: Position.T, name: string} type run_action = int -> run_args -> unit type action = init_action * run_action * done_action @@ -95,9 +95,9 @@ fun log_sep thy = log thy "------------------" -fun apply_actions thy pos info (pre, post, time) actions = +fun apply_actions thy pos name info (pre, post, time) actions = let - fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos} + fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} fun run (id, run, _) = (apply (run id); log_sep thy) in (log thy info; log_sep thy; List.app run actions) end @@ -121,7 +121,7 @@ val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" in - only_within_range thy pos (apply_actions thy pos info st) (Actions.get thy) + only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) end fun done_actions st = diff -r 5fe601aff9be -r 8854e892cf3e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 24 15:00:17 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Sep 24 17:26:05 2009 +0200 @@ -31,6 +31,7 @@ datatype me_data = MeData of { calls: int, success: int, + proofs: int, time: int, timeout: int, lemmas: int, @@ -55,14 +56,14 @@ 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, time, timeout, lemmas, posns) = - MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=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, posns=posns} val empty_data = Data(make_sh_data (0, 0, 0, 0, 0, 0), - make_me_data(0, 0, 0, 0, 0, []), + make_me_data(0, 0, 0, 0, 0, 0, []), MinData{succs=0, ab_ratios=0, it_ratios=0}, - make_me_data(0, 0, 0, 0, 0, [])) + make_me_data(0, 0, 0, 0, 0, 0, [])) fun map_sh_data f (Data (ShData{calls, success, lemmas, time_isa, time_atp, time_atp_fail}, meda0, minda, meda)) = @@ -73,11 +74,11 @@ (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,time,timeout,lemmas,posns}, minda, meda)) = - Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,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,time,timeout,lemmas,posns})) = - Data(shda, meda0, minda, make_me_data(f (calls,success,time,timeout,lemmas,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))) val inc_sh_calls = map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail) @@ -113,52 +114,60 @@ map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r)) val inc_metis_calls = map_me_data - (fn (calls, success, time, timeout, lemmas,posns) - => (calls + 1, success, time, timeout, lemmas,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,time,timeout,lemmas,posns) - => (calls, success + 1, time, timeout, lemmas,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,posns) + => (calls, success, proofs + 1, time, timeout, lemmas,posns)) fun inc_metis_time t = map_me_data - (fn (calls,success,time,timeout,lemmas,posns) - => (calls, success, time + t, timeout, lemmas,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,time,timeout,lemmas,posns) - => (calls, success, time, timeout + 1, lemmas,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,time,timeout,lemmas,posns) - => (calls, success, time, timeout, lemmas + n, posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, lemmas + n, posns)) fun inc_metis_posns pos = map_me_data - (fn (calls,success,time,timeout,lemmas,posns) - => (calls, success, time, timeout, lemmas, 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, time, timeout, lemmas,posns) - => (calls + 1, success, time, timeout, lemmas,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,time,timeout,lemmas,posns) - => (calls, success + 1, time, timeout, lemmas,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,posns) + => (calls, success, proofs + 1, time, timeout, lemmas,posns)) fun inc_metis_time0 t = map_me_data0 - (fn (calls,success,time,timeout,lemmas,posns) - => (calls, success, time + t, timeout, lemmas,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,time,timeout,lemmas,posns) - => (calls, success, time, timeout + 1, lemmas,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,time,timeout,lemmas,posns) - => (calls, success, time, timeout, lemmas + n, posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, lemmas + n, posns)) fun inc_metis_posns0 pos = map_me_data0 - (fn (calls,success,time,timeout,lemmas,posns) - => (calls, success, time, timeout, lemmas, pos::posns)) + (fn (calls,success,proofs,time,timeout,lemmas,posns) + => (calls, success, proofs, time, timeout, lemmas, pos::posns)) local @@ -190,10 +199,10 @@ let val str0 = string_of_int o the_default 0 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_time +fun log_metis_data log tag sh_calls sh_success metis_calls metis_success metis_proofs metis_time metis_timeout metis_lemmas metis_posns = (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls); - log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success); + 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); @@ -216,11 +225,11 @@ fun log_data id log (Data (ShData{calls=sh_calls, lemmas=sh_lemmas, success=sh_success, time_isa=sh_time_isa,time_atp=sh_time_atp,time_atp_fail=sh_time_atp_fail}, - MeData{calls=metis_calls0, + MeData{calls=metis_calls0, proofs=metis_proofs0, success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0,posns=metis_posns0}, MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios}, - MeData{calls=metis_calls, + MeData{calls=metis_calls, proofs=metis_proofs, success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) = if sh_calls > 0 @@ -229,12 +238,12 @@ log_sh_data log sh_calls sh_success sh_lemmas 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_time metis_timeout metis_lemmas 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_time0 metis_timeout0 metis_lemmas0 metis_posns0) + metis_success0 metis_proofs0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0) else () ) else () @@ -376,8 +385,8 @@ end -fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, - inc_metis_lemmas, inc_metis_posns) args named_thms id +fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout, + 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 @@ -388,6 +397,7 @@ change_data id (inc_metis_lemmas (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 (); "succeeded (" ^ string_of_int t ^ ")") fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms) handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout") @@ -401,13 +411,13 @@ |> log o prefix (metis_tag id) end -fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) = +fun sledgehammer_action args id (st as {log, pre, name, ...}: Mirabelle.run_args) = if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre)))) then () else let - val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, + val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_proofs, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) - val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, + val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_proofs0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0) val named_thms = ref (NONE : (string * thm list) list option) val minimize = AList.defined (op =) args minimizeK @@ -416,12 +426,12 @@ if is_some (!named_thms) then (if minimize - then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st + then Mirabelle.catch metis_tag (run_metis metis0_fns args name (these (!named_thms))) id st else (); if minimize andalso not(null(these(!named_thms))) then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st else (); - Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st) + Mirabelle.catch metis_tag (run_metis metis_fns args name (these (!named_thms))) id st) else () end