(*  Title:      Tools/try.ML

    Author:     Jasmin Blanchette, TU Muenchen

Manager for tools that should be tried on conjectures.

*)

signature TRY =

sig

  type tool =

    string * (int * bool Unsynchronized.ref

              * (bool -> Proof.state -> bool * (string * Proof.state)))

  val tryN : string

  val auto_time_limit: real Unsynchronized.ref

  val register_tool : tool -> theory -> theory

  val get_tools : theory -> tool list

  val try_tools : Proof.state -> (string * string) option

end;

structure Try : TRY =

struct

type tool =

  string * (int * bool Unsynchronized.ref

            * (bool -> Proof.state -> bool * (string * Proof.state)))

val tryN = "try"

(* preferences *)

val auto_time_limit = Unsynchronized.ref 4.0

val auto_try_time_limitN = "auto-try-time-limit"

val _ =

  ProofGeneralPgip.add_preference Preferences.category_tracing

    (Preferences.real_pref auto_time_limit

      auto_try_time_limitN "Time limit for automatically tried tools (in seconds).")

(* configuration *)

structure Data = Theory_Data

(

  type T = tool list

  val empty = []

  val extend = I

  fun merge data : T = AList.merge (op =) (K true) data

)

val get_tools = Data.get

val register_tool = Data.map o Ord_List.insert (int_ord o pairself (#1 o snd))

(* try command *)

fun try_tools state =

  get_tools (Proof.theory_of state)

  |> tap (fn tools => "Trying " ^ commas_quote (map fst tools) ^ "..."

                      |> Output.urgent_message)

  |> Par_List.get_some

         (fn (name, (_, _, tool)) =>

             case try (tool false) state of

               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)

             | _ => NONE)

val _ =

  Outer_Syntax.improper_command tryN

      "try a combination of automatic proving and disproving tools" Keyword.diag

      (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))

(* automatic try *)

fun auto_try state =

  get_tools (Proof.theory_of state)

  |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)

  |> Par_List.get_some (fn tool =>

                           case try (tool true) state of

                             SOME (true, (_, state)) => SOME state

                           | _ => NONE)

  |> the_default state

(* Too large values are understood as milliseconds, ensuring compatibility with

   old setting files. No users can possibly in their right mind want the user

   interface to block for more than 100 seconds. *)

fun smart_seconds r =

  seconds (if r >= 100.0 then

             (legacy_feature (quote auto_try_time_limitN ^

                " expressed in milliseconds -- use seconds instead"); 0.001 * r)

           else

             r)

val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>

  if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then

    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state

    handle TimeLimit.TimeOut => state

  else

    state))

end;