(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

    Author:     Philipp Meyer, TU Muenchen

    Author:     Jasmin Blanchette, TU Muenchen

Minimization of fact list for Metis using ATPs.

*)

signature SLEDGEHAMMER_MINIMIZE =

sig

  type locality = Sledgehammer_Filter.locality

  type params = Sledgehammer.params

  val minimize_facts :

    params -> int -> int -> Proof.state -> ((string * locality) * thm list) list

    -> ((string * locality) * thm list) list option * string

  val run_minimize :

    params -> int -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit

end;

structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =

struct

open ATP_Proof

open Sledgehammer_Util

open Sledgehammer_Filter

open Sledgehammer_Translate

open Sledgehammer

(* wrapper for calling external prover *)

fun string_for_failure Unprovable = "Unprovable."

  | string_for_failure TimedOut = "Timed out."

  | string_for_failure Interrupted = "Interrupted."

  | string_for_failure _ = "Unknown error."

fun n_facts names =

  let val n = length names in

    string_of_int n ^ " fact" ^ plural_s n ^

    (if n > 0 then

       ": " ^ (names |> map fst

                     |> sort_distinct string_ord |> space_implode " ")

     else

       "")

  end

fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,

                 isar_shrink_factor, ...} : params) (prover : prover)

               explicit_apply timeout i n state axioms =

  let

    val _ =

      priority ("Testing " ^ n_facts (map fst axioms) ^ "...")

    val params =

      {blocking = true, debug = debug, verbose = verbose, overlord = overlord,

       provers = provers, full_types = full_types,

       explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),

       max_relevant = NONE, isar_proof = isar_proof,

       isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}

    val axioms =

      axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))

    val {context = ctxt, goal, ...} = Proof.goal state

    val problem =

      {state = state, goal = goal, subgoal = i, subgoal_count = n,

       axioms = axioms, only = true}

    val result as {outcome, used_axioms, ...} = prover params (K "") problem

  in

    priority (case outcome of

                SOME failure => string_for_failure failure

              | NONE =>

                if length used_axioms = length axioms then "Found proof."

                else "Found proof with " ^ n_facts used_axioms ^ ".");

    result

  end

(* minimalization of thms *)

fun filter_used_axioms used = filter (member (op =) used o fst)

fun sublinear_minimize _ [] p = p

  | sublinear_minimize test (x :: xs) (seen, result) =

    case test (xs @ seen) of

      result as {outcome = NONE, used_axioms, ...} : prover_result =>

      sublinear_minimize test (filter_used_axioms used_axioms xs)

                         (filter_used_axioms used_axioms seen, result)

    | _ => sublinear_minimize test xs (x :: seen, result)

(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer

   preprocessing time is included in the estimate below but isn't part of the

   timeout. *)

val fudge_msecs = 1000

fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."

  | minimize_facts (params as {provers = prover_name :: _, timeout, ...}) i n

                   state axioms =

  let

    val thy = Proof.theory_of state

    val prover = get_prover thy false prover_name

    val msecs = Time.toMilliseconds timeout

    val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")

    val {goal, ...} = Proof.goal state

    val (_, hyp_ts, concl_t) = strip_subgoal goal i

    val explicit_apply =

      not (forall (Meson.is_fol_term thy)

                  (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))

    fun do_test timeout =

      test_facts params prover explicit_apply timeout i n state

    val timer = Timer.startRealTimer ()

  in

    (case do_test timeout axioms of

       result as {outcome = NONE, used_axioms, ...} =>

       let

         val time = Timer.checkRealTimer timer

         val new_timeout =

           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)

           |> Time.fromMilliseconds

         val (min_thms, {message, ...}) =

           sublinear_minimize (do_test new_timeout)

               (filter_used_axioms used_axioms axioms) ([], result)

         val n = length min_thms

         val _ = priority (cat_lines

           ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^

            (case length (filter (curry (op =) Chained o snd o fst) min_thms) of

               0 => ""

             | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")

       in (SOME min_thms, message) end

     | {outcome = SOME TimedOut, ...} =>

       (NONE, "Timeout: You can increase the time limit using the \"timeout\" \

              \option (e.g., \"timeout = " ^

              string_of_int (10 + msecs div 1000) ^ " s\").")

     | {outcome = SOME UnknownError, ...} =>

       (* Failure sometimes mean timeout, unfortunately. *)

       (NONE, "Failure: No proof was found with the current time limit. You \

              \can increase the time limit using the \"timeout\" \

              \option (e.g., \"timeout = " ^

              string_of_int (10 + msecs div 1000) ^ " s\").")

     | {message, ...} => (NONE, "ATP error: " ^ message))

    handle ERROR msg => (NONE, "Error: " ^ msg)

  end

fun run_minimize params i refs state =

  let

    val ctxt = Proof.context_of state

    val reserved = reserved_isar_keyword_table ()

    val chained_ths = #facts (Proof.goal state)

    val axioms =

      maps (map (apsnd single)

            o name_thm_pairs_from_ref ctxt reserved chained_ths) refs

  in

    case subgoal_count state of

      0 => priority "No subgoal!"

    | n =>

      (kill_provers ();

       priority (#2 (minimize_facts params i n state axioms)))

  end

end;