--- a/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Fri May 27 10:30:07 2011 +0200
@@ -544,9 +544,9 @@
\prew
\slshape
The prover found a type-unsound proof involving ``\textit{foo}'',
-``\textit{bar}'', ``\textit{baz}'' even though a supposedly type-sound encoding
-was used (or, less likely, your axioms are inconsistent). You might want to
-report this to the Isabelle developers.
+``\textit{bar}'', and ``\textit{baz}'' even though a supposedly type-sound
+encoding was used (or, less likely, your axioms are inconsistent). You might
+want to report this to the Isabelle developers.
\postw
\point{Auto can solve it---why not Sledgehammer?}
--- a/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri May 27 10:30:07 2011 +0200
@@ -44,6 +44,7 @@
type 'a proof = ('a, 'a, 'a fo_term) formula step list
+ val serial_commas : string -> string list -> string list
val strip_spaces : bool -> (char -> bool) -> string -> string
val short_output : bool -> string -> string
val string_for_failure : failure -> string
@@ -93,6 +94,12 @@
InternalError |
UnknownError of string
+fun serial_commas _ [] = ["??"]
+ | serial_commas _ [s] = [s]
+ | serial_commas conj [s1, s2] = [s1, conj, s2]
+ | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+ | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
fun strip_c_style_comment _ [] = []
| strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
strip_spaces_in_list true is_evil cs
@@ -141,7 +148,8 @@
\remote provers."
fun involving [] = ""
- | involving ss = "involving " ^ commas_quote ss ^ " "
+ | involving ss =
+ "involving " ^ space_implode " " (serial_commas "and" (map quote ss)) ^ " "
fun string_for_failure Unprovable = "The problem is unprovable."
| string_for_failure IncompleteUnprovable = "The prover gave up."
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Fri May 27 10:30:07 2011 +0200
@@ -8,9 +8,11 @@
signature ASYNC_MANAGER =
sig
- val break_into_chunks : string list -> string list
+ val implode_desc : string * string -> string
+ val break_into_chunks : string -> string list
val launch :
- string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
+ string -> Time.time -> Time.time -> string * string
+ -> (unit -> bool * string) -> unit
val kill_threads : string -> string -> unit
val running_threads : string -> string -> unit
val thread_messages : string -> string -> int option -> unit
@@ -27,6 +29,12 @@
(** thread management **)
+val implode_desc = op ^ o apfst quote
+
+fun implode_message (workers, work) =
+ space_implode " " (ATP_Proof.serial_commas "and" (map quote workers)) ^ work
+
+
(* data structures over threads *)
structure Thread_Heap = Heap
@@ -45,10 +53,12 @@
type state =
{manager: Thread.thread option,
timeout_heap: Thread_Heap.T,
- active: (Thread.thread * (string * Time.time * Time.time * string)) list,
- canceling: (Thread.thread * (string * Time.time * string)) list,
- messages: (string * string) list,
- store: (string * string) list}
+ active:
+ (Thread.thread
+ * (string * Time.time * Time.time * (string * string))) list,
+ canceling: (Thread.thread * (string * Time.time * (string * string))) list,
+ messages: (bool * (string * (string * string))) list,
+ store: (string * (string * string)) list}
fun make_state manager timeout_heap active canceling messages store : state =
{manager = manager, timeout_heap = timeout_heap, active = active,
@@ -60,17 +70,17 @@
(* unregister thread *)
-fun unregister message thread =
+fun unregister (urgent, message) thread =
Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
(case lookup_thread active thread of
- SOME (tool, _, _, desc) =>
+ SOME (tool, _, _, desc as (worker, its_desc)) =>
let
val active' = delete_thread thread active;
val now = Time.now ()
val canceling' = (thread, (tool, now, desc)) :: canceling
- val message' = desc ^ "\n" ^ message
- val messages' = (tool, message') :: messages;
+ val message' = (worker, its_desc ^ "\n" ^ message)
+ val messages' = (urgent, (tool, message')) :: messages
val store' = (tool, message') ::
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store));
@@ -95,18 +105,23 @@
(* This is a workaround for Proof General's off-by-a-few sendback display bug,
whereby "pr" in "proof" is not highlighted. *)
-val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
+val break_into_chunks = space_explode "\000" o replace_all "\n\n" "\000"
fun print_new_messages () =
- case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, canceling, messages, store} =>
- (messages, make_state manager timeout_heap active canceling []
- store)) of
- [] => ()
- | msgs as (tool, _) :: _ =>
- let val ss = break_into_chunks (map snd msgs) in
- List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
- end
+ Synchronized.change_result global_state
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ messages
+ |> List.partition (fn (urgent, _) => null active orelse urgent)
+ ||> (fn postponed_messages =>
+ make_state manager timeout_heap active canceling
+ postponed_messages store))
+ |> map (fn (_, (tool, (worker, work))) => ((tool, work), worker))
+ |> AList.group (op =)
+ |> List.app (fn ((tool, work), workers) =>
+ tool ^ ": " ^
+ implode_message (workers |> sort string_ord, work)
+ |> break_into_chunks
+ |> List.app Output.urgent_message)
fun check_thread_manager () = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
@@ -141,7 +156,7 @@
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
|> these
- |> List.app (unregister "Timed out.\n");
+ |> List.app (unregister (false, "Timed out.\n"));
print_new_messages ();
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
@@ -168,8 +183,7 @@
let
val self = Thread.self ()
val _ = register tool birth_time death_time desc self
- val message = f ()
- in unregister message self end);
+ in unregister (f ()) self end);
())
@@ -177,7 +191,7 @@
(* kill threads *)
-fun kill_threads tool workers = Synchronized.change global_state
+fun kill_threads tool das_wort_worker = Synchronized.change global_state
(fn {manager, timeout_heap, active, canceling, messages, store} =>
let
val killing =
@@ -185,7 +199,9 @@
if tool' = tool then SOME (th, (tool', Time.now (), desc))
else NONE) active
val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
- val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
+ val _ =
+ if null killing then ()
+ else Output.urgent_message ("Killed active " ^ das_wort_worker ^ "s.")
in state' end);
@@ -193,7 +209,7 @@
fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
-fun running_threads tool workers =
+fun running_threads tool das_wort_worker =
let
val {active, canceling, ...} = Synchronized.value global_state;
@@ -201,37 +217,36 @@
fun running_info (_, (tool', birth_time, death_time, desc)) =
if tool' = tool then
SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
- seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
+ seconds (Time.- (death_time, now)) ^ " to live:\n" ^
+ implode_desc desc)
else
NONE
fun canceling_info (_, (tool', death_time, desc)) =
if tool' = tool then
- SOME ("Trying to interrupt thread since " ^
- seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
+ SOME ("Trying to interrupt " ^ das_wort_worker ^ " since " ^
+ seconds (Time.- (now, death_time)) ^ ":\n" ^ implode_desc desc)
else
NONE
val running =
case map_filter running_info active of
- [] => ["No " ^ workers ^ " running."]
- | ss => "Running " ^ workers ^ ":" :: ss
+ [] => ["No " ^ das_wort_worker ^ "s running."]
+ | ss => "Running " ^ das_wort_worker ^ "s " :: ss
val interrupting =
case map_filter canceling_info canceling of
[] => []
- | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
+ | ss => "Interrupting " ^ das_wort_worker ^ "s " :: ss
in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
-fun thread_messages tool worker opt_limit =
+fun thread_messages tool das_wort_worker opt_limit =
let
val limit = the_default message_display_limit opt_limit;
val tool_store = Synchronized.value global_state
|> #store |> filter (curry (op =) tool o fst)
val header =
- "Recent " ^ worker ^ " messages" ^
+ "Recent " ^ das_wort_worker ^ " messages" ^
(if length tool_store <= limit then ":"
else " (" ^ string_of_int limit ^ " displayed):");
- in
- List.app Output.urgent_message (header :: break_into_chunks
- (map snd (#1 (chop limit tool_store))))
- end
+ val ss = tool_store |> chop limit |> #1 |> map (implode_desc o snd)
+ in List.app Output.urgent_message (header :: maps break_into_chunks ss) end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
@@ -68,7 +68,7 @@
val smt_slice_fact_frac : real Config.T
val smt_slice_time_frac : real Config.T
val smt_slice_min_secs : int Config.T
- val das_Tool : string
+ val das_tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
val is_smt_prover : Proof.context -> string -> bool
val is_unit_equational_atp : Proof.context -> string -> bool
@@ -115,7 +115,7 @@
(* Identifier to distinguish Sledgehammer from other tools using
"Async_Manager". *)
-val das_Tool = "Sledgehammer"
+val das_tool = "Sledgehammer"
val select_smt_solver =
Context.proof_map o SMT_Config.select_solver
@@ -252,9 +252,9 @@
commas (local_provers @ remote_provers) ^ ".")
end
-fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
-fun running_provers () = Async_Manager.running_threads das_Tool "provers"
-val messages = Async_Manager.thread_messages das_Tool "prover"
+fun kill_provers () = Async_Manager.kill_threads das_tool "prover"
+fun running_provers () = Async_Manager.running_threads das_tool "prover"
+val messages = Async_Manager.thread_messages das_tool "prover"
(** problems, results, ATPs, etc. **)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:07 2011 +0200
@@ -31,16 +31,16 @@
fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
n goal =
- quote name ^
- (if verbose then
- " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
- else
- "") ^
- " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
- (if blocking then
- "."
- else
- ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+ (name,
+ (if verbose then
+ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
+ else
+ "") ^
+ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
+ (if blocking then
+ "."
+ else
+ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
val auto_minimize_min_facts =
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
@@ -86,6 +86,11 @@
| NONE => result
end)
+val someN = "some"
+val noneN = "none"
+val timeoutN = "timeout"
+val unknownN = "unknown"
+
fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
expect, ...})
auto minimize_command only
@@ -109,7 +114,9 @@
problem
|> get_minimizing_prover ctxt auto name params (minimize_command name)
|> (fn {outcome, message, ...} =>
- (if is_some outcome then "none" else "some" (* sic *), message))
+ (if outcome = SOME ATP_Proof.TimedOut then timeoutN
+ else if is_some outcome then noneN
+ else someN, message))
fun go () =
let
val (outcome_code, message) =
@@ -117,13 +124,13 @@
really_go ()
else
(really_go ()
- handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
+ handle ERROR message => (unknownN, "Error: " ^ message ^ "\n")
| exn =>
if Exn.is_interrupt exn then
reraise exn
else
- ("unknown", "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
+ (unknownN, "Internal error:\n" ^
+ ML_Compiler.exn_message exn ^ "\n"))
val _ =
(* The "expect" argument is deliberately ignored if the prover is
missing so that the "Metis_Examples" can be processed on any
@@ -135,22 +142,27 @@
error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
else
warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
- in (outcome_code = "some", message) end
+ in (outcome_code, message) end
in
if auto then
- let val (success, message) = TimeLimit.timeLimit timeout go () in
+ let
+ val (outcome_code, message) = TimeLimit.timeLimit timeout go ()
+ val success = (outcome_code = someN)
+ in
(success, state |> success ? Proof.goal_message (fn () =>
Pretty.chunks [Pretty.str "",
Pretty.mark Markup.hilite (Pretty.str message)]))
end
else if blocking then
- let val (success, message) = TimeLimit.timeLimit hard_timeout go () in
- List.app Output.urgent_message
- (Async_Manager.break_into_chunks [desc ^ "\n" ^ message]);
- (success, state)
+ let val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go () in
+ Async_Manager.implode_desc desc ^ "\n" ^ message
+ |> Async_Manager.break_into_chunks
+ |> List.app Output.urgent_message;
+ (outcome_code = someN, state)
end
else
- (Async_Manager.launch das_Tool birth_time death_time desc (snd o go);
+ (Async_Manager.launch das_tool birth_time death_time desc
+ (apfst (curry (op <>) timeoutN) o go);
(false, state))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri May 27 10:30:07 2011 +0200
@@ -38,12 +38,7 @@
fun plural_s n = if n = 1 then "" else "s"
-fun serial_commas _ [] = ["??"]
- | serial_commas _ [s] = [s]
- | serial_commas conj [s1, s2] = [s1, conj, s2]
- | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
- | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-
+val serial_commas = ATP_Proof.serial_commas
val simplify_spaces = ATP_Proof.strip_spaces false (K true)
fun parse_bool_option option name s =