src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML

eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);

(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
    Author:     Jasmin Blanchette, LMU Muenchen
    Author:     Martin Desharnais, LMU Muenchen

Isabelle tactics as Sledgehammer provers.
*)

signature SLEDGEHAMMER_PROVER_TACTIC =
sig
  type stature = ATP_Problem_Generate.stature
  type mode = Sledgehammer_Prover.mode
  type prover = Sledgehammer_Prover.prover
  type base_slice = Sledgehammer_ATP_Systems.base_slice

  val is_tactic_prover : string -> bool
  val good_slices_of_tactic_prover : string -> base_slice list
  val run_tactic_prover : mode -> string -> prover
end;

structure Sledgehammer_Prover_Tactic : SLEDGEHAMMER_PROVER_TACTIC =
struct

open ATP_Proof
open Sledgehammer_Proof_Methods
open Sledgehammer_Prover

val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method

local

val slices_of_max_facts = map (fn max_facts => (1, false, false, max_facts, "mesh"))

in

(* FUDGE *)
fun good_slices_of_tactic_prover "metis" = slices_of_max_facts [0, 64, 32, 8, 16, 4, 2, 1]
  | good_slices_of_tactic_prover "fastforce" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
  | good_slices_of_tactic_prover "simp" = slices_of_max_facts [0, 16, 32, 8, 64, 4, 1, 2]
  | good_slices_of_tactic_prover "auto" = slices_of_max_facts [0, 16, 32, 8, 4, 64, 2, 1]
  | good_slices_of_tactic_prover _ = slices_of_max_facts [0, 2, 8, 16, 32, 64]

end

fun meth_of "algebra" = Algebra_Method
  | meth_of "argo" = Argo_Method
  | meth_of "auto" = Auto_Method
  | meth_of "blast" = Blast_Method
  | meth_of "fastforce" = Fastforce_Method
  | meth_of "force" = Force_Method
  | meth_of "linarith" = Linarith_Method
  | meth_of "meson" = Meson_Method
  | meth_of "metis" = Metis_Method (NONE, NONE, [])
  | meth_of "order" = Order_Method
  | meth_of "presburger" = Presburger_Method
  | meth_of "satx" = SATx_Method
  | meth_of "simp" = Simp_Method
  | meth_of _ = Metis_Method (NONE, NONE, [])

fun run_tactic_prover mode name ({slices, timeout, ...} : params)
    ({state, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =
  let
    val (basic_slice as (slice_size, _, _, _, _), No_Slice) = slice
    val facts = facts_of_basic_slice basic_slice factss
    val ctxt = Proof.context_of state

    fun run_try0 () : Try0.result option =
      let
        val run_timeout = slice_timeout slice_size slices timeout
        fun is_cartouche str = String.isPrefix "\<open>" str andalso String.isSuffix "\<close>" str
        fun xref_of_fact (((name, _), thm) : Sledgehammer_Fact.fact) =
            let
              val xref =
                if is_cartouche name then
                  Facts.Fact (Pretty.pure_string_of (Thm.pretty_thm ctxt thm))
                else
                  Facts.named name
            in
              (xref, [])
            end
        val xrefs = map xref_of_fact facts
        val facts : Try0.facts = {usings = xrefs, simps = [], intros = [], elims = [], dests = []}
      in
        Try0.get_proof_method_or_noop name (SOME run_timeout) facts state
      end

    val timer = Timer.startRealTimer ()
    val (outcome, command) =
      (case run_try0 () of
        NONE => (SOME GaveUp, "")
      | SOME {command, ...} => (NONE, command))
      handle ERROR _ => (SOME GaveUp, "")
           | Exn.Interrupt_Breakdown => (SOME GaveUp, "")
           | Timeout.TIMEOUT _ => (SOME TimedOut, "")
    val run_time = Timer.checkRealTimer timer

    val used_facts =
      (case outcome of
        NONE => (found_something name; map fst facts)
      | SOME _ => [])

    val message = fn preplay_outcome =>
      (case outcome of
        NONE =>
        let
          val banner = proof_banner mode name
        in
          (case preplay_outcome of
            NONE => try_command_line banner (Played run_time) command
          | SOME preplay_result =>
              one_line_proof_text (preplay_result, banner, subgoal, subgoal_count))
        end
      | SOME failure => string_of_atp_failure failure)
  in
    {outcome = outcome, used_facts = used_facts, used_from = facts,
     preferred_methss = (meth_of name, []), run_time = run_time, message = message}
  end

end;