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