# HG changeset patch # User desharna # Date 1740501461 -3600 # Node ID a1f85f579a0727abdc2b9c59245eeed633759425 # Parent b1af763166f424fe9a3a8b992d60e8d358b57a0b initial work on Magnushammer-inspured tactic hammer (from Jasmin) diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Sledgehammer.thy Tue Feb 25 17:37:41 2025 +0100 @@ -29,6 +29,7 @@ ML_file \Tools/Sledgehammer/sledgehammer_prover.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_atp.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_smt.ML\ +ML_file \Tools/Sledgehammer/sledgehammer_prover_tactic.ML\ ML_file \Tools/Sledgehammer/sledgehammer_prover_minimize.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mepo.ML\ ML_file \Tools/Sledgehammer/sledgehammer_mash.ML\ diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Feb 25 17:37:41 2025 +0100 @@ -51,6 +51,7 @@ open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP +open Sledgehammer_Prover_Tactic open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh @@ -437,7 +438,7 @@ extra_extra0)) = ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, the_default uncurried_aliases0 uncurried_aliases, extra_extra0) - | adjust_extra (extra as SMT_Slice _) = extra + | adjust_extra extra = extra fun adjust_slice max_slice_size ((slice_size0, abduce0, falsify0, num_facts0, fact_filter0), extra) = diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Feb 25 17:37:41 2025 +0100 @@ -25,6 +25,7 @@ open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_SMT +open Sledgehammer_Prover_Tactic open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh open Sledgehammer @@ -170,7 +171,7 @@ (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value ctxt = \ \see also \<^system_option>\sledgehammer_provers\\ - filter (is_prover_installed ctxt) (smts ctxt @ local_atps) + filter (is_prover_installed ctxt) (smt_solvers ctxt @ local_atps @ tactic_provers) |> implode_param fun set_default_raw_param param thy = diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 25 17:37:41 2025 +0100 @@ -160,7 +160,7 @@ isar_params () in if null atp_proof0 then - one_line_proof_text ctxt 0 one_line_params + one_line_proof_text one_line_params else let val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods @@ -475,7 +475,7 @@ in (case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of (0, 1) => - one_line_proof_text ctxt 0 + one_line_proof_text (if is_less (play_outcome_ord (play_outcome, one_line_play)) then (case isar_proof of Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs), @@ -502,7 +502,7 @@ else []) @ (if do_preplay then [string_of_play_outcome play_outcome] else []) in - one_line_proof_text ctxt 0 one_line_params ^ + one_line_proof_text one_line_params ^ (if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ Active.sendback_markup_command @@ -519,7 +519,7 @@ (case try generate_proof_text () of SOME s => s | NONE => - one_line_proof_text ctxt 0 one_line_params ^ + one_line_proof_text one_line_params ^ (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) end @@ -535,7 +535,7 @@ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params else - one_line_proof_text ctxt num_chained) one_line_params + one_line_proof_text) one_line_params fun abduce_text ctxt tms = "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^ diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Feb 25 17:37:41 2025 +0100 @@ -44,7 +44,7 @@ val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic val string_of_play_outcome : play_outcome -> string val play_outcome_ord : play_outcome ord - val one_line_proof_text : Proof.context -> int -> one_line_params -> string + val one_line_proof_text : one_line_params -> string end; structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = @@ -220,7 +220,7 @@ | apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n (* FIXME *) -fun proof_method_command meth i n used_chaineds _(*num_chained*) extras = +fun proof_method_command meth i n used_chaineds extras = let val (indirect_facts, direct_facts) = if is_proof_method_direct meth then ([], extras) else (extras, []) @@ -246,11 +246,10 @@ (* Add optional markup break (command may need multiple lines) *) Markup.markup (Markup.break {width = 1, indent = 2}) " ") -fun one_line_proof_text _ num_chained - ((used_facts, (meth, play)), banner, subgoal, subgoal_count) = +fun one_line_proof_text ((used_facts, (meth, play)), banner, subgoal, subgoal_count) = let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in map fst extra - |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained + |> proof_method_command meth subgoal subgoal_count (map fst chained) |> (if play = Play_Failed then failed_command_line else try_command_line banner play) end diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Tue Feb 25 17:37:41 2025 +0100 @@ -72,6 +72,7 @@ datatype prover_slice_extra = ATP_Slice of atp_slice | SMT_Slice of string list + | No_Slice type prover_slice = base_slice * prover_slice_extra @@ -199,6 +200,7 @@ datatype prover_slice_extra = ATP_Slice of atp_slice | SMT_Slice of string list +| No_Slice type prover_slice = base_slice * prover_slice_extra diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Feb 25 17:37:41 2025 +0100 @@ -43,29 +43,35 @@ open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT +open Sledgehammer_Prover_Tactic fun is_prover_supported ctxt = - is_atp orf is_smt_prover ctxt + is_atp orf is_smt_solver ctxt orf is_tactic_prover fun is_prover_installed ctxt prover_name = if is_atp prover_name then let val thy = Proof_Context.theory_of ctxt in is_atp_installed thy prover_name end + else if is_smt_solver ctxt prover_name then + is_smt_solver_installed ctxt prover_name else - is_smt_prover_installed ctxt prover_name + true fun get_prover ctxt mode name = if is_atp name then run_atp mode name - else if is_smt_prover ctxt name then run_smt_solver mode name + else if is_smt_solver ctxt name then run_smt_solver mode name + else if is_tactic_prover name then run_tactic_prover mode name else error ("No such prover: " ^ name) fun get_slices ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp name then map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt) - else if is_smt_prover ctxt name then + else if is_smt_solver ctxt name then map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name) + else if is_tactic_prover name then + map (rpair No_Slice) (good_slices_of_tactic_prover name) else error ("No such prover: " ^ name) end diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Feb 25 15:54:41 2025 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Tue Feb 25 17:37:41 2025 +0100 @@ -15,11 +15,11 @@ val smt_builtins : bool Config.T val smt_triggers : bool Config.T - val is_smt_prover : Proof.context -> string -> bool - val is_smt_prover_installed : Proof.context -> string -> bool + val is_smt_solver : Proof.context -> string -> bool + val is_smt_solver_installed : Proof.context -> string -> bool val run_smt_solver : mode -> string -> prover - val smts : Proof.context -> string list + val smt_solvers : Proof.context -> string list end; structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = @@ -38,10 +38,10 @@ val smt_builtins = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (K true) -val smts = sort_strings o SMT_Config.all_solvers_of +val smt_solvers = sort_strings o SMT_Config.all_solvers_of -val is_smt_prover = member (op =) o smts -val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of +val is_smt_solver = member (op =) o smt_solvers +val is_smt_solver_installed = member (op =) o SMT_Config.available_solvers_of (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) diff -r b1af763166f4 -r a1f85f579a07 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML Tue Feb 25 17:37:41 2025 +0100 @@ -0,0 +1,126 @@ +(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML + Author: Jasmin Blanchette, LMU Muenchen + +Isabelle tactics as Sledgehammer provers. +*) + +signature SLEDGEHAMMER_PROVER_TACTIC = +sig + type stature = ATP_Problem_Generate.stature + type mode = Sledgehammer_Prover.mode + type prover = Sledgehammer_Prover.prover + type base_slice = Sledgehammer_ATP_Systems.base_slice + + val autoN : string + val blastN : 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 +end; + +structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC = +struct + +open ATP_Problem_Generate +open ATP_Proof +open Sledgehammer_ATP_Systems +open Sledgehammer_Proof_Methods +open Sledgehammer_Prover + +val autoN = "auto" +val blastN = "blast" +val simpN = "simp" + +val tactic_provers = [autoN, blastN, simpN] + +val is_tactic_prover = member (op =) tactic_provers + +val meshN = "mesh" + +fun good_slices_of_tactic_prover name = + (* FUDGE *) + if name = simpN then + [(1, false, false, 0, meshN), + (1, false, false, 2, meshN), + (1, false, false, 8, meshN), + (1, false, false, 32, meshN), + (1, false, false, 128, meshN)] + else + [(1, false, false, 0, meshN), + (1, false, false, 1, meshN), + (1, false, false, 2, meshN), + (1, false, false, 4, meshN), + (1, false, false, 8, meshN)] + +(* In sync with Sledgehammer_Proof_Methods.tac_of_proof_method *) +fun tac_of ctxt name (local_facts, global_facts) = + if name = autoN then + Method.insert_tac ctxt (local_facts @ global_facts) THEN' + SELECT_GOAL (Clasimp.auto_tac ctxt) + else if name = blastN then + Method.insert_tac ctxt (local_facts @ global_facts) THEN' + blast_tac ctxt + else if name = simpN then + Method.insert_tac ctxt local_facts THEN' + Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) + else + error ("Unknown tactic: " ^ quote name) + +fun meth_of name = + if name = autoN then + Auto_Method + else if name = blastN then + Blast_Method + else if name = simpN then + Simp_Method + else + error ("Unknown tactic: " ^ quote name) + +fun run_tactic_prover mode name (params as {debug, verbose, isar_proofs, compress, try0, minimize, + timeout, ...}) + ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) + slice = + let + val (basic_slice, No_Slice) = slice + val facts = facts_of_basic_slice basic_slice factss + val ctxt = Proof.context_of state + + val (local_facts, global_facts) = + fold (fn fact => if fst (snd (fst fact)) = Global then apsnd (cons (snd fact)) + else apfst (cons (snd fact))) facts ([], []) + + val timer = Timer.startRealTimer () + + val out = + (Timeout.apply timeout + (Goal.prove ctxt [] [] (Logic.get_goal (Thm.prop_of goal) subgoal)) + (fn {context = ctxt, ...} => + HEADGOAL (tac_of ctxt name (local_facts, global_facts))); + NONE) + handle ERROR _ => SOME GaveUp + | Timeout.TIMEOUT _ => SOME TimedOut + + val run_time = Timer.checkRealTimer timer + + val (outcome, used_facts) = + (case out of + NONE => + (found_something name; + (NONE, map fst facts)) + | some_failure => (some_failure, [])) + + val message = fn _ => + (case outcome of + NONE => + one_line_proof_text ((used_facts, (meth_of name, Played run_time)), proof_banner mode name, + subgoal, subgoal_count) + | SOME failure => string_of_atp_failure failure) + in + {outcome = outcome, used_facts = used_facts, used_from = facts, + preferred_methss = (meth_of name, []), run_time = run_time, message = message} + end + +end;