src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Mon Feb 03 19:32:02 2014 +0100 (2014-02-03 ago)
changeset 55297 1dfcd49f5dcb
parent 55288 1a4358d14ce2
child 55308 dc68f6fb88d2
permissions -rw-r--r--
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Generic prover abstraction for Sledgehammer.
     7 *)
     8 
     9 signature SLEDGEHAMMER_PROVER =
    10 sig
    11   type atp_failure = ATP_Proof.atp_failure
    12   type stature = ATP_Problem_Generate.stature
    13   type type_enc = ATP_Problem_Generate.type_enc
    14   type fact = Sledgehammer_Fact.fact
    15   type proof_method = Sledgehammer_Proof_Methods.proof_method
    16   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
    17   type minimize_command = Sledgehammer_Proof_Methods.minimize_command
    18 
    19   datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    20 
    21   type params =
    22     {debug : bool,
    23      verbose : bool,
    24      overlord : bool,
    25      spy : bool,
    26      blocking : bool,
    27      provers : string list,
    28      type_enc : string option,
    29      strict : bool,
    30      lam_trans : string option,
    31      uncurried_aliases : bool option,
    32      learn : bool,
    33      fact_filter : string option,
    34      max_facts : int option,
    35      fact_thresholds : real * real,
    36      max_mono_iters : int option,
    37      max_new_mono_instances : int option,
    38      isar_proofs : bool option,
    39      compress_isar : real,
    40      try0_isar : bool,
    41      smt_proofs : bool option,
    42      slice : bool,
    43      minimize : bool option,
    44      timeout : Time.time,
    45      preplay_timeout : Time.time,
    46      expect : string}
    47 
    48   type prover_problem =
    49     {comment : string,
    50      state : Proof.state,
    51      goal : thm,
    52      subgoal : int,
    53      subgoal_count : int,
    54      factss : (string * fact list) list}
    55 
    56   type prover_result =
    57     {outcome : atp_failure option,
    58      used_facts : (string * stature) list,
    59      used_from : fact list,
    60      run_time : Time.time,
    61      preplay : (proof_method * play_outcome) Lazy.lazy,
    62      message : proof_method * play_outcome -> string,
    63      message_tail : string}
    64 
    65   type prover =
    66     params -> ((string * string list) list -> string -> minimize_command)
    67     -> prover_problem -> prover_result
    68 
    69   val SledgehammerN : string
    70   val overlord_file_location_of_prover : string -> string * string
    71   val proof_banner : mode -> string -> string
    72   val extract_proof_method : params -> proof_method -> string * (string * string list) list
    73   val is_proof_method : string -> bool
    74   val is_atp : theory -> string -> bool
    75   val bunch_of_proof_methods : bool -> bool -> string -> proof_method list
    76   val is_fact_chained : (('a * stature) * 'b) -> bool
    77   val filter_used_facts :
    78     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    79     ((''a * stature) * 'b) list
    80   val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
    81     Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
    82   val remotify_atp_if_not_installed : theory -> string -> string option
    83   val isar_supported_prover_of : theory -> string -> string
    84   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    85     string -> proof_method * play_outcome -> 'a
    86   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    87     Proof.context
    88 
    89   val supported_provers : Proof.context -> unit
    90   val kill_provers : unit -> unit
    91   val running_provers : unit -> unit
    92   val messages : int option -> unit
    93 end;
    94 
    95 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
    96 struct
    97 
    98 open ATP_Util
    99 open ATP_Problem
   100 open ATP_Systems
   101 open ATP_Problem_Generate
   102 open ATP_Proof_Reconstruct
   103 open Metis_Tactic
   104 open Sledgehammer_Fact
   105 open Sledgehammer_Proof_Methods
   106 
   107 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   108 
   109 (* Identifier that distinguishes Sledgehammer from other tools that could use
   110    "Async_Manager". *)
   111 val SledgehammerN = "Sledgehammer"
   112 
   113 val proof_method_names = [metisN, smtN]
   114 val is_proof_method = member (op =) proof_method_names
   115 
   116 val is_atp = member (op =) o supported_atps
   117 
   118 fun remotify_atp_if_supported_and_not_already_remote thy name =
   119   if String.isPrefix remote_prefix name then
   120     SOME name
   121   else
   122     let val remote_name = remote_prefix ^ name in
   123       if is_atp thy remote_name then SOME remote_name else NONE
   124     end
   125 
   126 fun remotify_atp_if_not_installed thy name =
   127   if is_atp thy name andalso is_atp_installed thy name then SOME name
   128   else remotify_atp_if_supported_and_not_already_remote thy name
   129 
   130 type params =
   131   {debug : bool,
   132    verbose : bool,
   133    overlord : bool,
   134    spy : bool,
   135    blocking : bool,
   136    provers : string list,
   137    type_enc : string option,
   138    strict : bool,
   139    lam_trans : string option,
   140    uncurried_aliases : bool option,
   141    learn : bool,
   142    fact_filter : string option,
   143    max_facts : int option,
   144    fact_thresholds : real * real,
   145    max_mono_iters : int option,
   146    max_new_mono_instances : int option,
   147    isar_proofs : bool option,
   148    compress_isar : real,
   149    try0_isar : bool,
   150    smt_proofs : bool option,
   151    slice : bool,
   152    minimize : bool option,
   153    timeout : Time.time,
   154    preplay_timeout : Time.time,
   155    expect : string}
   156 
   157 type prover_problem =
   158   {comment : string,
   159    state : Proof.state,
   160    goal : thm,
   161    subgoal : int,
   162    subgoal_count : int,
   163    factss : (string * fact list) list}
   164 
   165 type prover_result =
   166   {outcome : atp_failure option,
   167    used_facts : (string * stature) list,
   168    used_from : fact list,
   169    run_time : Time.time,
   170    preplay : (proof_method * play_outcome) Lazy.lazy,
   171    message : proof_method * play_outcome -> string,
   172    message_tail : string}
   173 
   174 type prover =
   175   params -> ((string * string list) list -> string -> minimize_command)
   176   -> prover_problem -> prover_result
   177 
   178 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   179 
   180 fun proof_banner mode name =
   181   (case mode of
   182     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   183   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   184   | _ => "Try this")
   185 
   186 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   187   [Metis_Method (SOME full_type_enc, NONE)] @
   188   (if needs_full_types then
   189      [Metis_Method (SOME full_type_enc, NONE),
   190       Metis_Method (SOME really_full_type_enc, NONE),
   191       Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
   192    else
   193      [Metis_Method (NONE, NONE),
   194       Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
   195   [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
   196   (if smt_proofs then [SMT_Method] else [])
   197 
   198 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   199       (Metis_Method (type_enc', lam_trans')) =
   200     let
   201       val override_params =
   202         (if is_none type_enc' andalso is_none type_enc then []
   203          else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
   204         (if is_none lam_trans' andalso is_none lam_trans then []
   205          else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
   206     in (metisN, override_params) end
   207   | extract_proof_method _ SMT_Method = (smtN, [])
   208 
   209 (* based on "Mirabelle.can_apply" and generalized *)
   210 fun timed_apply timeout tac state i =
   211   let
   212     val {context = ctxt, facts, goal} = Proof.goal state
   213     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   214   in
   215     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   216   end
   217 
   218 fun timed_proof_method meth timeout ths =
   219   timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
   220 
   221 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
   222 
   223 fun filter_used_facts keep_chained used =
   224   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
   225 
   226 fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   227   let
   228     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   229   in
   230     if timeout = Time.zeroTime then
   231       (get_preferred meths, Not_Played)
   232     else
   233       let
   234         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
   235         val ths = pairs |> sort_wrt (fst o fst) |> map snd
   236         fun play [] [] = (get_preferred meths, Play_Failed)
   237           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
   238           | play timed_out (meth :: meths) =
   239             let
   240               val _ =
   241                 if verbose then
   242                   Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
   243                     "\" for " ^ string_of_time timeout ^ "...")
   244                 else
   245                   ()
   246               val timer = Timer.startRealTimer ()
   247             in
   248               (case timed_proof_method meth timeout ths state i of
   249                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
   250               | _ => play timed_out meths)
   251             end
   252             handle TimeLimit.TimeOut => play (meth :: timed_out) meths
   253       in
   254         play [] meths
   255       end
   256   end
   257 
   258 val canonical_isar_supported_prover = eN
   259 
   260 fun isar_supported_prover_of thy name =
   261   if is_atp thy name then name
   262   else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
   263 
   264 (* FIXME: See the analogous logic in the function "maybe_minimize" in
   265    "sledgehammer_prover_minimize.ML". *)
   266 fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
   267   let
   268     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
   269     val (min_name, override_params) =
   270       (case preplay of
   271         (meth, Played _) =>
   272         if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
   273       | _ => (maybe_isar_name, []))
   274   in minimize_command override_params min_name end
   275 
   276 val max_fact_instances = 10 (* FUDGE *)
   277 
   278 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   279   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   280   #> Config.put Monomorph.max_new_instances
   281        (max_new_instances |> the_default best_max_new_instances)
   282   #> Config.put Monomorph.max_thm_instances max_fact_instances
   283 
   284 fun supported_provers ctxt =
   285   let
   286     val thy = Proof_Context.theory_of ctxt
   287     val (remote_provers, local_provers) =
   288       proof_method_names @
   289       sort_strings (supported_atps thy) @
   290       sort_strings (SMT_Solver.available_solvers_of ctxt)
   291       |> List.partition (String.isPrefix remote_prefix)
   292   in
   293     Output.urgent_message ("Supported provers: " ^
   294                            commas (local_provers @ remote_provers) ^ ".")
   295   end
   296 
   297 fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   298 fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   299 val messages = Async_Manager.thread_messages SledgehammerN "prover"
   300 
   301 end;