rationalized output for forthcoming slicing model

--- 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;

--- 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

--- 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 =

--- 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))

--- 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

--- 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)

--- 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