65 val SledgehammerN : string |
65 val SledgehammerN : string |
66 val str_of_mode : mode -> string |
66 val str_of_mode : mode -> string |
67 val overlord_file_location_of_prover : string -> string * string |
67 val overlord_file_location_of_prover : string -> string * string |
68 val proof_banner : mode -> string -> string |
68 val proof_banner : mode -> string -> string |
69 val is_atp : theory -> string -> bool |
69 val is_atp : theory -> string -> bool |
70 val bunches_of_proof_methods : bool -> bool -> bool -> string -> proof_method list list |
70 val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string -> |
|
71 proof_method list list |
71 val is_fact_chained : (('a * stature) * 'b) -> bool |
72 val is_fact_chained : (('a * stature) * 'b) -> bool |
72 val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> |
73 val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> |
73 ((''a * stature) * 'b) list |
74 ((''a * stature) * 'b) list |
74 val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> |
75 val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> |
75 Proof.context |
76 Proof.context |
153 (case mode of |
154 (case mode of |
154 Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" |
155 Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" |
155 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
156 | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" |
156 | _ => "Try this") |
157 | _ => "Try this") |
157 |
158 |
158 fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans = |
159 fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = |
159 (if try0 then |
160 let |
160 [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method], |
161 val try0_methodss = |
161 [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]] |
162 if try0 then |
162 else |
163 [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, |
163 []) @ |
164 Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] |
164 [[Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE)], |
165 else |
165 (if needs_full_types then |
166 [] |
166 [Metis_Method (NONE, NONE), |
167 |
167 Metis_Method (SOME really_full_type_enc, NONE), |
168 val metis_methods = |
168 Metis_Method (SOME full_typesN, SOME desperate_lam_trans), |
169 (if try0 then [] else [Metis_Method (NONE, NONE)]) @ |
169 Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] |
170 Metis_Method (SOME full_typesN, NONE) :: |
170 else |
171 Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: |
171 [Metis_Method (SOME full_typesN, NONE), |
172 (if needs_full_types then |
172 Metis_Method (SOME no_typesN, SOME desperate_lam_trans), |
173 [Metis_Method (SOME really_full_type_enc, NONE), |
173 Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @ |
174 Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] |
174 (if smt_proofs then [[SMT_Method]] else []) |
175 else |
|
176 [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) |
|
177 |
|
178 val smt_methodss = |
|
179 if smt_proofs then |
|
180 [SMT_Method SMT_Default :: |
|
181 map (fn strategy => SMT_Method (SMT_Verit strategy)) |
|
182 (Verit_Proof.all_veriT_stgies (Context.Proof ctxt))] |
|
183 else |
|
184 [] |
|
185 in |
|
186 try0_methodss @ [metis_methods] @ smt_methodss |
|
187 end |
175 |
188 |
176 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained |
189 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained |
177 |
190 |
178 fun filter_used_facts keep_chained used = |
191 fun filter_used_facts keep_chained used = |
179 filter ((member (eq_fst (op =)) used o fst) orf |
192 filter ((member (eq_fst (op =)) used o fst) orf |