blanchet@42942
|
1 |
(* Title: HOL/ex/sledgehammer_tactics.ML
|
bulwahn@40881
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@42942
|
3 |
Copyright 2010, 2011
|
bulwahn@40881
|
4 |
|
bulwahn@40881
|
5 |
Sledgehammer as a tactic.
|
bulwahn@40881
|
6 |
*)
|
bulwahn@40881
|
7 |
|
bulwahn@40881
|
8 |
signature SLEDGEHAMMER_TACTICS =
|
bulwahn@40881
|
9 |
sig
|
blanchet@45319
|
10 |
type relevance_override = Sledgehammer_Filter.relevance_override
|
blanchet@45319
|
11 |
|
blanchet@45300
|
12 |
val sledgehammer_with_metis_tac :
|
blanchet@45319
|
13 |
Proof.context -> (string * string) list -> relevance_override -> int
|
blanchet@45319
|
14 |
-> tactic
|
blanchet@45300
|
15 |
val sledgehammer_as_oracle_tac :
|
blanchet@45319
|
16 |
Proof.context -> (string * string) list -> relevance_override -> int
|
blanchet@45319
|
17 |
-> tactic
|
bulwahn@40881
|
18 |
end;
|
bulwahn@40881
|
19 |
|
bulwahn@40881
|
20 |
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
|
bulwahn@40881
|
21 |
struct
|
blanchet@42942
|
22 |
|
blanchet@45319
|
23 |
open Sledgehammer_Filter
|
blanchet@45319
|
24 |
|
blanchet@45319
|
25 |
fun run_atp override_params relevance_override i n ctxt goal =
|
bulwahn@40881
|
26 |
let
|
bulwahn@41165
|
27 |
val chained_ths = [] (* a tactic has no chained ths *)
|
blanchet@46577
|
28 |
val params as {provers, relevance_thresholds, max_relevant, slice, ...} =
|
blanchet@45300
|
29 |
Sledgehammer_Isar.default_params ctxt override_params
|
blanchet@45300
|
30 |
val name = hd provers
|
blanchet@43862
|
31 |
val prover =
|
blanchet@43862
|
32 |
Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
|
bulwahn@41165
|
33 |
val default_max_relevant =
|
blanchet@46577
|
34 |
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice name
|
bulwahn@41165
|
35 |
val is_built_in_const =
|
blanchet@41335
|
36 |
Sledgehammer_Provers.is_built_in_const_for_prover ctxt name
|
blanchet@41335
|
37 |
val relevance_fudge =
|
blanchet@41335
|
38 |
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
|
blanchet@43929
|
39 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
|
blanchet@45483
|
40 |
val ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
|
bulwahn@41165
|
41 |
val facts =
|
blanchet@45483
|
42 |
Sledgehammer_Filter.nearly_all_facts ctxt ho_atp relevance_override
|
nik@45450
|
43 |
chained_ths hyp_ts concl_t
|
blanchet@45483
|
44 |
|> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
|
blanchet@44217
|
45 |
(the_default default_max_relevant max_relevant) is_built_in_const
|
blanchet@44217
|
46 |
relevance_fudge relevance_override chained_ths hyp_ts concl_t
|
bulwahn@40881
|
47 |
val problem =
|
blanchet@41338
|
48 |
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
|
blanchet@41484
|
49 |
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
|
blanchet@42612
|
50 |
smt_filter = NONE}
|
bulwahn@40881
|
51 |
in
|
blanchet@46391
|
52 |
(case prover params (K (K (K ""))) problem of
|
bulwahn@41165
|
53 |
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
|
bulwahn@41165
|
54 |
| _ => NONE)
|
bulwahn@41165
|
55 |
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
|
bulwahn@40881
|
56 |
end
|
bulwahn@40881
|
57 |
|
bulwahn@40881
|
58 |
fun thms_of_name ctxt name =
|
bulwahn@40881
|
59 |
let
|
bulwahn@40881
|
60 |
val lex = Keyword.get_lexicons
|
wenzelm@43232
|
61 |
val get = maps (Proof_Context.get_fact ctxt o fst)
|
bulwahn@40881
|
62 |
in
|
bulwahn@40881
|
63 |
Source.of_string name
|
bulwahn@40883
|
64 |
|> Symbol.source
|
bulwahn@40881
|
65 |
|> Token.source {do_recover=SOME false} lex Position.start
|
bulwahn@40881
|
66 |
|> Token.source_proper
|
bulwahn@40881
|
67 |
|> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
|
bulwahn@40881
|
68 |
|> Source.exhaust
|
bulwahn@40881
|
69 |
end
|
bulwahn@40881
|
70 |
|
blanchet@45319
|
71 |
fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
|
blanchet@45319
|
72 |
case run_atp override_params relevance_override i i ctxt th of
|
blanchet@45300
|
73 |
SOME facts =>
|
blanchet@46385
|
74 |
Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt
|
blanchet@46385
|
75 |
(maps (thms_of_name ctxt) facts) i th
|
blanchet@45300
|
76 |
| NONE => Seq.empty
|
bulwahn@40881
|
77 |
|
blanchet@45319
|
78 |
fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th =
|
bulwahn@40881
|
79 |
let
|
wenzelm@43232
|
80 |
val thy = Proof_Context.theory_of ctxt
|
blanchet@45319
|
81 |
val xs = run_atp (override_params @ [("sound", "true")]) relevance_override
|
blanchet@45319
|
82 |
i i ctxt th
|
blanchet@41605
|
83 |
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
|
blanchet@41605
|
84 |
|
bulwahn@40881
|
85 |
end;
|