1(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_prover.ML
2    Author:     Fabian Immler, TU Muenchen
3    Author:     Makarius
4    Author:     Jasmin Blanchette, TU Muenchen
5
6Generic prover abstraction for Sledgehammer.
7*)
8
9signature SLEDGEHAMMER_PROVER =
10sig
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
18  datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
19
20  type params =
21    {debug : bool,
22     verbose : bool,
23     overlord : bool,
24     spy : bool,
25     provers : string list,
26     type_enc : string option,
27     strict : bool,
28     lam_trans : string option,
29     uncurried_aliases : bool option,
30     learn : bool,
31     fact_filter : string option,
32     max_facts : int option,
33     fact_thresholds : real * real,
34     max_mono_iters : int option,
35     max_new_mono_instances : int option,
36     isar_proofs : bool option,
37     compress : real option,
38     try0 : bool,
39     smt_proofs : bool option,
40     slice : bool,
41     minimize : bool,
42     timeout : Time.time,
43     preplay_timeout : Time.time,
44     expect : string}
45
46  type prover_problem =
47    {comment : string,
48     state : Proof.state,
49     goal : thm,
50     subgoal : int,
51     subgoal_count : int,
52     factss : (string * fact list) list,
53     found_proof : unit -> unit}
54
55  type prover_result =
56    {outcome : atp_failure option,
57     used_facts : (string * stature) list,
58     used_from : fact list,
59     preferred_methss : proof_method * proof_method list list,
60     run_time : Time.time,
61     message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
62
63  type prover = params -> prover_problem -> prover_result
64
65  val SledgehammerN : string
66  val str_of_mode : mode -> string
67  val overlord_file_location_of_prover : string -> string * string
68  val proof_banner : mode -> string -> string
69  val is_atp : theory -> string -> bool
70  val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list
71  val is_fact_chained : (('a * stature) * 'b) -> bool
72  val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
73    ((''a * stature) * 'b) list
74  val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
75    Proof.context
76  val supported_provers : Proof.context -> unit
77end;
78
79structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
80struct
81
82open ATP_Proof
83open ATP_Util
84open ATP_Systems
85open ATP_Problem
86open ATP_Problem_Generate
87open ATP_Proof_Reconstruct
88open Metis_Tactic
89open Sledgehammer_Fact
90open Sledgehammer_Proof_Methods
91
92(* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *)
93val SledgehammerN = "Sledgehammer"
94
95datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
96
97fun str_of_mode Auto_Try = "Auto Try"
98  | str_of_mode Try = "Try"
99  | str_of_mode Normal = "Normal"
100  | str_of_mode Minimize = "Minimize"
101  | str_of_mode MaSh = "MaSh"
102
103val is_atp = member (op =) o supported_atps
104
105type params =
106  {debug : bool,
107   verbose : bool,
108   overlord : bool,
109   spy : bool,
110   provers : string list,
111   type_enc : string option,
112   strict : bool,
113   lam_trans : string option,
114   uncurried_aliases : bool option,
115   learn : bool,
116   fact_filter : string option,
117   max_facts : int option,
118   fact_thresholds : real * real,
119   max_mono_iters : int option,
120   max_new_mono_instances : int option,
121   isar_proofs : bool option,
122   compress : real option,
123   try0 : bool,
124   smt_proofs : bool option,
125   slice : bool,
126   minimize : bool,
127   timeout : Time.time,
128   preplay_timeout : Time.time,
129   expect : string}
130
131type prover_problem =
132  {comment : string,
133   state : Proof.state,
134   goal : thm,
135   subgoal : int,
136   subgoal_count : int,
137   factss : (string * fact list) list,
138   found_proof : unit -> unit}
139
140type prover_result =
141  {outcome : atp_failure option,
142   used_facts : (string * stature) list,
143   used_from : fact list,
144   preferred_methss : proof_method * proof_method list list,
145   run_time : Time.time,
146   message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
147
148type prover = params -> prover_problem -> prover_result
149
150fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
151
152fun proof_banner mode name =
153  (case mode of
154    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
155  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
156  | _ => "Try this")
157
158fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans =
159  (if try0 then
160    [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
161     [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
162   else
163     []) @
164  [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)],
165   (if needs_full_types then
166      [Metis_Method (NONE, NONE),
167       Metis_Method (SOME really_full_type_enc, NONE),
168       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
169       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
170    else
171      [Metis_Method (SOME full_typesN, NONE),
172       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
173       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @
174  (if smt_method then [[SMT_Method]] else [])
175
176fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
177
178fun filter_used_facts keep_chained used =
179  filter ((member (eq_fst (op =)) used o fst) orf
180    (if keep_chained then is_fact_chained else K false))
181
182val max_fact_instances = 10 (* FUDGE *)
183
184fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances =
185  Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters)
186  #> Config.put Monomorph.max_new_instances
187       (max_new_instances |> the_default best_max_new_instances)
188  #> Config.put Monomorph.max_thm_instances max_fact_instances
189
190fun supported_provers ctxt =
191  let
192    val thy = Proof_Context.theory_of ctxt
193    val (remote_provers, local_provers) =
194      sort_strings (supported_atps thy) @ sort_strings (SMT_Config.available_solvers_of ctxt)
195      |> List.partition (String.isPrefix remote_prefix)
196  in
197    writeln ("Supported provers: " ^ commas (local_provers @ remote_provers))
198  end
199
200end;
201