author | blanchet |
Wed, 18 Jul 2012 08:44:03 +0200 | |
changeset 48299 | 5e5c6616f0fe |
parent 48293 | 914ca0827804 |
child 48381 | 1b7d798460bb |
permissions | -rw-r--r-- |
47790 | 1 |
(* Title: HOL/TPTP/sledgehammer_tactics.ML |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41959
diff
changeset
|
3 |
Copyright 2010, 2011 |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
4 |
|
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
5 |
Sledgehammer as a tactic. |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
6 |
*) |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
7 |
|
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
8 |
signature SLEDGEHAMMER_TACTICS = |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
9 |
sig |
48292 | 10 |
type fact_override = Sledgehammer_Fact.fact_override |
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset
|
11 |
|
44429 | 12 |
val sledgehammer_with_metis_tac : |
48292 | 13 |
Proof.context -> (string * string) list -> fact_override -> int -> tactic |
44429 | 14 |
val sledgehammer_as_oracle_tac : |
48292 | 15 |
Proof.context -> (string * string) list -> fact_override -> int -> tactic |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
16 |
end; |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
17 |
|
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
18 |
structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
19 |
struct |
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41959
diff
changeset
|
20 |
|
48299 | 21 |
open Sledgehammer_Util |
48287 | 22 |
open Sledgehammer_Fact |
48299 | 23 |
open Sledgehammer_Provers |
24 |
open Sledgehammer_Filter_MaSh |
|
25 |
open Sledgehammer_Isar |
|
44462
d9a657c44380
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
blanchet
parents:
44429
diff
changeset
|
26 |
|
48292 | 27 |
fun run_prover override_params fact_override i n ctxt goal = |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
28 |
let |
48299 | 29 |
val mode = Normal |
48293 | 30 |
val params as {provers, max_facts, slice, ...} = |
48299 | 31 |
default_params ctxt override_params |
44429 | 32 |
val name = hd provers |
48299 | 33 |
val prover = get_prover ctxt mode name |
34 |
val default_max_facts = default_max_facts_for_prover ctxt slice name |
|
43088 | 35 |
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i |
48299 | 36 |
val ho_atp = exists (is_ho_atp ctxt) provers |
37 |
val reserved = reserved_isar_keyword_table () |
|
38 |
val css_table = clasimpset_rule_table_of ctxt |
|
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset
|
39 |
val facts = |
48299 | 40 |
nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts |
41 |
concl_t |
|
42 |
|> relevant_facts ctxt params name |
|
48293 | 43 |
(the_default default_max_facts max_facts) fact_override hyp_ts |
44 |
concl_t |
|
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
45 |
val problem = |
41090 | 46 |
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, |
48289 | 47 |
facts = facts |> map (apfst (apfst (fn name => name ()))) |
48299 | 48 |
|> map Untranslated_Fact} |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
49 |
in |
45520 | 50 |
(case prover params (K (K (K ""))) problem of |
40921
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset
|
51 |
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME |
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset
|
52 |
| _ => NONE) |
a516fbdd9931
improving sledgehammer_tactic and adding relevance filtering to the tactic
bulwahn
parents:
40635
diff
changeset
|
53 |
handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
54 |
end |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
55 |
|
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
56 |
fun thms_of_name ctxt name = |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
57 |
let |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
58 |
val lex = Keyword.get_lexicons |
42361 | 59 |
val get = maps (Proof_Context.get_fact ctxt o fst) |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
60 |
in |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
61 |
Source.of_string name |
40635
47004929bc71
ported sledgehammer_tactic to current development version
bulwahn
parents:
40633
diff
changeset
|
62 |
|> Symbol.source |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
63 |
|> Token.source {do_recover=SOME false} lex Position.start |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
64 |
|> Token.source_proper |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
65 |
|> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
66 |
|> Source.exhaust |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
67 |
end |
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
68 |
|
48292 | 69 |
fun sledgehammer_with_metis_tac ctxt override_params fact_override i th = |
70 |
let val override_params = override_params @ [("preplay_timeout", "0")] in |
|
71 |
case run_prover override_params fact_override i i ctxt th of |
|
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
72 |
SOME facts => |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
73 |
Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
74 |
(maps (thms_of_name ctxt) facts) i th |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
75 |
| NONE => Seq.empty |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
76 |
end |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
77 |
|
48292 | 78 |
fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th = |
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
79 |
let |
42361 | 80 |
val thy = Proof_Context.theory_of ctxt |
47766
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
81 |
val override_params = |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
82 |
override_params @ |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
83 |
[("preplay_timeout", "0"), |
9f7cdd5fff7c
more work on TPTP Isabelle and Sledgehammer tactics
blanchet
parents:
47532
diff
changeset
|
84 |
("minimize", "false")] |
48292 | 85 |
val xs = run_prover override_params fact_override i i ctxt th |
41357
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41243
diff
changeset
|
86 |
in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end |
ae76960d86a2
added "sledgehammer_tac" as possible reconstructor in Mirabelle
blanchet
parents:
41243
diff
changeset
|
87 |
|
40633
6cd611ceb64e
adding files to use sledgehammer as a tactic for non-interactive use
bulwahn
parents:
diff
changeset
|
88 |
end; |