src/HOL/Mirabelle/Tools/mirabelle_metis.ML
author blanchet
Mon Jan 23 17:40:32 2012 +0100 (2012-01-23)
changeset 46320 0b8b73b49848
parent 45524 43ca06e6c168
child 46365 547d1a1dcaf6
permissions -rw-r--r--
renamed two files to make room for a new file
     1 (*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3 *)
     4 
     5 structure Mirabelle_Metis : MIRABELLE_ACTION =
     6 struct
     7 
     8 fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
     9 
    10 fun init _ = I
    11 fun done _ _ = ()
    12 
    13 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
    14   let
    15     val thms = Mirabelle.theorems_of_sucessful_proof post
    16     val names = map Thm.get_name_hint thms
    17     val add_info = if null names then I else suffix (":\n" ^ commas names)
    18 
    19     val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
    20 
    21     fun metis ctxt =
    22       Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt
    23                              (thms @ facts)
    24   in
    25     (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    26     |> prefix (metis_tag id)
    27     |> add_info
    28     |> log
    29   end
    30   handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
    31        | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
    32 
    33 fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
    34 
    35 end