src/HOL/Mirabelle/Tools/mirabelle_metis.ML
author sultana
Tue Apr 24 13:59:29 2012 +0100 (2012-04-24)
changeset 47730 15f4309bb9eb
parent 47477 src/HOL/Mirabelle/Actions/mirabelle_metis.ML@3fabf352243e
child 47847 7cddb6c8f93c
permissions -rw-r--r--
reversed Tools to Actions Mirabelle renaming;
sultana@47477
     1
(*  Title:      HOL/Mirabelle/Actions/mirabelle_metis.ML
wenzelm@32564
     2
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
boehmes@32385
     3
*)
boehmes@32385
     4
boehmes@32385
     5
structure Mirabelle_Metis : MIRABELLE_ACTION =
boehmes@32385
     6
struct
boehmes@32385
     7
boehmes@32521
     8
fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
boehmes@32521
     9
boehmes@32521
    10
fun init _ = I
boehmes@32521
    11
fun done _ _ = ()
boehmes@32521
    12
wenzelm@32567
    13
fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
boehmes@32385
    14
  let
boehmes@32385
    15
    val thms = Mirabelle.theorems_of_sucessful_proof post
wenzelm@36743
    16
    val names = map Thm.get_name_hint thms
boehmes@32472
    17
    val add_info = if null names then I else suffix (":\n" ^ commas names)
boehmes@32385
    18
wenzelm@42361
    19
    val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
boehmes@32385
    20
blanchet@45524
    21
    fun metis ctxt =
blanchet@46365
    22
      Metis_Tactic.metis_tac [] ATP_Problem_Generate.liftingN ctxt
blanchet@46320
    23
                             (thms @ facts)
boehmes@32385
    24
  in
boehmes@32469
    25
    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
boehmes@32521
    26
    |> prefix (metis_tag id)
boehmes@32472
    27
    |> add_info
boehmes@32472
    28
    |> log
boehmes@32385
    29
  end
boehmes@32521
    30
  handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
boehmes@32521
    31
       | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
boehmes@32385
    32
boehmes@32521
    33
fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
boehmes@32385
    34
boehmes@32385
    35
end