author | blanchet |
Wed, 16 Nov 2011 17:59:58 +0100 | |
changeset 45524 | 43ca06e6c168 |
parent 44651 | 5d6a11e166cf |
child 46320 | 0b8b73b49848 |
permissions | -rw-r--r-- |
32564 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML |
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 = |
22 |
Metis_Tactic.metis_tac [] ATP_Translate.lam_liftingN ctxt (thms @ facts) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
23 |
in |
32469 | 24 |
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
32521 | 25 |
|> prefix (metis_tag id) |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
26 |
|> add_info |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
27 |
|> log |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
28 |
end |
32521 | 29 |
handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout") |
30 |
| 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
|
31 |
|
32521 | 32 |
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
|
33 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
34 |
end |