--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Tue Apr 24 13:59:29 2012 +0100
@@ -0,0 +1,35 @@
+(* Title: HOL/Mirabelle/Actions/mirabelle_metis.ML
+ Author: Jasmin Blanchette and Sascha Boehme, TU Munich
+*)
+
+structure Mirabelle_Metis : MIRABELLE_ACTION =
+struct
+
+fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
+ let
+ val thms = Mirabelle.theorems_of_sucessful_proof post
+ val names = map Thm.get_name_hint thms
+ val add_info = if null names then I else suffix (":\n" ^ commas names)
+
+ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
+
+ fun metis ctxt =
+ Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt
+ (thms @ facts)
+ in
+ (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
+ |> prefix (metis_tag id)
+ |> add_info
+ |> log
+ end
+ handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+ | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
+
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
+
+end