# HG changeset patch
# User blanchet
# Date 1643805828 -3600
# Node ID 789e0e1a9e33effa75781b5e05332f3c656bf2b2
# Parent  5f29ddeb03864c7da8c41aec340bd731611dce42
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')

diff -r 5f29ddeb0386 -r 789e0e1a9e33 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Feb 02 13:43:48 2022 +0100
@@ -297,7 +297,7 @@
       @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
   end
 
-fun prover_slices_of_schedule ctxt
+fun prover_slices_of_schedule ctxt factss
     ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule =
   let
     fun triplicate_slices original =
@@ -319,11 +319,13 @@
        the_default uncurried_aliases0 uncurried_aliases, extra_extra0)
 
     fun adjust_slice ((num_facts0, fact_filter0), extra) =
-      ((case max_facts of
-         NONE => num_facts0
-       | SOME max_facts => Int.min (num_facts0, max_facts),
-        the_default fact_filter0 fact_filter),
-       Option.map adjust_extra extra)
+      let
+        val fact_filter = fact_filter |> the_default fact_filter0
+        val max_facts = max_facts |> the_default num_facts0
+        val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
+      in
+        ((num_facts, fact_filter), Option.map adjust_extra extra)
+      end
 
     val provers = distinct (op =) schedule
     val prover_slices =
@@ -416,16 +418,17 @@
 
         fun launch_provers () =
           let
+            val factss = get_factss provers
             val problem =
               {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
-               factss = get_factss provers, found_proof = found_proof}
+               factss = factss, found_proof = found_proof}
             val learn = mash_learn_proof ctxt params (Thm.prop_of goal)
             val launch = launch_prover_and_preplay params mode writeln_result learn
 
             val schedule =
               if mode = Auto_Try then provers
               else schedule_of_provers provers slices
-            val prover_slices = prover_slices_of_schedule ctxt params schedule
+            val prover_slices = prover_slices_of_schedule ctxt factss params schedule
 
             val _ =
               if verbose then
diff -r 5f29ddeb0386 -r 789e0e1a9e33 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Feb 02 13:43:48 2022 +0100
@@ -82,7 +82,7 @@
   val is_atp : string -> bool
   val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
     proof_method list list
-  val get_facts_of_filter : string -> (string * fact list) list -> fact list
+  val facts_of_filter : string -> (string * fact list) list -> fact list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
@@ -225,7 +225,7 @@
     try0_methodss @ [metis_methods] @ smt_methodss
   end
 
-fun get_facts_of_filter fact_filter factss =
+fun facts_of_filter fact_filter factss =
   (case AList.lookup (op =) factss fact_filter of
     SOME facts => facts
   | NONE => snd (hd factss))
diff -r 5f29ddeb0386 -r 789e0e1a9e33 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Feb 02 13:43:48 2022 +0100
@@ -183,7 +183,7 @@
           end
 
         val effective_fact_filter = fact_filter |> the_default good_fact_filter
-        val facts = get_facts_of_filter effective_fact_filter factss
+        val facts = facts_of_filter effective_fact_filter factss
         val num_facts =
           (case max_facts of
             NONE => good_max_facts
diff -r 5f29ddeb0386 -r 789e0e1a9e33 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Feb 02 13:34:52 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Feb 02 13:43:48 2022 +0100
@@ -124,7 +124,7 @@
     val ((best_max_facts, best_fact_filter), _) = slice
 
     val effective_fact_filter = fact_filter |> the_default best_fact_filter
-    val facts = take best_max_facts (get_facts_of_filter effective_fact_filter factss)
+    val facts = take best_max_facts (facts_of_filter effective_fact_filter factss)
 
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt_filter name params state goal subgoal facts