src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
author blanchet
Fri Jan 31 16:07:20 2014 +0100 (2014-01-31 ago)
changeset 55211 5d027af93a08
parent 55208 11dd3d1da83b
child 55212 5832470d956e
permissions -rw-r--r--
moved ML code around
     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 reconstructor = Sledgehammer_Reconstructor.reconstructor
    16   type play_outcome = Sledgehammer_Reconstructor.play_outcome
    17   type minimize_command = Sledgehammer_Reconstructor.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      slice : bool,
    42      minimize : bool option,
    43      timeout : Time.time,
    44      preplay_timeout : Time.time,
    45      expect : string}
    46 
    47   type prover_problem =
    48     {comment : string,
    49      state : Proof.state,
    50      goal : thm,
    51      subgoal : int,
    52      subgoal_count : int,
    53      factss : (string * fact list) list}
    54 
    55   type prover_result =
    56     {outcome : atp_failure option,
    57      used_facts : (string * stature) list,
    58      used_from : fact list,
    59      run_time : Time.time,
    60      preplay : (reconstructor * play_outcome) Lazy.lazy,
    61      message : reconstructor * play_outcome -> string,
    62      message_tail : string}
    63 
    64   type prover =
    65     params -> ((string * string list) list -> string -> minimize_command)
    66     -> prover_problem -> prover_result
    67 
    68   val dest_dir : string Config.T
    69   val problem_prefix : string Config.T
    70   val completish : bool Config.T
    71   val atp_full_names : bool Config.T
    72   val SledgehammerN : string
    73   val plain_metis : reconstructor
    74   val overlord_file_location_of_prover : string -> string * string
    75   val proof_banner : mode -> string -> string
    76   val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
    77   val is_reconstructor : string -> bool
    78   val is_atp : theory -> string -> bool
    79   val is_ho_atp: Proof.context -> string -> bool
    80   val supported_provers : Proof.context -> unit
    81   val kill_provers : unit -> unit
    82   val running_provers : unit -> unit
    83   val messages : int option -> unit
    84   val is_fact_chained : (('a * stature) * 'b) -> bool
    85   val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
    86   val filter_used_facts :
    87     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    88     ((''a * stature) * 'b) list
    89   val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
    90     Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
    91   val remotify_atp_if_not_installed : theory -> string -> string option
    92   val isar_supported_prover_of : theory -> string -> string
    93   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
    94     string -> reconstructor * play_outcome -> 'a
    95   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    96     Proof.context
    97   val run_reconstructor : mode -> string -> prover
    98 end;
    99 
   100 structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
   101 struct
   102 
   103 open ATP_Util
   104 open ATP_Problem
   105 open ATP_Proof
   106 open ATP_Systems
   107 open ATP_Problem_Generate
   108 open ATP_Proof_Reconstruct
   109 open Metis_Tactic
   110 open Sledgehammer_Util
   111 open Sledgehammer_Fact
   112 open Sledgehammer_Reconstructor
   113 open Sledgehammer_Isar
   114 
   115 (* Empty string means create files in Isabelle's temporary files directory. *)
   116 val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   117 val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
   118 val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
   119 
   120 (* In addition to being easier to read, readable names are often much shorter,
   121    especially if types are mangled in names. This makes a difference for some
   122    provers (e.g., E). For these reason, short names are enabled by default. *)
   123 val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
   124 
   125 datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   126 
   127 (* Identifier that distinguishes Sledgehammer from other tools that could use
   128    "Async_Manager". *)
   129 val SledgehammerN = "Sledgehammer"
   130 
   131 val reconstructor_names = [metisN, smtN]
   132 val plain_metis = Metis (hd partial_type_encs, combsN)
   133 val is_reconstructor = member (op =) reconstructor_names
   134 
   135 val is_atp = member (op =) o supported_atps
   136 
   137 fun is_atp_of_format is_format ctxt name =
   138   let val thy = Proof_Context.theory_of ctxt in
   139     (case try (get_atp thy) name of
   140       SOME config =>
   141       exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
   142     | NONE => false)
   143   end
   144 
   145 val is_ho_atp = is_atp_of_format is_format_higher_order
   146 
   147 fun remotify_atp_if_supported_and_not_already_remote thy name =
   148   if String.isPrefix remote_prefix name then
   149     SOME name
   150   else
   151     let val remote_name = remote_prefix ^ name in
   152       if is_atp thy remote_name then SOME remote_name else NONE
   153     end
   154 
   155 fun remotify_atp_if_not_installed thy name =
   156   if is_atp thy name andalso is_atp_installed thy name then SOME name
   157   else remotify_atp_if_supported_and_not_already_remote thy name
   158 
   159 fun supported_provers ctxt =
   160   let
   161     val thy = Proof_Context.theory_of ctxt
   162     val (remote_provers, local_provers) =
   163       reconstructor_names @
   164       sort_strings (supported_atps thy) @
   165       sort_strings (SMT_Solver.available_solvers_of ctxt)
   166       |> List.partition (String.isPrefix remote_prefix)
   167   in
   168     Output.urgent_message ("Supported provers: " ^
   169                            commas (local_provers @ remote_provers) ^ ".")
   170   end
   171 
   172 fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   173 fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   174 val messages = Async_Manager.thread_messages SledgehammerN "prover"
   175 
   176 type params =
   177   {debug : bool,
   178    verbose : bool,
   179    overlord : bool,
   180    spy : bool,
   181    blocking : bool,
   182    provers : string list,
   183    type_enc : string option,
   184    strict : bool,
   185    lam_trans : string option,
   186    uncurried_aliases : bool option,
   187    learn : bool,
   188    fact_filter : string option,
   189    max_facts : int option,
   190    fact_thresholds : real * real,
   191    max_mono_iters : int option,
   192    max_new_mono_instances : int option,
   193    isar_proofs : bool option,
   194    compress_isar : real,
   195    try0_isar : bool,
   196    slice : bool,
   197    minimize : bool option,
   198    timeout : Time.time,
   199    preplay_timeout : Time.time,
   200    expect : string}
   201 
   202 type prover_problem =
   203   {comment : string,
   204    state : Proof.state,
   205    goal : thm,
   206    subgoal : int,
   207    subgoal_count : int,
   208    factss : (string * fact list) list}
   209 
   210 type prover_result =
   211   {outcome : atp_failure option,
   212    used_facts : (string * stature) list,
   213    used_from : fact list,
   214    run_time : Time.time,
   215    preplay : (reconstructor * play_outcome) Lazy.lazy,
   216    message : reconstructor * play_outcome -> string,
   217    message_tail : string}
   218 
   219 type prover =
   220   params -> ((string * string list) list -> string -> minimize_command)
   221   -> prover_problem -> prover_result
   222 
   223 fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   224 
   225 fun proof_banner mode name =
   226   (case mode of
   227     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   228   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   229   | _ => "Try this")
   230 
   231 fun bunch_of_reconstructors needs_full_types lam_trans =
   232   if needs_full_types then
   233     [Metis (full_type_enc, lam_trans false),
   234      Metis (really_full_type_enc, lam_trans false),
   235      Metis (full_type_enc, lam_trans true),
   236      Metis (really_full_type_enc, lam_trans true),
   237      SMT]
   238   else
   239     [Metis (partial_type_enc, lam_trans false),
   240      Metis (full_type_enc, lam_trans false),
   241      Metis (no_typesN, lam_trans true),
   242      Metis (really_full_type_enc, lam_trans true),
   243      SMT]
   244 
   245 fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
   246     let
   247       val override_params =
   248         (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
   249          else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
   250         (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
   251          else [("lam_trans", [lam_trans'])])
   252     in (metisN, override_params) end
   253   | extract_reconstructor _ SMT = (smtN, [])
   254 
   255 (* based on "Mirabelle.can_apply" and generalized *)
   256 fun timed_apply timeout tac state i =
   257   let
   258     val {context = ctxt, facts, goal} = Proof.goal state
   259     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   260   in
   261     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   262   end
   263 
   264 fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
   265   | tac_of_reconstructor SMT = SMT_Solver.smt_tac
   266 
   267 fun timed_reconstructor reconstr debug timeout ths =
   268   timed_apply timeout (silence_reconstructors debug
   269     #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
   270 
   271 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
   272 
   273 fun filter_used_facts keep_chained used =
   274   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
   275 
   276 fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
   277   let
   278     fun get_preferred reconstrs =
   279       if member (op =) reconstrs preferred then preferred
   280       else List.last reconstrs
   281   in
   282     if timeout = Time.zeroTime then
   283       (get_preferred reconstrs, Not_Played)
   284     else
   285       let
   286         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
   287         val ths = pairs |> sort_wrt (fst o fst) |> map snd
   288         fun play [] [] = (get_preferred reconstrs, Play_Failed)
   289           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
   290           | play timed_out (reconstr :: reconstrs) =
   291             let
   292               val _ =
   293                 if verbose then
   294                   Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
   295                     "\" for " ^ string_of_time timeout ^ "...")
   296                 else
   297                   ()
   298               val timer = Timer.startRealTimer ()
   299             in
   300               case timed_reconstructor reconstr debug timeout ths state i of
   301                 SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
   302               | _ => play timed_out reconstrs
   303             end
   304             handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
   305       in
   306         play [] reconstrs
   307       end
   308   end
   309 
   310 val canonical_isar_supported_prover = eN
   311 
   312 fun isar_supported_prover_of thy name =
   313   if is_atp thy name then name
   314   else the_default name (remotify_atp_if_not_installed thy canonical_isar_supported_prover)
   315 
   316 (* FIXME: See the analogous logic in the function "maybe_minimize" in
   317    "sledgehammer_prover_minimize.ML". *)
   318 fun choose_minimize_command thy (params as {isar_proofs, ...}) minimize_command name preplay =
   319   let
   320     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
   321     val (min_name, override_params) =
   322       (case preplay of
   323         (reconstr, Played _) =>
   324         if isar_proofs = SOME true then (maybe_isar_name, [])
   325         else extract_reconstructor params reconstr
   326       | _ => (maybe_isar_name, []))
   327   in minimize_command override_params min_name end
   328 
   329 val max_fact_instances = 10 (* FUDGE *)
   330 
   331 fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
   332   Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
   333   #> Config.put Monomorph.max_new_instances
   334        (max_new_instances |> the_default best_max_new_instances)
   335   #> Config.put Monomorph.max_thm_instances max_fact_instances
   336 
   337 fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
   338     minimize_command
   339     ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   340   let
   341     val reconstr =
   342       if name = metisN then
   343         Metis (type_enc |> the_default (hd partial_type_encs),
   344                lam_trans |> the_default default_metis_lam_trans)
   345       else if name = smtN then
   346         SMT
   347       else
   348         raise Fail ("unknown reconstructor: " ^ quote name)
   349     val used_facts = facts |> map fst
   350   in
   351     (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
   352        state subgoal reconstr [reconstr] of
   353       play as (_, Played time) =>
   354       {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
   355        preplay = Lazy.value play,
   356        message =
   357          fn play =>
   358             let
   359               val (_, override_params) = extract_reconstructor params reconstr
   360               val one_line_params =
   361                 (play, proof_banner mode name, used_facts, minimize_command override_params name,
   362                  subgoal, subgoal_count)
   363               val num_chained = length (#facts (Proof.goal state))
   364             in
   365               one_line_proof_text num_chained one_line_params
   366             end,
   367        message_tail = ""}
   368     | play =>
   369       let
   370         val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
   371       in
   372         {outcome = SOME failure, used_facts = [], used_from = [],
   373          run_time = Time.zeroTime, preplay = Lazy.value play,
   374          message = fn _ => string_of_atp_failure failure, message_tail = ""}
   375       end)
   376   end
   377 
   378 end;