--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 31 16:53:14 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Mon Mar 31 18:55:45 2025 +0200
@@ -11,21 +11,6 @@
type prover = Sledgehammer_Prover.prover
type base_slice = Sledgehammer_ATP_Systems.base_slice
- val algebraN : string
- val argoN : string
- val autoN : string
- val blastN : string
- val fastforceN : string
- val forceN : string
- val linarithN : string
- val mesonN : string
- val metisN : string
- val orderN : string
- val presburgerN : string
- val satxN : string
- val simpN : string
-
- val tactic_provers : string list
val is_tactic_prover : string -> bool
val good_slices_of_tactic_prover : string -> base_slice list
val run_tactic_prover : mode -> string -> prover
@@ -40,25 +25,7 @@
open Sledgehammer_Proof_Methods
open Sledgehammer_Prover
-val algebraN = "algebra"
-val argoN = "argo"
-val autoN = "auto"
-val blastN = "blast"
-val fastforceN = "fastforce"
-val forceN = "force"
-val linarithN = "linarith"
-val mesonN = "meson"
-val metisN = "metis"
-val orderN = "order"
-val presburgerN = "presburger"
-val satxN = "satx"
-val simpN = "simp"
-
-val tactic_provers =
- [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN,
- metisN, orderN, presburgerN, satxN, simpN]
-
-val is_tactic_prover = member (op =) tactic_provers
+val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method
val meshN = "mesh"
@@ -69,21 +36,20 @@
(1, false, false, 8, meshN),
(1, false, false, 32, meshN)]
-fun meth_of name =
- if name = algebraN then Algebra_Method
- else if name = argoN then Argo_Method
- else if name = autoN then Auto_Method
- else if name = blastN then Blast_Method
- else if name = fastforceN then Fastforce_Method
- else if name = forceN then Force_Method
- else if name = linarithN then Linarith_Method
- else if name = mesonN then Meson_Method
- else if name = metisN then Metis_Method (NONE, NONE, [])
- else if name = orderN then Order_Method
- else if name = presburgerN then Presburger_Method
- else if name = satxN then SATx_Method
- else if name = simpN then Simp_Method
- else error ("Unknown tactic: " ^ quote name)
+fun meth_of "algebra" = Algebra_Method
+ | meth_of "argo" = Argo_Method
+ | meth_of "auto" = Auto_Method
+ | meth_of "blast" = Blast_Method
+ | meth_of "fastforce" = Fastforce_Method
+ | meth_of "force" = Force_Method
+ | meth_of "linarith" = Linarith_Method
+ | meth_of "meson" = Meson_Method
+ | meth_of "metis" = Metis_Method (NONE, NONE, [])
+ | meth_of "order" = Order_Method
+ | meth_of "presburger" = Presburger_Method
+ | meth_of "satx" = SATx_Method
+ | meth_of "simp" = Simp_Method
+ | meth_of _ = Metis_Method (NONE, NONE, [])
fun run_tactic_prover mode name ({slices, timeout, ...} : params)
({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =