--- a/src/HOL/Mirabelle/Mirabelle.thy Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy Wed May 12 12:22:44 2021 +0200
@@ -7,7 +7,6 @@
begin
ML_file \<open>Tools/mirabelle.ML\<close>
-ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
--- a/src/HOL/Sledgehammer.thy Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Sledgehammer.thy Wed May 12 12:22:44 2021 +0200
@@ -33,5 +33,6 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
end
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Wed May 12 12:22:44 2021 +0200
@@ -8,8 +8,6 @@
imports Complex_Main TPTP_Interpret "HOL-Library.Refute"
begin
-ML_file \<open>sledgehammer_tactics.ML\<close>
-
ML \<open>Proofterm.proofs := 0\<close>
declare [[show_consts]] (* for Refute *)
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Wed May 12 12:22:44 2021 +0200
@@ -8,8 +8,6 @@
imports TPTP_Parser TPTP_Interpret
begin
-ML_file "sledgehammer_tactics.ML"
-
import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
ML \<open>
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed May 12 06:35:16 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* Title: HOL/TPTP/sledgehammer_tactics.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010, 2011
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
- type fact_override = Sledgehammer_Fact.fact_override
-
- val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
- thm list -> int -> tactic
- val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
- thm list -> int -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Fact
-open Sledgehammer_Prover
-open Sledgehammer_Prover_ATP
-open Sledgehammer_Prover_Minimize
-open Sledgehammer_MaSh
-open Sledgehammer_Commands
-
-fun run_prover override_params fact_override chained i n ctxt goal =
- let
- val thy = Proof_Context.theory_of ctxt
- val mode = Normal
- val params as {provers, max_facts, ...} = default_params thy override_params
- val name = hd provers
- val prover = get_prover ctxt mode name
- val default_max_facts = default_max_facts_of_prover ctxt name
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
- val ho_atp = exists (is_ho_atp ctxt) provers
- val keywords = Thy_Header.get_keywords' ctxt
- val css_table = clasimpset_rule_table_of ctxt
- val facts =
- nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
- |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
- hyp_ts concl_t
- |> hd |> snd
- val problem =
- {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)], found_proof = I}
- in
- (case prover params problem of
- {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
- | _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
- end
-
-fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
- let val override_params = override_params @ [("preplay_timeout", "0")] in
- (case run_prover override_params fact_override chained i i ctxt th of
- SOME facts =>
- Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
- (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty)
- end
-
-fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
- let
- val override_params =
- override_params @
- [("preplay_timeout", "0"),
- ("minimize", "false")]
- val xs = run_prover override_params fact_override chained i i ctxt th
- in
- if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Wed May 12 12:22:44 2021 +0200
@@ -0,0 +1,76 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010, 2011
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ type fact_override = Sledgehammer_Fact.fact_override
+
+ val sledgehammer_with_metis_tac : Proof.context -> (string * string) list -> fact_override ->
+ thm list -> int -> tactic
+ val sledgehammer_as_oracle_tac : Proof.context -> (string * string) list -> fact_override ->
+ thm list -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Prover
+open Sledgehammer_Prover_ATP
+open Sledgehammer_Prover_Minimize
+open Sledgehammer_MaSh
+open Sledgehammer_Commands
+
+fun run_prover override_params fact_override chained i n ctxt goal =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val mode = Normal
+ val params as {provers, max_facts, ...} = default_params thy override_params
+ val name = hd provers
+ val prover = get_prover ctxt mode name
+ val default_max_facts = default_max_facts_of_prover ctxt name
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
+ val ho_atp = exists (is_ho_atp ctxt) provers
+ val keywords = Thy_Header.get_keywords' ctxt
+ val css_table = clasimpset_rule_table_of ctxt
+ val facts =
+ nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
+ |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
+ hyp_ts concl_t
+ |> hd |> snd
+ val problem =
+ {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ factss = [("", facts)], found_proof = I}
+ in
+ (case prover params problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ end
+
+fun sledgehammer_with_metis_tac ctxt override_params fact_override chained i th =
+ let val override_params = override_params @ [("preplay_timeout", "0")] in
+ (case run_prover override_params fact_override chained i i ctxt th of
+ SOME facts =>
+ Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
+ (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty)
+ end
+
+fun sledgehammer_as_oracle_tac ctxt override_params fact_override chained i th =
+ let
+ val override_params =
+ override_params @
+ [("preplay_timeout", "0"),
+ ("minimize", "false")]
+ val xs = run_prover override_params fact_override chained i i ctxt th
+ in
+ if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty
+ end
+
+end;