# HG changeset patch # User blanchet # Date 1314177453 -7200 # Node ID d9a657c443802a43434ad602b6a30163ade04db7 # Parent 5e19eecb0e1c10d0f2f2318f5ac582dcda4a27ba more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac" diff -r 5e19eecb0e1c -r d9a657c44380 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 11:17:33 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Aug 24 11:17:33 2011 +0200 @@ -569,27 +569,34 @@ fun run_reconstructor trivial full m name reconstructor named_thms id ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) = let - fun do_reconstructor thms ctxt = - (if !reconstructor = "sledgehammer_tac" then - (fn ctxt => fn thms => - Method.insert_tac thms THEN' - (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (e_override_params timeout) - ORELSE' - Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt - (vampire_override_params timeout))) - else if !reconstructor = "smt" then - SMT_Solver.smt_tac - else if full orelse !reconstructor = "metis (full_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] - else if !reconstructor = "metis (no_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] - else if !reconstructor = "metis" then - Metis_Tactics.metis_tac [] - else - K (K (K all_tac))) ctxt thms - fun apply_reconstructor thms = - Mirabelle.can_apply timeout (do_reconstructor thms) st + fun do_reconstructor named_thms ctxt = + let + val ref_of_str = + suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm + #> fst + val thms = named_thms |> maps snd + val facts = named_thms |> map (ref_of_str o fst o fst) + val relevance_override = {add = facts, del = [], only = true} + in + if !reconstructor = "sledgehammer_tac" then + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (e_override_params timeout) relevance_override + ORELSE' + Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt + (vampire_override_params timeout) relevance_override + else if !reconstructor = "smt" then + SMT_Solver.smt_tac ctxt thms + else if full orelse !reconstructor = "metis (full_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms + else if !reconstructor = "metis (no_types)" then + Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms + else if !reconstructor = "metis" then + Metis_Tactics.metis_tac [] ctxt thms + else + K all_tac + end + fun apply_reconstructor named_thms = + Mirabelle.can_apply timeout (do_reconstructor named_thms) st fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")" | with_time (true, t) = (change_data id (inc_reconstructor_success m); @@ -601,8 +608,8 @@ if name = "proof" then change_data id (inc_reconstructor_proofs m) else (); "succeeded (" ^ string_of_int t ^ ")") - fun timed_reconstructor thms = - (with_time (Mirabelle.cpu_time apply_reconstructor thms), true) + fun timed_reconstructor named_thms = + (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true) handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false)) | ERROR msg => ("error: " ^ msg, false) @@ -612,7 +619,7 @@ val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m) in - maps snd named_thms + named_thms |> timed_reconstructor |>> log o prefix (reconstructor_tag reconstructor id) |> snd diff -r 5e19eecb0e1c -r d9a657c44380 src/HOL/TPTP/CASC_Setup.thy --- a/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 11:17:33 2011 +0200 +++ b/src/HOL/TPTP/CASC_Setup.thy Wed Aug 24 11:17:33 2011 +0200 @@ -119,14 +119,16 @@ SOLVE_TIMEOUT (max_secs div 10) "smt" (ALLGOALS (SMT_Solver.smt_tac ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 5) "sledgehammer" - (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) + (ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] + Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "simp" (ALLGOALS (asm_full_simp_tac (simpset_of ctxt))) ORELSE SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt - THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [])) + THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt [] + Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) diff -r 5e19eecb0e1c -r d9a657c44380 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 11:17:33 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 11:17:33 2011 +0200 @@ -38,6 +38,7 @@ val trace : bool Config.T val ignore_no_atp : bool Config.T val instantiate_inducts : bool Config.T + val no_relevance_override : relevance_override val const_names_in_fact : theory -> (string * typ -> term list -> bool * term list) -> term -> string list @@ -100,6 +101,8 @@ del : (Facts.ref * Attrib.src list) list, only : bool} +val no_relevance_override = {add = [], del = [], only = false} + val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator val abs_name = sledgehammer_prefix ^ "abs" val skolem_prefix = sledgehammer_prefix ^ "sko" diff -r 5e19eecb0e1c -r d9a657c44380 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 11:17:33 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 24 11:17:33 2011 +0200 @@ -22,6 +22,7 @@ open ATP_Systems open ATP_Translate open Sledgehammer_Util +open Sledgehammer_Filter open Sledgehammer_Provers open Sledgehammer_Minimize open Sledgehammer_Run @@ -46,7 +47,6 @@ (** Sledgehammer commands **) -val no_relevance_override = {add = [], del = [], only = false} fun add_relevance_override ns : relevance_override = {add = ns, del = [], only = false} fun del_relevance_override ns : relevance_override = diff -r 5e19eecb0e1c -r d9a657c44380 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 11:17:33 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Aug 24 11:17:33 2011 +0200 @@ -7,16 +7,22 @@ signature SLEDGEHAMMER_TACTICS = sig + type relevance_override = Sledgehammer_Filter.relevance_override + val sledgehammer_with_metis_tac : - Proof.context -> (string * string) list -> int -> tactic + Proof.context -> (string * string) list -> relevance_override -> int + -> tactic val sledgehammer_as_oracle_tac : - Proof.context -> (string * string) list -> int -> tactic + Proof.context -> (string * string) list -> relevance_override -> int + -> tactic end; structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = struct -fun run_atp override_params i n ctxt goal = +open Sledgehammer_Filter + +fun run_atp override_params relevance_override i n ctxt goal = let val chained_ths = [] (* a tactic has no chained ths *) val params as {provers, relevance_thresholds, max_relevant, slicing, ...} = @@ -30,7 +36,6 @@ Sledgehammer_Provers.is_built_in_const_for_prover ctxt name val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name - val relevance_override = {add = [], del = [], only = false} val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val facts = Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths @@ -62,16 +67,17 @@ |> Source.exhaust end -fun sledgehammer_with_metis_tac ctxt override_params i th = - case run_atp override_params i i ctxt th of +fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = + case run_atp override_params relevance_override i i ctxt th of SOME facts => Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty -fun sledgehammer_as_oracle_tac ctxt override_params i th = +fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = let val thy = Proof_Context.theory_of ctxt - val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th + val xs = run_atp (override_params @ [("sound", "true")]) relevance_override + i i ctxt th in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end end;