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