# HG changeset patch
# User blanchet
# Date 1277479574 -7200
# Node ID c2c1caff5deaf28ac1868cca30471fce13c15c0a
# Parent  61a01843a0281c57cafa9a186635f50eae7af6f2
got rid of "respect_no_atp" option, which even I don't use

diff -r 61a01843a028 -r c2c1caff5dea src/HOL/Tools/ATP_Manager/atp_manager.ML
--- 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: " ^
diff -r 61a01843a028 -r c2c1caff5dea src/HOL/Tools/ATP_Manager/atp_systems.ML
--- 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
diff -r 61a01843a028 -r c2c1caff5dea src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 17:13:38 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Jun 25 17:26:14 2010 +0200
@@ -14,7 +14,7 @@
 
   val use_natural_form : bool Unsynchronized.ref
   val relevant_facts :
-    bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
+    bool -> real -> real -> bool -> int -> bool -> relevance_override
     -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
 end;
 
@@ -24,6 +24,7 @@
 open Clausifier
 open Metis_Clauses
 
+val respect_no_atp = true
 (* Experimental feature: Filter theorems in natural form or in CNF? *)
 val use_natural_form = Unsynchronized.ref false
 
@@ -392,7 +393,7 @@
 val exists_sledgehammer_const =
   exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s) o prop_of
 
-fun all_name_thms_pairs respect_no_atp ctxt chained_ths =
+fun all_name_thms_pairs ctxt chained_ths =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
@@ -436,7 +437,7 @@
 
 (* The single-name theorems go after the multiple-name ones, so that single
    names are preferred when both are available. *)
-fun name_thm_pairs respect_no_atp ctxt name_thms_pairs =
+fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
   let
     val (mults, singles) = List.partition is_multi name_thms_pairs
     val ps = [] |> fold add_names singles |> fold add_names mults
@@ -447,7 +448,7 @@
               Display.string_of_thm_without_context th); false)
   | is_named _ = true
 fun checked_name_thm_pairs respect_no_atp ctxt =
-  name_thm_pairs respect_no_atp ctxt
+  name_thm_pairs ctxt respect_no_atp
   #> tap (fn ps => trace_msg
                         (fn () => ("Considering " ^ Int.toString (length ps) ^
                                    " theorems")))
@@ -505,8 +506,8 @@
     (has_typed_var dangerous_types t orelse
      forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
 
-fun relevant_facts full_types respect_no_atp relevance_threshold
-                   relevance_convergence defs_relevant max_new theory_relevant
+fun relevant_facts full_types relevance_threshold relevance_convergence
+                   defs_relevant max_new theory_relevant
                    (relevance_override as {add, del, only})
                    (ctxt, (chained_ths, _)) goal_cls =
   let
@@ -517,8 +518,7 @@
     val axioms =
       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
           (map (name_thms_pair_from_ref ctxt chained_ths) add @
-           (if only then []
-            else all_name_thms_pairs respect_no_atp ctxt chained_ths))
+           (if only then [] else all_name_thms_pairs ctxt chained_ths))
       |> cnf_rules_pairs thy
       |> not has_override ? make_unique
       |> filter (fn (cnf_thm, (_, orig_thm)) =>
diff -r 61a01843a028 -r c2c1caff5dea src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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,