--- a/src/HOL/IsaMakefile Tue Dec 21 09:16:03 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Dec 21 10:25:17 2010 +0100
@@ -1314,7 +1314,7 @@
Mirabelle/Tools/mirabelle_quickcheck.ML \
Mirabelle/Tools/mirabelle_refute.ML \
Mirabelle/Tools/mirabelle_sledgehammer.ML \
- Mirabelle/Tools/sledgehammer_tactic.ML
+ Mirabelle/Tools/sledgehammer_tactics.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 09:16:03 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle.thy Tue Dec 21 10:25:17 2010 +0100
@@ -3,8 +3,9 @@
*)
theory Mirabelle
-imports Pure
+imports Sledgehammer
uses "Tools/mirabelle.ML"
+ "Tools/sledgehammer_tactics.ML"
begin
(* no multithreading, no parallel proofs *) (* FIXME *)
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 09:16:03 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Tue Dec 21 10:25:17 2010 +0100
@@ -13,7 +13,6 @@
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
"Tools/mirabelle_sledgehammer_filter.ML"
- "Tools/sledgehammer_tactic.ML"
begin
text {*
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 09:16:03 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Dec 21 10:25:17 2010 +0100
@@ -13,6 +13,7 @@
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
val metis_ftK = "metis_ft"
+val reconstructorK = "reconstructor"
fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -331,10 +332,13 @@
type locality = Sledgehammer_Filter.locality
(* hack *)
-fun reconstructor_from_msg msg =
- if String.isSubstring "metisFT" msg then "metisFT"
- else if String.isSubstring "metis" msg then "metis"
- else "smt"
+fun reconstructor_from_msg args msg =
+ (case AList.lookup (op =) args reconstructorK of
+ SOME name => name
+ | NONE =>
+ if String.isSubstring "metisFT" msg then "metisFT"
+ else if String.isSubstring "metis" msg then "metis"
+ else "smt")
local
@@ -445,7 +449,7 @@
change_data id (inc_sh_max_lems (length names));
change_data id (inc_sh_time_isa time_isa);
change_data id (inc_sh_time_prover time_prover);
- reconstructor := reconstructor_from_msg msg;
+ reconstructor := reconstructor_from_msg args msg;
named_thms := SOME (map_filter get_thms names);
log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -487,7 +491,7 @@
change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
if length named_thms' = n0
then log (minimize_tag id ^ "already minimal")
- else (reconstructor := reconstructor_from_msg msg;
+ else (reconstructor := reconstructor_from_msg args msg;
named_thms := SOME named_thms';
log (minimize_tag id ^ "succeeded:\n" ^ msg))
)
@@ -499,7 +503,11 @@
({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
let
fun do_reconstructor thms ctxt =
- (if !reconstructor = "smt" then
+ (if !reconstructor = "sledgehammer_tac" then
+ (fn ctxt => fn thms =>
+ Method.insert_tac thms THEN'
+ Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+ else if !reconstructor = "smt" then
SMT_Solver.smt_tac
else if full orelse !reconstructor = "metisFT" then
Metis_Tactics.metisFT_tac
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Tue Dec 21 09:16:03 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(* Title: sledgehammer_tactics.ML
- Author: Jasmin Blanchette, TU Muenchen
- Copyright 2010
-
-Sledgehammer as a tactic.
-*)
-
-signature SLEDGEHAMMER_TACTICS =
-sig
- val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
- val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
-end;
-
-structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
-struct
-
-fun run_atp force_full_types timeout i n ctxt goal name =
- let
- val chained_ths = [] (* a tactic has no chained ths *)
- val params as {type_sys, relevance_thresholds, max_relevant, ...} =
- ((if force_full_types then [("full_types", "true")] else [])
- @ [("timeout", Int.toString (Time.toSeconds timeout))])
- @ [("overlord", "true")]
- |> Sledgehammer_Isar.default_params ctxt
- val prover = Sledgehammer_Provers.get_prover ctxt false name
- val default_max_relevant =
- Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
- val is_built_in_const =
- 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) = Sledgehammer_Util.strip_subgoal goal i
- val no_dangerous_types =
- Sledgehammer_ATP_Translate.types_dangerous_types type_sys
- val facts =
- Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
- relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
- (* Check for constants other than the built-in HOL constants. If none of
- them appear (as should be the case for TPTP problems, unless "auto" or
- "simp" already did its "magic"), we can skip the relevance filter. *)
- val pure_goal =
- not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
- not (String.isSubstring "HOL" s))
- (prop_of goal))
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = map Sledgehammer_Provers.Untranslated_Fact facts,
- smt_head = NONE}
- in
- (case prover params (K "") problem of
- {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
- | _ => NONE)
- handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
- end
-
-fun to_period ("." :: _) = []
- | to_period ("" :: ss) = to_period ss
- | to_period (s :: ss) = s :: to_period ss
- | to_period [] = []
-
-val atp = "e" (* or "vampire" *)
-
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (ProofContext.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover=SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-fun sledgehammer_with_metis_tac ctxt i th =
- let
- val timeout = Time.fromSeconds 30
- in
- case run_atp false timeout i i ctxt th atp of
- SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
- | NONE => Seq.empty
- end
-
-fun sledgehammer_as_oracle_tac ctxt i th =
- let
- val thy = ProofContext.theory_of ctxt
- val timeout = Time.fromSeconds 30
- val xs = run_atp true timeout i i ctxt th atp
- in
- if is_some xs then Skip_Proof.cheat_tac thy th
- else Seq.empty
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactics.ML Tue Dec 21 10:25:17 2010 +0100
@@ -0,0 +1,101 @@
+(* Title: sledgehammer_tactics.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2010
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+ val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
+ val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+
+fun run_atp force_full_types timeout i n ctxt goal name =
+ let
+ val chained_ths = [] (* a tactic has no chained ths *)
+ val params as {type_sys, relevance_thresholds, max_relevant, ...} =
+ ((if force_full_types then [("full_types", "true")] else [])
+ @ [("timeout", Int.toString (Time.toSeconds timeout))])
+ (* @ [("overlord", "true")] *)
+ |> Sledgehammer_Isar.default_params ctxt
+ val prover = Sledgehammer_Provers.get_prover ctxt false name
+ val default_max_relevant =
+ Sledgehammer_Provers.default_max_relevant_for_prover ctxt name
+ val is_built_in_const =
+ 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) = Sledgehammer_Util.strip_subgoal goal i
+ val no_dangerous_types =
+ Sledgehammer_ATP_Translate.types_dangerous_types type_sys
+ val facts =
+ Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
+ relevance_thresholds
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ (* Check for constants other than the built-in HOL constants. If none of
+ them appear (as should be the case for TPTP problems, unless "auto" or
+ "simp" already did its "magic"), we can skip the relevance filter. *)
+ val pure_goal =
+ not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
+ not (String.isSubstring "HOL" s))
+ (prop_of goal))
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ facts = map Sledgehammer_Provers.Untranslated_Fact facts,
+ smt_head = NONE}
+ in
+ (case prover params (K "") problem of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
+ | _ => NONE)
+ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)
+ end
+
+fun to_period ("." :: _) = []
+ | to_period ("" :: ss) = to_period ss
+ | to_period (s :: ss) = s :: to_period ss
+ | to_period [] = []
+
+val atp = "vampire" (* or "e" or "spass" etc. *)
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (ProofContext.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover=SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+fun sledgehammer_with_metis_tac ctxt i th =
+ let
+ val timeout = Time.fromSeconds 30
+ in
+ case run_atp false timeout i i ctxt th atp of
+ SOME facts =>
+ Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+ | NONE => Seq.empty
+ end
+
+fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val timeout = Time.fromSeconds 30
+ val xs = run_atp force_full_types timeout i i ctxt th atp
+ in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+
+val sledgehammer_as_unsound_oracle_tac =
+ generic_sledgehammer_as_oracle_tac false
+val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
+
+end;