src/HOL/Tools/try.ML

run synchronous Auto Tools in parallel

(*  Title:      HOL/Tools/try.ML
    Author:     Jasmin Blanchette, TU Muenchen

Try a combination of proof methods.
*)

signature TRY =
sig
  val auto : bool Unsynchronized.ref
  val invoke_try : Time.time option -> Proof.state -> bool
  val setup : theory -> theory
end;

structure Try : TRY =
struct

val auto = Unsynchronized.ref false

val _ =
  ProofGeneralPgip.add_preference Preferences.category_tracing
      (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")

val default_timeout = seconds 5.0

fun can_apply timeout_opt pre post tac st =
  let val {goal, ...} = Proof.goal st in
    case (case timeout_opt of
            SOME timeout => TimeLimit.timeLimit timeout
          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
      SOME (x, _) => nprems_of (post x) < nprems_of goal
    | NONE => false
  end
  handle TimeLimit.TimeOut => false

fun do_generic timeout_opt command pre post apply st =
  let val timer = Timer.startRealTimer () in
    if can_apply timeout_opt pre post apply st then
      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
    else
      NONE
  end

fun named_method thy name =
  Method.method thy (Args.src ((name, []), Position.none))

fun apply_named_method_on_first_goal name ctxt =
  let val thy = ProofContext.theory_of ctxt in
    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
  end
  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)

fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
  if not auto orelse run_if_auto then
    do_generic timeout_opt
               (name ^ (if all_goals andalso
                           nprems_of (#goal (Proof.goal st)) > 1 then
                          "[1]"
                        else
                          "")) I (#goal o Proof.goal)
               (apply_named_method_on_first_goal name (Proof.context_of st)) st
  else
    NONE

(* name * (all_goals, run_if_auto) *)
val named_methods =
  [("simp", (false, true)),
   ("auto", (true, true)),
   ("fast", (false, false)),
   ("fastsimp", (false, false)),
   ("force", (false, false)),
   ("blast", (false, true)),
   ("metis", (false, true)),
   ("linarith", (false, true)),
   ("presburger", (false, true))]
val do_methods = map do_named_method named_methods

fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"

fun do_try auto timeout_opt st =
  case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
                  |> map_filter I |> sort (int_ord o pairself snd) of
    [] => (if auto then () else writeln "No proof found."; (false, st))
  | xs as (s, _) :: _ =>
    let
      val xs = xs |> map swap |> AList.coalesce (op =)
                  |> map (swap o apsnd commas)
      val message =
        (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
        Markup.markup Markup.sendback
            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
             " " ^ s) ^
        "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    in
      (true, st |> (if auto then
                      Proof.goal_message
                          (fn () => Pretty.chunks [Pretty.str "",
                                    Pretty.markup Markup.hilite
                                                  [Pretty.str message]])
                    else
                      tap (fn _ => Output.urgent_message message)))
    end

val invoke_try = fst oo do_try false

val tryN = "try"

val _ =
  Outer_Syntax.improper_command tryN
      "try a combination of proof methods" Keyword.diag
      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
                                    o Toplevel.proof_of)))

val auto_try = do_try true NONE

val setup = Auto_Tools.register_tool (auto, auto_try)

end;