src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

Mirabelle: actions are responsible for handling exceptions,
Mirabelle core logs only structural information,
measuring running times for sledgehammer and subsequent metis invocation,
Mirabelle produces reports for every theory (only for sledgehammer at the moment)

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

structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
struct

fun thms_of_name ctxt name =
  let
    val lex = OuterKeyword.get_lexicons
    val get = maps (ProofContext.get_fact ctxt o fst)
  in
    Source.of_string name
    |> Symbol.source {do_recover=false}
    |> OuterLex.source {do_recover=SOME false} lex Position.start
    |> OuterLex.source_proper
    |> Source.source OuterLex.stopper (SpecParse.xthms1 >> get) NONE
    |> Source.exhaust
  end

fun safe init done f x =
  let
    val y = init x
    val z = Exn.capture f y
    val _ = done y
  in Exn.release z end

fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
  | with_time false t = "failed (" ^ string_of_int t ^ ")"

val proverK = "prover"
val keepK = "keep"
val metisK = "metis"


local

fun init NONE = !AtpWrapper.destdir
  | init (SOME path) =
      let
        (* Warning: we implicitly assume single-threaded execution here! *)
        val old = !AtpWrapper.destdir
        val _ = AtpWrapper.destdir := path
      in old end

fun done path = AtpWrapper.destdir := path

fun run prover_name timeout st _ =
  let
    val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
    val atp_timeout = AtpManager.get_timeout () 
    val atp = prover atp_timeout NONE NONE prover_name 1
    val (success, (message, thm_names), _, _, _) =
      TimeLimit.timeLimit timeout atp (Proof.get_goal st)
  in (success, message, SOME thm_names) end
  handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
       | TimeLimit.TimeOut => (false, "time out", NONE)
       | ERROR msg => (false, "error: " ^ msg, NONE)

in

fun run_sledgehammer (args, st, timeout, log) =
  let
    val prover_name =
      AList.lookup (op =) args proverK
      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
    val dir = AList.lookup (op =) args keepK
    val ((success, msg, thm_names), time) =
      safe init done (Mirabelle.cpu_time (run prover_name timeout st)) dir
    fun sh_log s = log ("sledgehammer: " ^ with_time success time ^ " [" ^
      prover_name ^ "]" ^ s)
    val _ = if success then sh_log (":\n" ^ msg) else sh_log ""
  in if success then thm_names else NONE end

end


fun run_metis (args, st, timeout, log) thm_names =
  let
    fun get_thms ctxt = maps (thms_of_name ctxt)
    fun metis thms ctxt = MetisTools.metis_tac ctxt thms
    fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
    fun timed_metis thms =
      uncurry with_time (Mirabelle.cpu_time apply_metis thms)
      handle TimeLimit.TimeOut => "time out"
    fun log_metis s = log ("-----\nmetis (sledgehammer): " ^ s)
  in
    if not (AList.defined (op =) args metisK) then ()
    else if is_none thm_names then ()
    else
      these thm_names
      |> get_thms (Proof.context_of st)
      |> timed_metis
      |> log_metis
  end


fun sledgehammer_action args {pre, timeout, log, ...} =
  run_sledgehammer (args, pre, timeout, log)
  |> run_metis (args, pre, timeout, log)

fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)

end