# HG changeset patch
# User blanchet
# Date 1677839129 -3600
# Node ID 8a28ab58d155e20b46bc55dab0c3e0b9ff0f5a9b
# Parent  615a6a6a4b0b44098b87e90e90f215bd9db23dcd
detect duplicates in Sledgehammer output -- suggested by Larry Paulson

diff -r 615a6a6a4b0b -r 8a28ab58d155 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 03 10:30:10 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 03 11:25:29 2023 +0100
@@ -288,7 +288,7 @@
   end
 
 fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode
-    has_already_found_something found_something writeln_result learn
+    has_already_found_something found_something massage_message writeln_result learn
     (problem as {state, subgoal, ...}) (slice as ((_, _, falsify, _, _), _)) prover_name =
   let
     val ctxt = Proof.context_of state
@@ -314,7 +314,7 @@
         {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1,
          subgoal_count = 1, factss = map (apsnd (append new_facts)) factss,
          has_already_found_something = has_already_found_something,
-         found_something = found_something "an inconsistency"}
+         found_something = found_something "a falsification"}
       end
 
     val problem as {goal, ...} = problem |> falsify ? flip_problem
@@ -344,7 +344,9 @@
         ()
       else
         (case outcome of
-          SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message)
+          SH_Some _ =>
+          the_default writeln writeln_result (prover_name ^ ": " ^
+            massage_message (if falsify then "falsification" else "proof") message)
         | _ => ())
   in
     (outcome, message)
@@ -487,6 +489,33 @@
           else
             ()
 
+        val seen_messages = Synchronized.var "seen_messages" ([] : string list)
+
+        fun strip_until_left_paren "" = ""
+          | strip_until_left_paren s =
+            let
+              val n = String.size s
+              val s' = String.substring (s, 0, n - 1)
+            in
+              s' |> String.substring (s, n - 1, 1) <> "(" ? strip_until_left_paren
+            end
+
+        (* Remove the measured preplay time when looking for duplicates. This is
+           admittedly rather ad hoc. *)
+        fun strip_time s =
+          if String.isSuffix " s)" s orelse String.isSuffix " ms)" s then
+            strip_until_left_paren s
+          else
+            s
+
+        fun massage_message proof_or_inconsistency s =
+          let val s' = strip_time s in
+            if member (op =) (Synchronized.value seen_messages) s' then
+              "Found duplicate " ^ proof_or_inconsistency
+            else
+              (Synchronized.change seen_messages (cons s'); s)
+          end
+
         val ctxt = Proof.context_of state
         val inst_inducts = induction_rules = SOME Instantiate
         val {facts = chained_thms, goal, ...} = Proof.goal state
@@ -544,7 +573,7 @@
                found_something = found_something "a proof"}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
             val launch = launch_prover_and_preplay params mode has_already_found_something
-              found_something writeln_result learn
+              found_something massage_message writeln_result learn
 
             val schedule =
               if mode = Auto_Try then provers