--- a/NEWS Tue Feb 08 16:10:09 2011 +0100
+++ b/NEWS Tue Feb 08 16:10:10 2011 +0100
@@ -11,6 +11,13 @@
usedir option -Q.
+*** HOL ***
+
+* Sledgehammer:
+ sledgehammer available_provers ~> sledgehammer supported_provers
+ INCOMPATIBILITY.
+
+
*** Document preparation ***
* New term style "isub" as ad-hoc conversion of variables x1, y23 into
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 16:10:09 2011 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Feb 08 16:10:10 2011 +0100
@@ -303,7 +303,7 @@
due to Sledgehammer's asynchronous nature. The \textit{num} argument specifies a
limit on the number of messages to display (5 by default).
-\item[$\bullet$] \textbf{\textit{available\_provers}:} Prints the list of
+\item[$\bullet$] \textbf{\textit{supported\_provers}:} Prints the list of
automatic provers supported by Sledgehammer. See \S\ref{installation} and
\S\ref{mode-of-operation} for more information on how to install automatic
provers.
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 16:10:09 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Feb 08 16:10:10 2011 +0100
@@ -39,7 +39,7 @@
val remote_prefix : string
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
- val available_atps : theory -> string list
+ val supported_atps : theory -> string list
val is_atp_installed : theory -> string -> bool
val refresh_systems_on_tptp : unit -> unit
val setup : theory -> theory
@@ -307,7 +307,7 @@
the (Symtab.lookup (Data.get thy) name) |> fst
handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-val available_atps = Symtab.keys o Data.get
+val supported_atps = Symtab.keys o Data.get
fun is_atp_installed thy name =
let val {exec, required_execs, ...} = get_atp thy name in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 16:10:09 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Feb 08 16:10:10 2011 +0100
@@ -113,7 +113,7 @@
fun is_prover_list ctxt s =
case space_explode " " s of
- ss as _ :: _ => forall (is_prover_available ctxt) ss
+ ss as _ :: _ => forall (is_prover_supported ctxt) ss
| _ => false
fun check_and_repair_raw_param ctxt (name, value) =
@@ -141,23 +141,23 @@
fun merge data : T = AList.merge (op =) (K true) data
)
-fun remotify_prover_if_available_and_not_already_remote ctxt name =
+fun remotify_prover_if_supported_and_not_already_remote ctxt name =
if String.isPrefix remote_prefix name then
SOME name
else
let val remote_name = remote_prefix ^ name in
- if is_prover_available ctxt remote_name then SOME remote_name else NONE
+ if is_prover_supported ctxt remote_name then SOME remote_name else NONE
end
fun remotify_prover_if_not_installed ctxt name =
- if is_prover_available ctxt name andalso is_prover_installed ctxt name then
+ if is_prover_supported ctxt name andalso is_prover_installed ctxt name then
SOME name
else
- remotify_prover_if_available_and_not_already_remote ctxt name
+ remotify_prover_if_supported_and_not_already_remote ctxt name
fun avoid_too_many_local_threads _ _ [] = []
| avoid_too_many_local_threads ctxt 0 provers =
- map_filter (remotify_prover_if_available_and_not_already_remote ctxt)
+ map_filter (remotify_prover_if_supported_and_not_already_remote ctxt)
provers
| avoid_too_many_local_threads ctxt n (prover :: provers) =
let val n = if String.isPrefix remote_prefix prover then n else n - 1 in
@@ -270,7 +270,7 @@
val runN = "run"
val minimizeN = "minimize"
val messagesN = "messages"
-val available_proversN = "available_provers"
+val supported_proversN = "supported_provers"
val running_proversN = "running_provers"
val kill_proversN = "kill_provers"
val refresh_tptpN = "refresh_tptp"
@@ -305,8 +305,8 @@
(#add relevance_override) state
else if subcommand = messagesN then
messages opt_i
- else if subcommand = available_proversN then
- available_provers ctxt
+ else if subcommand = supported_proversN then
+ supported_provers ctxt
else if subcommand = running_proversN then
running_provers ()
else if subcommand = kill_proversN then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 16:10:09 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Feb 08 16:10:10 2011 +0100
@@ -71,7 +71,7 @@
val das_Tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
val is_smt_prover : Proof.context -> string -> bool
- val is_prover_available : Proof.context -> string -> bool
+ val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
val default_max_relevant_for_prover : Proof.context -> string -> int
val is_built_in_const_for_prover :
@@ -89,7 +89,7 @@
val smt_weighted_fact :
theory -> int -> prover_fact * int
-> (string * locality) * (int option * thm)
- val available_provers : Proof.context -> unit
+ val supported_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
@@ -121,16 +121,14 @@
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
-fun is_prover_available ctxt name =
+fun is_prover_supported ctxt name =
let val thy = ProofContext.theory_of ctxt in
- is_smt_prover ctxt name orelse member (op =) (available_atps thy) name
+ is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
end
fun is_prover_installed ctxt =
is_smt_prover ctxt orf is_atp_installed (ProofContext.theory_of ctxt)
-fun available_smt_solvers ctxt = SMT_Solver.available_solvers_of ctxt
-
fun default_max_relevant_for_prover ctxt name =
let val thy = ProofContext.theory_of ctxt in
if is_smt_prover ctxt name then
@@ -205,15 +203,15 @@
fun relevance_fudge_for_prover ctxt name =
if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
-fun available_provers ctxt =
+fun supported_provers ctxt =
let
val thy = ProofContext.theory_of ctxt
val (remote_provers, local_provers) =
- sort_strings (available_atps thy) @
- sort_strings (available_smt_solvers ctxt)
+ sort_strings (supported_atps thy) @
+ sort_strings (SMT_Solver.available_solvers_of ctxt)
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Available provers: " ^
+ Output.urgent_message ("Supported provers: " ^
commas (local_provers @ remote_provers) ^ ".")
end
@@ -672,7 +670,7 @@
let val thy = ProofContext.theory_of ctxt in
if is_smt_prover ctxt name then
run_smt_solver auto name
- else if member (op =) (available_atps thy) name then
+ else if member (op =) (supported_atps thy) name then
run_atp auto name (get_atp thy name)
else
error ("No such prover: " ^ name ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 16:10:09 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Feb 08 16:10:10 2011 +0100
@@ -183,7 +183,7 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val no_dangerous_types = types_dangerous_types type_sys
val _ = () |> not blocking ? kill_provers
- val _ = case find_first (not o is_prover_available ctxt) provers of
+ val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."