further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
1 (* Title: HOL/TPTP/sledgehammer_tactics.ML
2 Author: Jasmin Blanchette, TU Muenchen
5 Sledgehammer as a tactic.
8 signature SLEDGEHAMMER_TACTICS =
10 type relevance_override = Sledgehammer_Filter.relevance_override
12 val sledgehammer_with_metis_tac :
13 Proof.context -> (string * string) list -> relevance_override -> int
15 val sledgehammer_as_oracle_tac :
16 Proof.context -> (string * string) list -> relevance_override -> int
20 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
23 open Sledgehammer_Filter
25 fun run_prover override_params relevance_override i n ctxt goal =
27 val mode = Sledgehammer_Provers.Normal
28 val chained_ths = [] (* a tactic has no chained ths *)
29 val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
30 Sledgehammer_Isar.default_params ctxt override_params
32 val prover = Sledgehammer_Provers.get_prover ctxt mode name
33 val default_max_relevant =
34 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
35 val is_built_in_const =
36 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
38 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
39 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
40 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
42 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override
43 chained_ths hyp_ts concl_t
44 |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
45 (the_default default_max_relevant max_relevant) is_built_in_const
46 relevance_fudge relevance_override chained_ths hyp_ts concl_t
48 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
49 facts = map Sledgehammer_Provers.Untranslated_Fact facts}
51 (case prover params (K (K (K ""))) problem of
52 {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
54 handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
57 fun thms_of_name ctxt name =
59 val lex = Keyword.get_lexicons
60 val get = maps (Proof_Context.get_fact ctxt o fst)
64 |> Token.source {do_recover=SOME false} lex Position.start
65 |> Token.source_proper
66 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
70 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
74 [("preplay_timeout", "0")]
76 case run_prover override_params relevance_override i i ctxt th of
78 Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt
79 (maps (thms_of_name ctxt) facts) i th
83 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
85 val thy = Proof_Context.theory_of ctxt
88 [("preplay_timeout", "0"),
89 ("minimize", "false")]
90 val xs = run_prover override_params relevance_override i i ctxt th
91 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end