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

     Author:     Fabian Immler, TU Muenchen

     Author:     Makarius

     Author:     Jasmin Blanchette, TU Muenchen

 Sledgehammer's heart.

 *)

 signature SLEDGEHAMMER_RUN =

 sig

   type relevance_override = Sledgehammer_Filter.relevance_override

   type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command

   type params = Sledgehammer_Provers.params

   type prover = Sledgehammer_Provers.prover

   val auto_minimize_min_facts : int Unsynchronized.ref

   val get_minimizing_prover : Proof.context -> bool -> string -> prover

   val run_sledgehammer :

     params -> bool -> int -> relevance_override -> (string -> minimize_command)

     -> Proof.state -> bool * Proof.state

 end;

 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =

 struct

 open Sledgehammer_Util

 open Sledgehammer_Filter

 open Sledgehammer_ATP_Translate

 open Sledgehammer_Provers

 open Sledgehammer_Minimize

 fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i

                        n goal =

   quote name ^

   (if verbose then

      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts

    else

      "") ^

   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^

   (if blocking then

      "."

    else

      ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))

 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)

 fun get_minimizing_prover ctxt auto name

         (params as {debug, verbose, explicit_apply, ...}) minimize_command

         (problem as {state, subgoal, subgoal_count, facts, ...}) =

   get_prover ctxt auto name params minimize_command problem

   |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>

          if is_some outcome then

            result

          else

            let

              val (used_facts, message) =

                if length used_facts >= !auto_minimize_min_facts then

                  minimize_facts name params (SOME explicit_apply) (not verbose)

                      subgoal subgoal_count state

                      (filter_used_facts used_facts

                           (map (apsnd single o untranslated_fact) facts))

                  |>> Option.map (map fst)

                else

                  (SOME used_facts, message)

            in

              case used_facts of

                SOME used_facts =>

                (if debug andalso not (null used_facts) then

                   facts ~~ (0 upto length facts - 1)

                   |> map (fn (fact, j) =>

                              fact |> untranslated_fact |> apsnd (K j))

                   |> filter_used_facts used_facts

                   |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)

                   |> commas

                   |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^

                               quote name ^ " proof (of " ^

                               string_of_int (length facts) ^ "): ") "."

                   |> Output.urgent_message

                 else

                   ();

                 {outcome = NONE, used_facts = used_facts,

                  run_time_in_msecs = run_time_in_msecs, message = message})

              | NONE => result

            end)

 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,

                               expect, ...})

         auto minimize_command only

         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =

   let

     val ctxt = Proof.context_of state

     val birth_time = Time.now ()

     val death_time = Time.+ (birth_time, timeout)

     val max_relevant =

       max_relevant

       |> the_default (default_max_relevant_for_prover ctxt slicing name)

     val num_facts = length facts |> not only ? Integer.min max_relevant

     val desc =

       prover_description ctxt params name num_facts subgoal subgoal_count goal

     val problem =

       {state = state, goal = goal, subgoal = subgoal,

        subgoal_count = subgoal_count, facts = facts |> take num_facts,

        smt_filter = smt_filter}

     fun really_go () =

       problem

       |> get_minimizing_prover ctxt auto name params (minimize_command name)

       |> (fn {outcome, message, ...} =>

              (if is_some outcome then "none" else "some" (* sic *), message))

     fun go () =

       let

         val (outcome_code, message) =

           if debug then

             really_go ()

           else

             (really_go ()

              handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")

                   | exn =>

                     if Exn.is_interrupt exn then

                       reraise exn

                     else

                       ("unknown", "Internal error:\n" ^

                                   ML_Compiler.exn_message exn ^ "\n"))

         val _ =

           (* The "expect" argument is deliberately ignored if the prover is

              missing so that the "Metis_Examples" can be processed on any

              machine. *)

           if expect = "" orelse outcome_code = expect orelse

              not (is_prover_installed ctxt name) then

             ()

           else if blocking then

             error ("Unexpected outcome: " ^ quote outcome_code ^ ".")

           else

             warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");

       in (outcome_code = "some", message) end

   in

     if auto then

       let val (success, message) = TimeLimit.timeLimit timeout go () in

         (success, state |> success ? Proof.goal_message (fn () =>

              Pretty.chunks [Pretty.str "",

                             Pretty.mark Markup.hilite (Pretty.str message)]))

       end

     else if blocking then

       let val (success, message) = TimeLimit.timeLimit timeout go () in

         List.app Output.urgent_message

                  (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);

         (success, state)

       end

     else

       (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);

        (false, state))

   end

 fun class_of_smt_solver ctxt name =

   ctxt |> select_smt_solver name

        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class

 (* Makes backtraces more transparent and might be more efficient as well. *)

 fun smart_par_list_map _ [] = []

   | smart_par_list_map f [x] = [f x]

   | smart_par_list_map f xs = Par_List.map f xs

 fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p

   | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"

 val auto_max_relevant_divisor = 2 (* FUDGE *)

 fun run_sledgehammer (params as {debug, blocking, provers, type_sys,

                                  relevance_thresholds, max_relevant, slicing,

                                  timeout, ...})

         auto i (relevance_override as {only, ...}) minimize_command state =

   if null provers then

     error "No prover is set."

   else case subgoal_count state of

     0 => (Output.urgent_message "No subgoal!"; (false, state))

   | n =>

     let

       val _ = Proof.assert_backward state

       val print = if auto then K () else Output.urgent_message

       val state =

         state |> Proof.map_context (Config.put SMT_Config.verbose debug)

       val ctxt = Proof.context_of state

       val thy = Proof_Context.theory_of ctxt

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

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

       val _ = () |> not blocking ? kill_provers

       val _ = case find_first (not o is_prover_supported ctxt) provers of

                 SOME name => error ("No such prover: " ^ name ^ ".")

               | NONE => ()

       val _ = print "Sledgehammering..."

       val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)

       fun launch_provers state get_facts translate maybe_smt_filter provers =

         let

           val facts = get_facts ()

           val num_facts = length facts

           val facts = facts ~~ (0 upto num_facts - 1)

                       |> map (translate num_facts)

           val problem =

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

              facts = facts,

              smt_filter = maybe_smt_filter

                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}

           val launch = launch_prover params auto minimize_command only

         in

           if auto then

             fold (fn prover => fn (true, state) => (true, state)

                                 | (false, _) => launch problem prover)

                  provers (false, state)

           else

             provers

             |> (if blocking then smart_par_list_map else map) (launch problem)

             |> exists fst |> rpair state

         end

       fun get_facts label relevance_fudge provers =

         let

           val max_max_relevant =

             case max_relevant of

               SOME n => n

             | NONE =>

               0 |> fold (Integer.max

                          o default_max_relevant_for_prover ctxt slicing)

                         provers

                 |> auto ? (fn n => n div auto_max_relevant_divisor)

           val is_built_in_const =

             is_built_in_const_for_prover ctxt (hd provers)

         in

           relevant_facts ctxt relevance_thresholds max_max_relevant

                          is_built_in_const relevance_fudge relevance_override

                          chained_ths hyp_ts concl_t

           |> tap (fn facts =>

                      if debug then

                        label ^ plural_s (length provers) ^ ": " ^

                        (if null facts then

                           "Found no relevant facts."

                         else

                           "Including (up to) " ^ string_of_int (length facts) ^

                           " relevant fact" ^ plural_s (length facts) ^ ":\n" ^

                           (facts |> map (fst o fst) |> space_implode " ") ^ ".")

                        |> print

                      else

                        ())

         end

       fun launch_atps accum =

         if null atps then

           accum

         else

           launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps)

                          (K (Untranslated_Fact o fst)) (K (K NONE)) atps

       fun launch_smts accum =

         if null smts then

           accum

         else

           let

             val facts = get_facts "SMT solver" smt_relevance_fudge smts

             val weight = SMT_Weighted_Fact oo weight_smt_fact thy

             fun smt_filter facts =

               (if debug then curry (op o) SOME

                else TimeLimit.timeLimit timeout o try)

                   (SMT_Solver.smt_filter_preprocess state (facts ()))

           in

             smts |> map (`(class_of_smt_solver ctxt))

                  |> AList.group (op =)

                  |> map (launch_provers state (K facts) weight smt_filter o snd)

                  |> exists fst |> rpair state

           end

       fun launch_atps_and_smt_solvers () =

         [launch_atps, launch_smts]

         |> smart_par_list_map (fn f => f (false, state) |> K ())

         handle ERROR msg => (print ("Error: " ^ msg); error msg)

     in

       (false, state)

       |> (if blocking then launch_atps #> not auto ? launch_smts

           else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))

       handle TimeLimit.TimeOut =>

              (print "Sledgehammer ran out of time."; (false, state))

     end

 end;