author | blanchet |
Mon, 06 Jun 2011 20:56:06 +0200 | |
changeset 43212 | 050a03afe024 |
parent 43205 | 23b81469499f |
child 44651 | 5d6a11e166cf |
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 |
|
43212 | 21 |
fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts) |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
22 |
in |
32469 | 23 |
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |
32521 | 24 |
|> prefix (metis_tag id) |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
25 |
|> add_info |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
26 |
|> log |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
27 |
end |
32521 | 28 |
handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout") |
29 |
| 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
|
30 |
|
32521 | 31 |
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
|
32 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
diff
changeset
|
33 |
end |