1 (* Title: sledgehammer_tactics.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2010 |
|
4 |
|
5 Sledgehammer as a tactic. |
|
6 *) |
|
7 |
|
8 signature SLEDGEHAMMER_TACTICS = |
|
9 sig |
|
10 val sledgehammer_with_metis_tac : Proof.context -> int -> tactic |
|
11 val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic |
|
12 val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic |
|
13 end; |
|
14 |
|
15 structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
|
16 struct |
|
17 |
|
18 fun run_atp force_full_types timeout i n ctxt goal name = |
|
19 let |
|
20 val chained_ths = [] (* a tactic has no chained ths *) |
|
21 val params as {type_sys, relevance_thresholds, max_relevant, ...} = |
|
22 ((if force_full_types then [("full_types", "true")] else []) |
|
23 @ [("timeout", Int.toString (Time.toSeconds timeout))]) |
|
24 (* @ [("overlord", "true")] *) |
|
25 |> Sledgehammer_Isar.default_params ctxt |
|
26 val prover = Sledgehammer_Provers.get_prover ctxt false name |
|
27 val default_max_relevant = |
|
28 Sledgehammer_Provers.default_max_relevant_for_prover ctxt name |
|
29 val is_built_in_const = |
|
30 Sledgehammer_Provers.is_built_in_const_for_prover ctxt name |
|
31 val relevance_fudge = |
|
32 Sledgehammer_Provers.relevance_fudge_for_prover ctxt name |
|
33 val relevance_override = {add = [], del = [], only = false} |
|
34 val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i |
|
35 val no_dangerous_types = |
|
36 Sledgehammer_ATP_Translate.types_dangerous_types type_sys |
|
37 val facts = |
|
38 Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types |
|
39 relevance_thresholds |
|
40 (the_default default_max_relevant max_relevant) is_built_in_const |
|
41 relevance_fudge relevance_override chained_ths hyp_ts concl_t |
|
42 (* Check for constants other than the built-in HOL constants. If none of |
|
43 them appear (as should be the case for TPTP problems, unless "auto" or |
|
44 "simp" already did its "magic"), we can skip the relevance filter. *) |
|
45 val pure_goal = |
|
46 not (exists_Const (fn (s, _) => String.isSubstring "." s andalso |
|
47 not (String.isSubstring "HOL" s)) |
|
48 (prop_of goal)) |
|
49 val problem = |
|
50 {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
|
51 facts = map Sledgehammer_Provers.Untranslated_Fact facts, |
|
52 smt_head = NONE} |
|
53 in |
|
54 (case prover params (K "") problem of |
|
55 {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME |
|
56 | _ => NONE) |
|
57 handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) |
|
58 end |
|
59 |
|
60 fun to_period ("." :: _) = [] |
|
61 | to_period ("" :: ss) = to_period ss |
|
62 | to_period (s :: ss) = s :: to_period ss |
|
63 | to_period [] = [] |
|
64 |
|
65 val atp = "vampire" (* or "e" or "spass" etc. *) |
|
66 |
|
67 fun thms_of_name ctxt name = |
|
68 let |
|
69 val lex = Keyword.get_lexicons |
|
70 val get = maps (ProofContext.get_fact ctxt o fst) |
|
71 in |
|
72 Source.of_string name |
|
73 |> Symbol.source |
|
74 |> Token.source {do_recover=SOME false} lex Position.start |
|
75 |> Token.source_proper |
|
76 |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
|
77 |> Source.exhaust |
|
78 end |
|
79 |
|
80 fun sledgehammer_with_metis_tac ctxt i th = |
|
81 let |
|
82 val timeout = Time.fromSeconds 30 |
|
83 in |
|
84 case run_atp false timeout i i ctxt th atp of |
|
85 SOME facts => |
|
86 Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th |
|
87 | NONE => Seq.empty |
|
88 end |
|
89 |
|
90 fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = |
|
91 let |
|
92 val thy = ProofContext.theory_of ctxt |
|
93 val timeout = Time.fromSeconds 30 |
|
94 val xs = run_atp force_full_types timeout i i ctxt th atp |
|
95 in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
|
96 |
|
97 val sledgehammer_as_unsound_oracle_tac = |
|
98 generic_sledgehammer_as_oracle_tac false |
|
99 val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true |
|
100 |
|
101 end; |
|