--- 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
--- 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 []))
--- 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"
--- 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 =
--- 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;