5 Sledgehammer as a tactic. |
5 Sledgehammer as a tactic. |
6 *) |
6 *) |
7 |
7 |
8 signature SLEDGEHAMMER_TACTICS = |
8 signature SLEDGEHAMMER_TACTICS = |
9 sig |
9 sig |
10 type relevance_override = Sledgehammer_Fact.relevance_override |
10 type fact_override = Sledgehammer_Fact.fact_override |
11 |
11 |
12 val sledgehammer_with_metis_tac : |
12 val sledgehammer_with_metis_tac : |
13 Proof.context -> (string * string) list -> relevance_override -> int |
13 Proof.context -> (string * string) list -> fact_override -> int -> tactic |
14 -> tactic |
|
15 val sledgehammer_as_oracle_tac : |
14 val sledgehammer_as_oracle_tac : |
16 Proof.context -> (string * string) list -> relevance_override -> int |
15 Proof.context -> (string * string) list -> fact_override -> int -> tactic |
17 -> tactic |
|
18 end; |
16 end; |
19 |
17 |
20 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
18 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
21 struct |
19 struct |
22 |
20 |
23 open Sledgehammer_Fact |
21 open Sledgehammer_Fact |
24 |
22 |
25 fun run_prover override_params relevance_override i n ctxt goal = |
23 fun run_prover override_params fact_override i n ctxt goal = |
26 let |
24 let |
27 val mode = Sledgehammer_Provers.Normal |
25 val mode = Sledgehammer_Provers.Normal |
28 val chained_ths = [] (* a tactic has no chained ths *) |
|
29 val params as {provers, max_relevant, slice, ...} = |
26 val params as {provers, max_relevant, slice, ...} = |
30 Sledgehammer_Isar.default_params ctxt override_params |
27 Sledgehammer_Isar.default_params ctxt override_params |
31 val name = hd provers |
28 val name = hd provers |
32 val prover = Sledgehammer_Provers.get_prover ctxt mode name |
29 val prover = Sledgehammer_Provers.get_prover ctxt mode name |
33 val default_max_relevant = |
30 val default_max_relevant = |
34 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name |
31 Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name |
35 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
32 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
36 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
33 val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers |
37 val facts = |
34 val facts = |
38 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp relevance_override |
35 Sledgehammer_Fact.nearly_all_facts ctxt ho_atp fact_override [] |
39 chained_ths hyp_ts concl_t |
36 hyp_ts concl_t |
40 |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name |
37 |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params name |
41 (the_default default_max_relevant max_relevant) relevance_override |
38 (the_default default_max_relevant max_relevant) fact_override |
42 chained_ths hyp_ts concl_t |
39 hyp_ts concl_t |
43 val problem = |
40 val problem = |
44 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
41 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
45 facts = facts |> map (apfst (apfst (fn name => name ()))) |
42 facts = facts |> map (apfst (apfst (fn name => name ()))) |
46 |> map Sledgehammer_Provers.Untranslated_Fact} |
43 |> map Sledgehammer_Provers.Untranslated_Fact} |
47 in |
44 in |
62 |> Token.source_proper |
59 |> Token.source_proper |
63 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
60 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
64 |> Source.exhaust |
61 |> Source.exhaust |
65 end |
62 end |
66 |
63 |
67 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = |
64 fun sledgehammer_with_metis_tac ctxt override_params fact_override i th = |
68 let |
65 let val override_params = override_params @ [("preplay_timeout", "0")] in |
69 val override_params = |
66 case run_prover override_params fact_override i i ctxt th of |
70 override_params @ |
|
71 [("preplay_timeout", "0")] |
|
72 in |
|
73 case run_prover override_params relevance_override i i ctxt th of |
|
74 SOME facts => |
67 SOME facts => |
75 Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt |
68 Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt |
76 (maps (thms_of_name ctxt) facts) i th |
69 (maps (thms_of_name ctxt) facts) i th |
77 | NONE => Seq.empty |
70 | NONE => Seq.empty |
78 end |
71 end |
79 |
72 |
80 fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = |
73 fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th = |
81 let |
74 let |
82 val thy = Proof_Context.theory_of ctxt |
75 val thy = Proof_Context.theory_of ctxt |
83 val override_params = |
76 val override_params = |
84 override_params @ |
77 override_params @ |
85 [("preplay_timeout", "0"), |
78 [("preplay_timeout", "0"), |
86 ("minimize", "false")] |
79 ("minimize", "false")] |
87 val xs = run_prover override_params relevance_override i i ctxt th |
80 val xs = run_prover override_params fact_override i i ctxt th |
88 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
81 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
89 |
82 |
90 end; |
83 end; |