--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 17:13:38 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Jun 25 17:26:14 2010 +0200
@@ -19,7 +19,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -78,7 +77,6 @@
atps: string list,
full_types: bool,
explicit_apply: bool,
- respect_no_atp: bool,
relevance_threshold: real,
relevance_convergence: real,
theory_relevant: bool option,
@@ -142,13 +140,13 @@
{manager: Thread.thread option,
timeout_heap: Thread_Heap.T,
active: (Thread.thread * (Time.time * Time.time * string)) list,
- cancelling: (Thread.thread * (Time.time * string)) list,
+ canceling: (Thread.thread * (Time.time * string)) list,
messages: string list,
store: string list};
-fun make_state manager timeout_heap active cancelling messages store : state =
+fun make_state manager timeout_heap active canceling messages store : state =
{manager = manager, timeout_heap = timeout_heap, active = active,
- cancelling = cancelling, messages = messages, store = store};
+ canceling = canceling, messages = messages, store = store}
val global_state = Synchronized.var "atp_manager"
(make_state NONE Thread_Heap.empty [] [] [] []);
@@ -158,13 +156,13 @@
fun unregister ({verbose, ...} : params) message thread =
Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
(case lookup_thread active thread of
SOME (birth_time, _, desc) =>
let
val active' = delete_thread thread active;
val now = Time.now ()
- val cancelling' = (thread, (now, desc)) :: cancelling;
+ val canceling' = (thread, (now, desc)) :: canceling
val message' =
desc ^ "\n" ^ message ^
(if verbose then
@@ -176,7 +174,7 @@
val store' = message' ::
(if length store <= message_store_limit then store
else #1 (chop message_store_limit store));
- in make_state manager timeout_heap active' cancelling' messages' store' end
+ in make_state manager timeout_heap active' canceling' messages' store' end
| NONE => state));
@@ -202,8 +200,8 @@
fun print_new_messages () =
case Synchronized.change_result global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
- (messages, make_state manager timeout_heap active cancelling []
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
+ (messages, make_state manager timeout_heap active canceling []
store)) of
[] => ()
| msgs =>
@@ -212,7 +210,7 @@
|> List.app priority
fun check_thread_manager params = Synchronized.change global_state
- (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
+ (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
else let val manager = SOME (Toplevel.thread false (fn () =>
let
@@ -221,25 +219,25 @@
NONE => Time.+ (Time.now (), max_wait_time)
| SOME (time, _) => time);
- (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
- fun action {manager, timeout_heap, active, cancelling, messages, store} =
+ (*action: find threads whose timeout is reached, and interrupt canceling threads*)
+ fun action {manager, timeout_heap, active, canceling, messages, store} =
let val (timeout_threads, timeout_heap') =
Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
in
- if null timeout_threads andalso null cancelling
+ if null timeout_threads andalso null canceling
then NONE
else
let
- val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
- val cancelling' = filter (Thread.isActive o #1) cancelling;
- val state' = make_state manager timeout_heap' active cancelling' messages store;
+ val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val canceling' = filter (Thread.isActive o #1) canceling
+ val state' = make_state manager timeout_heap' active canceling' messages store;
in SOME (map #2 timeout_threads, state') end
end;
in
while Synchronized.change_result global_state
- (fn state as {timeout_heap, active, cancelling, messages, store, ...} =>
- if null active andalso null cancelling andalso null messages
- then (false, make_state NONE timeout_heap active cancelling messages store)
+ (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
+ if null active andalso null canceling andalso null messages
+ then (false, make_state NONE timeout_heap active canceling messages store)
else (true, state))
do
(Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
@@ -249,18 +247,18 @@
(*give threads some time to respond to interrupt*)
OS.Process.sleep min_wait_time)
end))
- in make_state manager timeout_heap active cancelling messages store end);
+ in make_state manager timeout_heap active canceling messages store end)
(* register ATP thread *)
fun register params birth_time death_time (thread, desc) =
(Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
let
val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
val active' = update_thread (thread, (birth_time, death_time, desc)) active;
- val state' = make_state manager timeout_heap' active' cancelling messages store;
+ val state' = make_state manager timeout_heap' active' canceling messages store;
in state' end);
check_thread_manager params);
@@ -271,10 +269,10 @@
(* kill ATPs *)
fun kill_atps () = Synchronized.change global_state
- (fn {manager, timeout_heap, active, cancelling, messages, store} =>
+ (fn {manager, timeout_heap, active, canceling, messages, store} =>
let
val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
- val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
+ val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
val _ = if null active then ()
else priority "Killed active Sledgehammer threads."
in state' end);
@@ -286,24 +284,24 @@
fun running_atps () =
let
- val {active, cancelling, ...} = Synchronized.value global_state;
+ val {active, canceling, ...} = Synchronized.value global_state;
val now = Time.now ();
fun running_info (_, (birth_time, death_time, desc)) =
"Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc;
- fun cancelling_info (_, (deadth_time, desc)) =
+ fun canceling_info (_, (deadth_time, desc)) =
"Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc;
val running =
if null active then "No ATPs running."
else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
val interrupting =
- if null cancelling then ""
+ if null canceling then
+ ""
else
- space_implode "\n\n"
- ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
-
+ space_implode "\n\n" ("Trying to interrupt the following ATPs:" ::
+ map canceling_info canceling)
in priority (running ^ "\n" ^ interrupting) end;
fun messages opt_limit =
@@ -320,25 +318,22 @@
(* named provers *)
-fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
-
structure Data = Theory_Data
(
type T = (prover * stamp) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (eq_snd op =) data
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
);
fun add_prover (name, prover) thy =
Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP name => err_dup_prover name;
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
fun get_prover thy name =
- case Symtab.lookup (Data.get thy) name of
- SOME (prover, _) => prover
- | NONE => error ("Unknown ATP: " ^ name)
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
fun available_atps thy =
priority ("Available ATPs: " ^
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 17:13:38 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri Jun 25 17:26:14 2010 +0200
@@ -126,9 +126,9 @@
fun generic_tptp_prover
(name, {home_var, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
- ({debug, overlord, full_types, explicit_apply, respect_no_atp,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor, ...} : params)
+ ({debug, overlord, full_types, explicit_apply, relevance_threshold,
+ relevance_convergence, theory_relevant, defs_relevant, isar_proof,
+ isar_shrink_factor, ...} : params)
minimize_command timeout
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
: problem) =
@@ -140,7 +140,7 @@
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
(case filtered_clauses of
- NONE => relevant_facts full_types respect_no_atp relevance_threshold
+ NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 17:13:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jun 25 17:26:14 2010 +0200
@@ -68,7 +68,6 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("respect_no_atp", "true"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
("theory_relevant", "smart"),
@@ -85,7 +84,6 @@
("no_overlord", "overlord"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
- ("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
@@ -167,7 +165,6 @@
val atps = lookup_string "atps" |> space_explode " "
val full_types = lookup_bool "full_types"
val explicit_apply = lookup_bool "explicit_apply"
- val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
@@ -181,7 +178,7 @@
in
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+ relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
theory_relevant = theory_relevant, defs_relevant = defs_relevant,
isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,