src/HOL/Mirabelle/Tools/mirabelle_metis.ML

Made record parameter flexible to allow for extensions

(* Title:  mirabelle_metis.ML
   Author: Jasmin Blanchette and Sascha Boehme
*)

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, ...} =
  let
    val thms = Mirabelle.theorems_of_sucessful_proof post
    val names = map Thm.get_name thms
    val add_info = if null names then I else suffix (":\n" ^ commas names)

    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))

    fun metis ctxt = MetisTools.metis_tac 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