1(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML 2 Author: Fabian Immler, TU Muenchen 3 Author: Makarius 4 Author: Jasmin Blanchette, TU Muenchen 5 6Sledgehammer's heart. 7*) 8 9signature SLEDGEHAMMER = 10sig 11 type stature = ATP_Problem_Generate.stature 12 type fact = Sledgehammer_Fact.fact 13 type fact_override = Sledgehammer_Fact.fact_override 14 type proof_method = Sledgehammer_Proof_Methods.proof_method 15 type play_outcome = Sledgehammer_Proof_Methods.play_outcome 16 type mode = Sledgehammer_Prover.mode 17 type params = Sledgehammer_Prover.params 18 19 val someN : string 20 val noneN : string 21 val timeoutN : string 22 val unknownN : string 23 24 val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> 25 proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) 26 val string_of_factss : (string * fact list) list -> string 27 val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> 28 Proof.state -> bool * (string * string list) 29end; 30 31structure Sledgehammer : SLEDGEHAMMER = 32struct 33 34open ATP_Util 35open ATP_Proof 36open ATP_Problem_Generate 37open Sledgehammer_Util 38open Sledgehammer_Fact 39open Sledgehammer_Proof_Methods 40open Sledgehammer_Isar_Proof 41open Sledgehammer_Isar_Preplay 42open Sledgehammer_Isar_Minimize 43open Sledgehammer_Prover 44open Sledgehammer_Prover_ATP 45open Sledgehammer_Prover_Minimize 46open Sledgehammer_MaSh 47 48val someN = "some" 49val noneN = "none" 50val timeoutN = "timeout" 51val unknownN = "unknown" 52 53val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] 54 55fun max_outcome_code codes = 56 NONE 57 |> fold (fn candidate => 58 fn accum as SOME _ => accum 59 | NONE => if member (op =) codes candidate then SOME candidate else NONE) 60 ordered_outcome_codes 61 |> the_default unknownN 62 63fun is_metis_method (Metis_Method _) = true 64 | is_metis_method _ = false 65 66fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = 67 (if timeout = Time.zeroTime then 68 (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) 69 else 70 let 71 val ctxt = Proof.context_of state 72 73 val fact_names = map fst used_facts 74 val {facts = chained, goal, ...} = Proof.goal state 75 val goal_t = Logic.get_goal (Thm.prop_of goal) i 76 77 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) 78 | try_methss ress [] = 79 (used_facts, 80 (case AList.lookup (op =) ress preferred_meth of 81 SOME play => (preferred_meth, play) 82 | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) 83 | try_methss ress (meths :: methss) = 84 let 85 fun mk_step fact_names meths = 86 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") 87 in 88 (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of 89 (res as (meth, Played time)) :: _ => 90 (* if a fact is needed by an ATP, it will be needed by "metis" *) 91 if not minimize orelse is_metis_method meth then 92 (used_facts, res) 93 else 94 let 95 val (time', used_names') = 96 minimized_isar_step ctxt chained time (mk_step fact_names [meth]) 97 ||> (facts_of_isar_step #> snd) 98 val used_facts' = filter (member (op =) used_names' o fst) used_facts 99 in 100 (used_facts', (meth, Played time')) 101 end 102 | ress' => try_methss (ress' @ ress) methss) 103 end 104 in 105 try_methss [] methss 106 end) 107 |> (fn (used_facts, (meth, play)) => 108 (used_facts |> not (proof_method_distinguishes_chained_and_direct meth) 109 ? filter_out (fn (_, (sc, _)) => sc = Chained), 110 (meth, play))) 111 112fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout, 113 expect, ...}) mode writeln_result only learn 114 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name = 115 let 116 val ctxt = Proof.context_of state 117 118 val hard_timeout = time_mult 5.0 timeout 119 val _ = spying spy (fn () => (state, subgoal, name, "Launched")); 120 val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name) 121 val num_facts = length facts |> not only ? Integer.min max_facts 122 123 val problem = 124 {comment = comment, state = state, goal = goal, subgoal = subgoal, 125 subgoal_count = subgoal_count, 126 factss = factss 127 |> map (apsnd ((not (is_ho_atp ctxt name) 128 ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false)) 129 #> take num_facts)), 130 found_proof = found_proof} 131 132 fun print_used_facts used_facts used_from = 133 tag_list 1 used_from 134 |> map (fn (j, fact) => fact |> apsnd (K j)) 135 |> filter_used_facts false used_facts 136 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) 137 |> commas 138 |> prefix ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ 139 " proof (of " ^ string_of_int (length facts) ^ "): ") 140 |> writeln 141 142 fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = 143 let 144 val num_used_facts = length used_facts 145 146 fun find_indices facts = 147 tag_list 1 facts 148 |> map (fn (j, fact) => fact |> apsnd (K j)) 149 |> filter_used_facts false used_facts 150 |> distinct (eq_fst (op =)) 151 |> map (prefix "@" o string_of_int o snd) 152 153 fun filter_info (fact_filter, facts) = 154 let 155 val indices = find_indices facts 156 (* "Int.max" is there for robustness -- it shouldn't be necessary *) 157 val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" 158 in 159 (commas (indices @ unknowns), fact_filter) 160 end 161 162 val filter_infos = 163 map filter_info (("actual", used_from) :: factss) 164 |> AList.group (op =) 165 |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) 166 in 167 "Success: Found proof with " ^ string_of_int num_used_facts ^ " of " ^ 168 string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ 169 (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) 170 end 171 | spying_str_of_res {outcome = SOME failure, ...} = 172 "Failure: " ^ string_of_atp_failure failure 173 174 fun really_go () = 175 problem 176 |> get_minimizing_prover ctxt mode learn name params 177 |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => 178 print_used_facts used_facts used_from 179 | _ => ()) 180 |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) 181 |> (fn {outcome, used_facts, preferred_methss, message, ...} => 182 (if outcome = SOME ATP_Proof.TimedOut then timeoutN 183 else if is_some outcome then noneN 184 else someN, 185 fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state 186 subgoal preferred_methss))) 187 188 fun go () = 189 let 190 val (outcome_code, message) = 191 if debug then 192 really_go () 193 else 194 (really_go () 195 handle 196 ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n") 197 | exn => 198 if Exn.is_interrupt exn then Exn.reraise exn 199 else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) 200 201 val _ = 202 (* The "expect" argument is deliberately ignored if the prover is 203 missing so that the "Metis_Examples" can be processed on any 204 machine. *) 205 if expect = "" orelse outcome_code = expect orelse 206 not (is_prover_installed ctxt name) then 207 () 208 else 209 error ("Unexpected outcome: " ^ quote outcome_code) 210 in (outcome_code, message) end 211 in 212 if mode = Auto_Try then 213 let val (outcome_code, message) = Timeout.apply timeout go () in 214 (outcome_code, if outcome_code = someN then [message ()] else []) 215 end 216 else 217 let 218 val (outcome_code, message) = Timeout.apply hard_timeout go () 219 val outcome = 220 if outcome_code = someN orelse mode = Normal then quote name ^ ": " ^ message () else "" 221 val _ = 222 if outcome <> "" andalso is_some writeln_result then the writeln_result outcome 223 else writeln outcome 224 in (outcome_code, []) end 225 end 226 227val auto_try_max_facts_divisor = 2 (* FUDGE *) 228 229fun string_of_facts facts = 230 "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ": " ^ 231 (facts |> map (fst o fst) |> space_implode " ") 232 233fun string_of_factss factss = 234 if forall (null o snd) factss then 235 "Found no relevant facts" 236 else 237 cat_lines (map (fn (filter, facts) => 238 (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) 239 240fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i 241 (fact_override as {only, ...}) state = 242 if null provers then 243 error "No prover is set" 244 else 245 (case subgoal_count state of 246 0 => (error "No subgoal!"; (false, (noneN, []))) 247 | n => 248 let 249 val _ = Proof.assert_backward state 250 val print = if mode = Normal andalso is_none writeln_result then writeln else K () 251 252 val found_proof = 253 if mode = Normal then 254 let val proof_found = Synchronized.var "proof_found" false in 255 fn () => 256 if Synchronized.change_result proof_found (rpair true) then () 257 else (writeln_result |> the_default writeln) "Proof found..." 258 end 259 else 260 I 261 262 val ctxt = Proof.context_of state 263 val keywords = Thy_Header.get_keywords' ctxt 264 val {facts = chained, goal, ...} = Proof.goal state 265 val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt 266 val ho_atp = exists (is_ho_atp ctxt) provers 267 val css = clasimpset_rule_table_of ctxt 268 val all_facts = 269 nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t 270 val _ = 271 (case find_first (not o is_prover_supported ctxt) provers of 272 SOME name => error ("No such prover: " ^ name) 273 | NONE => ()) 274 val _ = print "Sledgehammering..." 275 val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) 276 277 val spying_str_of_factss = 278 commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) 279 280 fun get_factss provers = 281 let 282 val max_max_facts = 283 (case max_facts of 284 SOME n => n 285 | NONE => 286 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers 287 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)) 288 val _ = spying spy (fn () => (state, i, "All", 289 "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^ 290 str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); 291 in 292 all_facts 293 |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t 294 |> tap (fn factss => if verbose then print (string_of_factss factss) else ()) 295 |> spy ? tap (fn factss => spying spy (fn () => 296 (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss))) 297 end 298 299 fun launch_provers () = 300 let 301 val factss = get_factss provers 302 val problem = 303 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, 304 factss = factss, found_proof = found_proof} 305 val learn = mash_learn_proof ctxt params (Thm.prop_of goal) 306 val launch = launch_prover params mode writeln_result only learn 307 in 308 if mode = Auto_Try then 309 (unknownN, []) 310 |> fold (fn prover => fn accum as (outcome_code, _) => 311 if outcome_code = someN then accum else launch problem prover) 312 provers 313 else 314 (learn chained; 315 provers 316 |> Par_List.map (launch problem #> fst) 317 |> max_outcome_code |> rpair []) 318 end 319 in 320 launch_provers () 321 handle Timeout.TIMEOUT _ => 322 (print "Sledgehammer ran out of time"; (unknownN, [])) 323 end 324 |> `(fn (outcome_code, _) => outcome_code = someN)) 325 326end; 327