1 (* Title: mirabelle_sledgehammer.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme |
|
3 *) |
|
4 |
|
5 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION = |
|
6 struct |
|
7 |
|
8 fun thms_of_name ctxt name = |
|
9 let |
|
10 val lex = OuterKeyword.get_lexicons |
|
11 val get = maps (ProofContext.get_fact ctxt o fst) |
|
12 in |
|
13 Source.of_string name |
|
14 |> Symbol.source {do_recover=false} |
|
15 |> OuterLex.source {do_recover=SOME false} lex Position.start |
|
16 |> OuterLex.source_proper |
|
17 |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE |
|
18 |> Source.exhaust |
|
19 end |
|
20 |
|
21 fun safe init done f x = |
|
22 let |
|
23 val y = init x |
|
24 val z = Exn.capture f y |
|
25 val _ = done y |
|
26 in Exn.release z end |
|
27 |
|
28 val proverK = "prover" |
|
29 val keepK = "keep" |
|
30 val metisK = "metis" |
|
31 |
|
32 fun sledgehammer_action args {pre=st, timeout, log, ...} = |
|
33 let |
|
34 val prover_name = |
|
35 AList.lookup (op =) args proverK |
|
36 |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) |
|
37 |
|
38 val thy = Proof.theory_of st |
|
39 |
|
40 val prover = the (AtpManager.get_prover prover_name thy) |
|
41 val atp_timeout = AtpManager.get_timeout () |
|
42 |
|
43 (* run sledgehammer *) |
|
44 fun init NONE = !AtpWrapper.destdir |
|
45 | init (SOME path) = |
|
46 let |
|
47 (* Warning: we implicitly assume single-threaded execution here! *) |
|
48 val old = !AtpWrapper.destdir |
|
49 val _ = AtpWrapper.destdir := path |
|
50 in old end |
|
51 fun done path = AtpWrapper.destdir := path |
|
52 fun sh _ = |
|
53 let |
|
54 val atp = prover atp_timeout NONE NONE prover_name 1 |
|
55 val (success, (message, thm_names), _, _, _) = |
|
56 TimeLimit.timeLimit timeout atp (Proof.get_goal st) |
|
57 in (success, message, SOME thm_names) end |
|
58 handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME []) |
|
59 val (success, message, thm_names) = safe init done sh |
|
60 (AList.lookup (op =) args keepK) |
|
61 val _ = |
|
62 if success then log (quote prover_name ^ " succeeded:\n" ^ message) |
|
63 else log (prover_name ^ " failed") |
|
64 |
|
65 (* try metis *) |
|
66 fun get_thms ctxt = maps (thms_of_name ctxt) |
|
67 fun metis thms ctxt = MetisTools.metis_tac ctxt thms |
|
68 fun log_metis s = |
|
69 log ("applying metis: " ^ s) |
|
70 fun apply_metis thms = |
|
71 if Mirabelle.can_apply timeout (metis thms) st |
|
72 then "succeeded" else "failed" |
|
73 val _ = |
|
74 if not (AList.defined (op =) args metisK) then () |
|
75 else |
|
76 these thm_names |
|
77 |> get_thms (Proof.context_of st) |
|
78 |> apply_metis |
|
79 |> log_metis |
|
80 in () end |
|
81 |
|
82 fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args) |
|
83 |
|
84 end |
|