equal
deleted
inserted
replaced
|
1 (* Title: HOL/Mirabelle/Actions/mirabelle_metis.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 structure Mirabelle_Metis : MIRABELLE_ACTION = |
|
6 struct |
|
7 |
|
8 fun metis_tag id = "#" ^ string_of_int id ^ " metis: " |
|
9 |
|
10 fun init _ = I |
|
11 fun done _ _ = () |
|
12 |
|
13 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = |
|
14 let |
|
15 val thms = Mirabelle.theorems_of_sucessful_proof post |
|
16 val names = map Thm.get_name_hint thms |
|
17 val add_info = if null names then I else suffix (":\n" ^ commas names) |
|
18 |
|
19 val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) |
|
20 |
|
21 fun metis ctxt = |
|
22 Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt |
|
23 (thms @ facts) |
|
24 in |
|
25 (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
|
26 |> prefix (metis_tag id) |
|
27 |> add_info |
|
28 |> log |
|
29 end |
|
30 handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout") |
|
31 | ERROR msg => log (metis_tag id ^ "error: " ^ msg) |
|
32 |
|
33 fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) |
|
34 |
|
35 end |