# HG changeset patch # User desharna # Date 1642775880 -3600 # Node ID d4a52993a81e56a20b5437d5b1ad32fb49620c07 # Parent 1f4c39ffb116c3d9861012772db7f89d49f5074d removed unsynchronized references in mirabelle_sledgehammer diff -r 1f4c39ffb116 -r d4a52993a81e src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Jan 21 15:29:36 2022 +0100 +++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Jan 21 15:38:00 2022 +0100 @@ -311,8 +311,7 @@ in fun run_sledgehammer (params as {provers, ...}) output_dir e_selection_heuristic term_order - force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial proof_method named_thms - pos st = + force_sos keep_probs keep_proofs proof_method_from_msg thy_index trivial pos st = let val thy = Proof.theory_of st val thy_name = Context.theory_name thy @@ -330,7 +329,7 @@ val prover_name = hd provers val (sledgehamer_outcome, msg, cpu_time) = run_sh params e_selection_heuristic term_order force_sos keep pos st - val (outcome_msg, change_data) = + val (outcome_msg, change_data, proof_method_and_used_thms) = (case sledgehamer_outcome of Sledgehammer.SH_Some {used_facts, run_time, ...} => let @@ -350,13 +349,13 @@ #> inc_sh_max_lems num_used_facts #> inc_sh_time_prover time_prover in - proof_method := proof_method_from_msg msg; - named_thms := SOME (map_filter get_thms used_facts); - (outcome_msg, change_data) + (outcome_msg, change_data, + SOME (proof_method_from_msg msg, map_filter get_thms used_facts)) end - | _ => ("", I)) + | _ => ("", I, NONE)) in - (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time) + (sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time, + proof_method_and_used_thms) end end @@ -385,35 +384,35 @@ Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt (override_params prover type_enc (my_timeout time_slice)) fact_override [] in - if !meth = "sledgehammer_tac" then + if meth = "sledgehammer_tac" then sledge_tac 0.2 ATP_Proof.vampireN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??" ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native" ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??" ORELSE' SMT_Solver.smt_tac ctxt thms - else if !meth = "smt" then + else if meth = "smt" then SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if String.isPrefix "metis (" (!meth) then + else if String.isPrefix "metis (" meth then let val (type_encs, lam_trans) = - !meth + meth |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end - else if !meth = "metis" then + else if meth = "metis" then Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms - else if !meth = "none" then + else if meth = "none" then K all_tac - else if !meth = "fail" then + else if meth = "fail" then K no_tac else - (warning ("Unknown method " ^ quote (!meth)); K no_tac) + (warning ("Unknown method " ^ quote meth); K no_tac) end fun apply_method named_thms = Mirabelle.can_apply timeout (do_method named_thms) st @@ -470,21 +469,17 @@ "" else let - val meth = Unsynchronized.ref "" - val named_thms = - Unsynchronized.ref (NONE : ((string * stature) * thm list) list option) val trivial = check_trivial andalso Try0.try0 (SOME try_timeout) ([], [], [], []) pre handle Timeout.TIMEOUT _ => false - val (outcome, log1, change_data1) = + val (outcome, log1, change_data1, proof_method_and_used_thms) = run_sledgehammer params output_dir e_selection_heuristic term_order - force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial meth - named_thms pos pre + force_sos keep_probs keep_proofs proof_method_from_msg theory_index trivial pos pre val (log2, change_data2) = - (case !named_thms of - SOME thms => - run_proof_method trivial false name meth thms timeout pos pre - |> apfst (prefix (!meth ^ " (sledgehammer): ")) + (case proof_method_and_used_thms of + SOME (proof_method, used_thms) => + run_proof_method trivial false name proof_method used_thms timeout pos pre + |> apfst (prefix (proof_method ^ " (sledgehammer): ")) | NONE => ("", I)) val () = Synchronized.change data (change_data1 #> change_data2 #> inc_sh_calls #> not trivial ? inc_sh_nontriv_calls)