author | wenzelm |
Sat, 05 Mar 2016 17:01:45 +0100 | |
changeset 62519 | a564458f94db |
parent 47847 | 7cddb6c8f93c |
child 63337 | ae9330fdbc16 |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML |
32564 | 2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
3 |
*) |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
4 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
5 |
structure Mirabelle_Metis : MIRABELLE_ACTION = |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
6 |
struct |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
7 |
|
32521 | 8 |
fun metis_tag id = "#" ^ string_of_int id ^ " metis: " |
9 |
||
10 |
fun init _ = I |
|
11 |
fun done _ _ = () |
|
12 |
||
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
13 |
fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) = |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
14 |
let |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
15 |
val thms = Mirabelle.theorems_of_sucessful_proof post |
36743
ce2297415b54
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
wenzelm
parents:
35830
diff
changeset
|
16 |
val names = map Thm.get_name_hint thms |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
17 |
val add_info = if null names then I else suffix (":\n" ^ commas names) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
18 |
|
42361 | 19 |
val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
20 |
|
45524 | 21 |
fun metis ctxt = |
46365 | 22 |
Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt |
46320 | 23 |
(thms @ facts) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
24 |
in |
32469 | 25 |
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
32521 | 26 |
|> prefix (metis_tag id) |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
27 |
|> add_info |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
28 |
|> log |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
29 |
end |
62519 | 30 |
handle Timeout.TIMEOUT _ => log (metis_tag id ^ "timeout") |
32521 | 31 |
| ERROR msg => log (metis_tag id ^ "error: " ^ msg) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
32 |
|
32521 | 33 |
fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
34 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
35 |
end |