src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55212 5832470d956e
parent 55211 5d027af93a08
child 55285 e88ad20035f4
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:07:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:10:39 2014 +0100
     1.3 @@ -65,10 +65,6 @@
     1.4      params -> ((string * string list) list -> string -> minimize_command)
     1.5      -> prover_problem -> prover_result
     1.6  
     1.7 -  val dest_dir : string Config.T
     1.8 -  val problem_prefix : string Config.T
     1.9 -  val completish : bool Config.T
    1.10 -  val atp_full_names : bool Config.T
    1.11    val SledgehammerN : string
    1.12    val plain_metis : reconstructor
    1.13    val overlord_file_location_of_prover : string -> string * string
    1.14 @@ -76,13 +72,8 @@
    1.15    val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
    1.16    val is_reconstructor : string -> bool
    1.17    val is_atp : theory -> string -> bool
    1.18 -  val is_ho_atp: Proof.context -> string -> bool
    1.19 -  val supported_provers : Proof.context -> unit
    1.20 -  val kill_provers : unit -> unit
    1.21 -  val running_provers : unit -> unit
    1.22 -  val messages : int option -> unit
    1.23 +  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
    1.24    val is_fact_chained : (('a * stature) * 'b) -> bool
    1.25 -  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
    1.26    val filter_used_facts :
    1.27      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
    1.28      ((''a * stature) * 'b) list
    1.29 @@ -94,7 +85,11 @@
    1.30      string -> reconstructor * play_outcome -> 'a
    1.31    val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
    1.32      Proof.context
    1.33 -  val run_reconstructor : mode -> string -> prover
    1.34 +
    1.35 +  val supported_provers : Proof.context -> unit
    1.36 +  val kill_provers : unit -> unit
    1.37 +  val running_provers : unit -> unit
    1.38 +  val messages : int option -> unit
    1.39  end;
    1.40  
    1.41  structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
    1.42 @@ -102,25 +97,12 @@
    1.43  
    1.44  open ATP_Util
    1.45  open ATP_Problem
    1.46 -open ATP_Proof
    1.47  open ATP_Systems
    1.48  open ATP_Problem_Generate
    1.49  open ATP_Proof_Reconstruct
    1.50  open Metis_Tactic
    1.51 -open Sledgehammer_Util
    1.52  open Sledgehammer_Fact
    1.53  open Sledgehammer_Reconstructor
    1.54 -open Sledgehammer_Isar
    1.55 -
    1.56 -(* Empty string means create files in Isabelle's temporary files directory. *)
    1.57 -val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
    1.58 -val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
    1.59 -val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
    1.60 -
    1.61 -(* In addition to being easier to read, readable names are often much shorter,
    1.62 -   especially if types are mangled in names. This makes a difference for some
    1.63 -   provers (e.g., E). For these reason, short names are enabled by default. *)
    1.64 -val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
    1.65  
    1.66  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
    1.67  
    1.68 @@ -134,16 +116,6 @@
    1.69  
    1.70  val is_atp = member (op =) o supported_atps
    1.71  
    1.72 -fun is_atp_of_format is_format ctxt name =
    1.73 -  let val thy = Proof_Context.theory_of ctxt in
    1.74 -    (case try (get_atp thy) name of
    1.75 -      SOME config =>
    1.76 -      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
    1.77 -    | NONE => false)
    1.78 -  end
    1.79 -
    1.80 -val is_ho_atp = is_atp_of_format is_format_higher_order
    1.81 -
    1.82  fun remotify_atp_if_supported_and_not_already_remote thy name =
    1.83    if String.isPrefix remote_prefix name then
    1.84      SOME name
    1.85 @@ -156,23 +128,6 @@
    1.86    if is_atp thy name andalso is_atp_installed thy name then SOME name
    1.87    else remotify_atp_if_supported_and_not_already_remote thy name
    1.88  
    1.89 -fun supported_provers ctxt =
    1.90 -  let
    1.91 -    val thy = Proof_Context.theory_of ctxt
    1.92 -    val (remote_provers, local_provers) =
    1.93 -      reconstructor_names @
    1.94 -      sort_strings (supported_atps thy) @
    1.95 -      sort_strings (SMT_Solver.available_solvers_of ctxt)
    1.96 -      |> List.partition (String.isPrefix remote_prefix)
    1.97 -  in
    1.98 -    Output.urgent_message ("Supported provers: " ^
    1.99 -                           commas (local_provers @ remote_provers) ^ ".")
   1.100 -  end
   1.101 -
   1.102 -fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   1.103 -fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   1.104 -val messages = Async_Manager.thread_messages SledgehammerN "prover"
   1.105 -
   1.106  type params =
   1.107    {debug : bool,
   1.108     verbose : bool,
   1.109 @@ -334,45 +289,21 @@
   1.110         (max_new_instances |> the_default best_max_new_instances)
   1.111    #> Config.put Monomorph.max_thm_instances max_fact_instances
   1.112  
   1.113 -fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
   1.114 -    minimize_command
   1.115 -    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   1.116 +fun supported_provers ctxt =
   1.117    let
   1.118 -    val reconstr =
   1.119 -      if name = metisN then
   1.120 -        Metis (type_enc |> the_default (hd partial_type_encs),
   1.121 -               lam_trans |> the_default default_metis_lam_trans)
   1.122 -      else if name = smtN then
   1.123 -        SMT
   1.124 -      else
   1.125 -        raise Fail ("unknown reconstructor: " ^ quote name)
   1.126 -    val used_facts = facts |> map fst
   1.127 +    val thy = Proof_Context.theory_of ctxt
   1.128 +    val (remote_provers, local_provers) =
   1.129 +      reconstructor_names @
   1.130 +      sort_strings (supported_atps thy) @
   1.131 +      sort_strings (SMT_Solver.available_solvers_of ctxt)
   1.132 +      |> List.partition (String.isPrefix remote_prefix)
   1.133    in
   1.134 -    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
   1.135 -       state subgoal reconstr [reconstr] of
   1.136 -      play as (_, Played time) =>
   1.137 -      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
   1.138 -       preplay = Lazy.value play,
   1.139 -       message =
   1.140 -         fn play =>
   1.141 -            let
   1.142 -              val (_, override_params) = extract_reconstructor params reconstr
   1.143 -              val one_line_params =
   1.144 -                (play, proof_banner mode name, used_facts, minimize_command override_params name,
   1.145 -                 subgoal, subgoal_count)
   1.146 -              val num_chained = length (#facts (Proof.goal state))
   1.147 -            in
   1.148 -              one_line_proof_text num_chained one_line_params
   1.149 -            end,
   1.150 -       message_tail = ""}
   1.151 -    | play =>
   1.152 -      let
   1.153 -        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
   1.154 -      in
   1.155 -        {outcome = SOME failure, used_facts = [], used_from = [],
   1.156 -         run_time = Time.zeroTime, preplay = Lazy.value play,
   1.157 -         message = fn _ => string_of_atp_failure failure, message_tail = ""}
   1.158 -      end)
   1.159 +    Output.urgent_message ("Supported provers: " ^
   1.160 +                           commas (local_provers @ remote_provers) ^ ".")
   1.161    end
   1.162  
   1.163 +fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
   1.164 +fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
   1.165 +val messages = Async_Manager.thread_messages SledgehammerN "prover"
   1.166 +
   1.167  end;