--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 14:12:55 2011 +0200
@@ -416,11 +416,12 @@
let
val _ = if is_appropriate_prop concl_t then ()
else raise Fail "inappropriate"
+ val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
- chained_ths hyp_ts concl_t
+ Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp
+ relevance_override chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
(the_default default_max_relevant max_relevant)
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200
@@ -129,11 +129,12 @@
val relevance_override = {add = [], del = [], only = false}
val subgoal = 1
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
+ val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt relevance_override
+ Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
chained_ths hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
(the_default default_max_relevant max_relevant)
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
--- a/src/HOL/TPTP/atp_export.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML Tue Aug 30 14:12:55 2011 +0200
@@ -27,8 +27,9 @@
val fact_name_of = prefix fact_prefix o ascii_of
fun facts_of thy =
- Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
- true [] []
+ Sledgehammer_Filter.all_facts (Proof_Context.init_global thy)
+ false(*FIXME works only for first-order*)
+ Symtab.empty true [] []
|> filter (curry (op =) @{typ bool} o fastype_of
o Object_Logic.atomize_term thy o prop_of o snd)
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200
@@ -55,7 +55,6 @@
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
val is_atp_installed : theory -> string -> bool
- val is_ho_atp: string -> bool
val refresh_systems_on_tptp : unit -> unit
val setup : theory -> theory
end;
@@ -500,15 +499,6 @@
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
end
-fun is_ho_atp name =
- let
- val local_ho_atps = [leo2N, satallaxN]
- val ho_atps = map (fn n => remote_prefix ^ n) local_ho_atps
- in List.filter (fn n => n = name) ho_atps
- |> List.null
- |> not
- end
-
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
--- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 14:12:55 2011 +0200
@@ -892,9 +892,6 @@
else
IConst (proxy_base |>> prefix const_prefix, T, T_args)
| NONE => if s = tptp_choice then
- (*this could be made neater by adding c_Eps as a proxy,
- but we'd need to be able to "see" Hilbert_Choice.Eps
- at this level in order to define fEps*)
tweak_ho_quant tptp_choice T args
else IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200
@@ -837,8 +837,8 @@
val is_chained = member Thm.eq_thm_prop chained_ths
val clasimpset_table = clasimpset_rule_table_of ctxt
fun locality_of_theorem global (name: string) th =
- if (String.isSubstring ".induct" name) orelse(*FIXME: use structured name*)
- (String.isSubstring ".inducts" name) then
+ if String.isSubstring ".induct" name orelse(*FIXME: use structured name*)
+ String.isSubstring ".inducts" name then
Induction
else if is_chained th then
Chained
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 14:12:55 2011 +0200
@@ -83,6 +83,7 @@
val is_metis_prover : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
+ val is_ho_atp: Proof.context -> string -> bool
val is_unit_equational_atp : Proof.context -> string -> bool
val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
@@ -91,7 +92,6 @@
val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
val is_built_in_const_for_prover :
Proof.context -> string -> string * typ -> term list -> bool * term list
- val is_induction_fact: prover_fact -> bool
val atp_relevance_fudge : relevance_fudge
val smt_relevance_fudge : relevance_fudge
val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
@@ -152,6 +152,19 @@
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
+fun is_ho_atp ctxt name =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in case try (get_atp thy) name of
+ SOME {best_slices, ...} =>
+ exists (fn cfg => case cfg of
+ (_, (_, (_, THF _, _, _))) => true
+ | _ => false
+ )
+ (best_slices ctxt)
+ | NONE => false
+ end
+
fun is_unit_equational_atp ctxt name =
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
@@ -330,11 +343,6 @@
type prover =
params -> (string -> minimize_command) -> prover_problem -> prover_result
-(* checking facts' locality *)
-
-fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
- | is_induction_fact _ = false
-
(* configuration attributes *)
(* Empty string means create files in Isabelle's temporary files directory. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200
@@ -144,6 +144,9 @@
get_prover ctxt mode name params minimize_command problem
|> minimize ctxt mode name params problem
+fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
+ | is_induction_fact _ = false
+
fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
timeout, expect, ...})
mode minimize_command only
@@ -161,12 +164,11 @@
prover_description ctxt params name num_facts subgoal subgoal_count goal
val problem =
let
- val filter_induction =
- List.filter (fn fact =>
- not (Sledgehammer_Provers.is_induction_fact fact))
+ val filter_induction = filter_out is_induction_fact
in {state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts =
- ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts
+ ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
+ facts
|> take num_facts,
smt_filter = smt_filter}
end
@@ -267,12 +269,10 @@
val {facts = chained_ths, goal, ...} = Proof.goal state
val chained_ths = chained_ths |> normalize_chained_theorems
val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i
- val targetting_ho_provers =
- List.foldr (fn (name, so_far) => (ATP_Systems.is_ho_atp name) orelse
- so_far)
- false provers
- val facts = nearly_all_facts ctxt targetting_ho_provers relevance_override
- chained_ths hyp_ts concl_t val _ = () |> not blocking ? kill_provers
+ val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers
+ val facts = nearly_all_facts ctxt is_ho_atp relevance_override
+ chained_ths hyp_ts concl_t
+ val _ = () |> not blocking ? kill_provers
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
@@ -323,7 +323,7 @@
|> (case is_appropriate_prop of
SOME is_app => filter (is_app o prop_of o snd)
| NONE => I)
- |> relevant_facts ctxt targetting_ho_provers relevance_thresholds
+ |> relevant_facts ctxt is_ho_atp relevance_thresholds
max_max_relevant is_built_in_const relevance_fudge
relevance_override chained_ths hyp_ts concl_t
|> tap (fn facts =>
--- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 14:12:55 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 14:12:55 2011 +0200
@@ -37,10 +37,13 @@
val relevance_fudge =
Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val is_ho_atp =
+ exists (Sledgehammer_Provers.is_ho_atp ctxt)
+ provers(*FIXME: duplicated from sledgehammer_run.ML*)
val facts =
- Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths
- hyp_ts concl_t
- |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override
+ chained_ths hyp_ts concl_t
+ |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds
(the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =