# HG changeset patch # User blanchet # Date 1643641763 -3600 # Node ID b087610592b48eefdb51f170dc1f50a651a3bfa8 # Parent 30a619de7973e89ee805f081320d9e46b9f07cf1 rationalized output for forthcoming slicing model diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Jan 31 16:09:23 2022 +0100 @@ -19,7 +19,11 @@ type prover_problem = Sledgehammer_Prover.prover_problem type prover_result = Sledgehammer_Prover.prover_result - datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None + datatype sledgehammer_outcome = + SH_Some of prover_result + | SH_Unknown + | SH_Timeout + | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string @@ -47,10 +51,11 @@ open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh -datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None - -fun is_sledgehammer_outcome_some (SH_Some _) = true - | is_sledgehammer_outcome_some _ = false +datatype sledgehammer_outcome = + SH_Some of prover_result +| SH_Unknown +| SH_Timeout +| SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" @@ -64,19 +69,18 @@ fun max_outcome outcomes = let - val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes + val result = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in - some + result |> alternative snd unknown |> alternative snd timeout |> alternative snd none |> the_default (SH_Unknown, "") end - fun is_metis_method (Metis_Method _) = true | is_metis_method _ = false @@ -156,7 +160,7 @@ |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas - |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ quote name ^ + |> prefix ("Fact" ^ plural_s num_facts ^ " in " ^ name ^ " proof (of " ^ string_of_int num_facts ^ "): ") |> writeln @@ -256,10 +260,10 @@ val message = message () val () = - if mode <> Auto_Try andalso is_sledgehammer_outcome_some outcome orelse mode = Normal then - the_default writeln writeln_result (quote prover_name ^ ": " ^ message) - else - () + (case outcome of + SH_Some _ => + the_default writeln writeln_result (prover_name ^ ": " ^ message) + | _ => ()) in (outcome, message) end @@ -275,7 +279,7 @@ "Found no relevant facts" else cat_lines (map (fn (filter, facts) => - (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) + (if filter = "" then "" else filter ^ ": ") ^ string_of_facts facts) factss) fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode writeln_result i (fact_override as {only, ...}) state = @@ -290,14 +294,11 @@ val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proof = - if mode = Normal then - let val proof_found = Synchronized.var "proof_found" false in - fn () => - if Synchronized.change_result proof_found (rpair true) then () - else (writeln_result |> the_default writeln) "Proof found..." - end - else - I + fn prover_name => + if mode = Normal then + (writeln_result |> the_default writeln) (prover_name ^ " found a proof...") + else + () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate @@ -350,7 +351,9 @@ in if mode = Auto_Try then (SH_Unknown, "") - |> fold (fn prover => fn accum as (SH_Some _, _) => accum | _ => launch problem prover) + |> fold (fn prover => + fn accum as (SH_Some _, _) => accum + | _ => launch problem prover) provers else (learn chained_thms; @@ -359,10 +362,13 @@ |> max_outcome) end in - launch_provers () - handle Timeout.TIMEOUT _ => - (print "Sledgehammer ran out of time"; (SH_Timeout, "")) - end - |> `(fn (outcome, _) => is_sledgehammer_outcome_some outcome)) + (launch_provers () + handle Timeout.TIMEOUT _ => (SH_Timeout, "")) + |> `(fn (outcome, _) => + (case outcome of + SH_Some _ => (print "QED"; true) + | SH_Timeout => (print "Timed out"; false) + | _ => (print "Done"; false))) + end) end; diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Jan 31 16:09:23 2022 +0100 @@ -868,7 +868,7 @@ let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, - subgoal_count = 1, factss = [("", facts)], found_proof = I} + subgoal_count = 1, facts = ("", facts), found_proof = K ()} in get_minimizing_prover ctxt MaSh (K ()) prover params problem end diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jan 31 16:09:23 2022 +0100 @@ -58,7 +58,7 @@ subgoal : int, subgoal_count : int, facts : string * fact list, - found_proof : unit -> unit} + found_proof : string -> unit} type prover_result = {outcome : atp_failure option, @@ -186,7 +186,7 @@ subgoal : int, subgoal_count : int, facts : string * fact list, - found_proof : unit -> unit} + found_proof : string -> unit} type prover_result = {outcome : atp_failure option, @@ -200,10 +200,10 @@ fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) -fun proof_banner mode name = +fun proof_banner mode prover_name = (case mode of - Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" - | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" + Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof" + | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof" | _ => "Try this") fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jan 31 16:09:23 2022 +0100 @@ -106,7 +106,7 @@ ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slice, timeout, preplay_timeout, spy, ...} : params) - ({comment, state, goal, subgoal, subgoal_count, facts, found_proof, ...} : prover_problem) = + ({comment, state, goal, subgoal, subgoal_count, facts, found_proof} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -264,7 +264,7 @@ in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end - | NONE => (found_proof (); NONE)) + | NONE => (found_proof name; NONE)) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (format, type_enc)) diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Jan 31 16:09:23 2022 +0100 @@ -98,7 +98,7 @@ slice = Time.zeroTime, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - facts = ("", facts), found_proof = I} + facts = ("", facts), found_proof = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem @@ -206,7 +206,7 @@ fun test timeout non_chained = test_facts params silent prover timeout i n state goal (chained @ non_chained) in - (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name); + (print silent (fn () => "Sledgehammer minimizer: " ^ prover_name); (case test timeout non_chained of result as {outcome = NONE, used_facts, run_time, ...} => let diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Jan 31 16:09:23 2022 +0100 @@ -129,7 +129,7 @@ (case outcome of NONE => let - val _ = found_proof (); + val _ = found_proof name; val preferred = if smt_proofs then SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) diff -r 30a619de7973 -r b087610592b4 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09:23 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Jan 31 16:09:23 2022 +0100 @@ -45,7 +45,7 @@ |> hd |> snd val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - facts = ("", facts), found_proof = I} + facts = ("", facts), found_proof = K ()} in (case prover params problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME