src/HOL/Tools/ATP_Manager/atp_manager.ML
author blanchet
Tue Apr 20 16:04:36 2010 +0200 (2010-04-20 ago)
changeset 36235 61159615a0c5
parent 36231 bede2d49ba3b
child 36281 dbbf4d5d584d
permissions -rw-r--r--
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
     1 (*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Central manager component for ATP threads.
     7 *)
     8 
     9 signature ATP_MANAGER =
    10 sig
    11   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    12   type params =
    13     {debug: bool,
    14      verbose: bool,
    15      overlord: bool,
    16      atps: string list,
    17      full_types: bool,
    18      explicit_apply: bool,
    19      respect_no_atp: bool,
    20      relevance_threshold: real,
    21      convergence: real,
    22      theory_relevant: bool option,
    23      higher_order: bool option,
    24      follow_defs: bool,
    25      isar_proof: bool,
    26      modulus: int,
    27      sorts: bool,
    28      timeout: Time.time,
    29      minimize_timeout: Time.time}
    30   type problem =
    31     {subgoal: int,
    32      goal: Proof.context * (thm list * thm),
    33      relevance_override: relevance_override,
    34      axiom_clauses: (thm * (string * int)) list option,
    35      filtered_clauses: (thm * (string * int)) list option}
    36   type prover_result =
    37     {success: bool,
    38      message: string,
    39      relevant_thm_names: string list,
    40      atp_run_time_in_msecs: int,
    41      proof: string,
    42      internal_thm_names: string Vector.vector,
    43      filtered_clauses: (thm * (string * int)) list}
    44   type prover = params -> Time.time -> problem -> prover_result
    45 
    46   val atps: string Unsynchronized.ref
    47   val timeout: int Unsynchronized.ref
    48   val full_types: bool Unsynchronized.ref
    49   val kill_atps: unit -> unit
    50   val running_atps: unit -> unit
    51   val messages: int option -> unit
    52   val add_prover: string * prover -> theory -> theory
    53   val get_prover: theory -> string -> prover option
    54   val available_atps: theory -> unit
    55   val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
    56 end;
    57 
    58 structure ATP_Manager : ATP_MANAGER =
    59 struct
    60 
    61 open Sledgehammer_Util
    62 open Sledgehammer_Fact_Filter
    63 open Sledgehammer_Proof_Reconstruct
    64 
    65 (** parameters, problems, results, and provers **)
    66 
    67 type params =
    68   {debug: bool,
    69    verbose: bool,
    70    overlord: bool,
    71    atps: string list,
    72    full_types: bool,
    73    explicit_apply: bool,
    74    respect_no_atp: bool,
    75    relevance_threshold: real,
    76    convergence: real,
    77    theory_relevant: bool option,
    78    higher_order: bool option,
    79    follow_defs: bool,
    80    isar_proof: bool,
    81    modulus: int,
    82    sorts: bool,
    83    timeout: Time.time,
    84    minimize_timeout: Time.time}
    85 
    86 type problem =
    87   {subgoal: int,
    88    goal: Proof.context * (thm list * thm),
    89    relevance_override: relevance_override,
    90    axiom_clauses: (thm * (string * int)) list option,
    91    filtered_clauses: (thm * (string * int)) list option};
    92 
    93 type prover_result =
    94   {success: bool,
    95    message: string,
    96    relevant_thm_names: string list,
    97    atp_run_time_in_msecs: int,
    98    proof: string,
    99    internal_thm_names: string Vector.vector,
   100    filtered_clauses: (thm * (string * int)) list};
   101 
   102 type prover = params -> Time.time -> problem -> prover_result;
   103 
   104 
   105 (** preferences **)
   106 
   107 val message_store_limit = 20;
   108 val message_display_limit = 5;
   109 
   110 val atps = Unsynchronized.ref "e spass remote_vampire";
   111 val timeout = Unsynchronized.ref 60;
   112 val full_types = Unsynchronized.ref false;
   113 
   114 val _ =
   115   ProofGeneralPgip.add_preference Preferences.category_proof
   116     (Preferences.string_pref atps
   117       "ATP: provers" "Default automatic provers (separated by whitespace)");
   118 
   119 val _ =
   120   ProofGeneralPgip.add_preference Preferences.category_proof
   121     (Preferences.int_pref timeout
   122       "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
   123 
   124 val _ =
   125   ProofGeneralPgip.add_preference Preferences.category_proof
   126     (Preferences.bool_pref full_types
   127       "ATP: full types" "ATPs will use full type information");
   128 
   129 
   130 
   131 (** thread management **)
   132 
   133 (* data structures over threads *)
   134 
   135 structure Thread_Heap = Heap
   136 (
   137   type elem = Time.time * Thread.thread;
   138   fun ord ((a, _), (b, _)) = Time.compare (a, b);
   139 );
   140 
   141 fun lookup_thread xs = AList.lookup Thread.equal xs;
   142 fun delete_thread xs = AList.delete Thread.equal xs;
   143 fun update_thread xs = AList.update Thread.equal xs;
   144 
   145 
   146 (* state of thread manager *)
   147 
   148 type state =
   149  {manager: Thread.thread option,
   150   timeout_heap: Thread_Heap.T,
   151   active: (Thread.thread * (Time.time * Time.time * string)) list,
   152   cancelling: (Thread.thread * (Time.time * string)) list,
   153   messages: string list,
   154   store: string list};
   155 
   156 fun make_state manager timeout_heap active cancelling messages store : state =
   157   {manager = manager, timeout_heap = timeout_heap, active = active,
   158     cancelling = cancelling, messages = messages, store = store};
   159 
   160 val global_state = Synchronized.var "atp_manager"
   161   (make_state NONE Thread_Heap.empty [] [] [] []);
   162 
   163 
   164 (* unregister ATP thread *)
   165 
   166 fun unregister ({verbose, ...} : params) message thread =
   167   Synchronized.change global_state
   168   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
   169     (case lookup_thread active thread of
   170       SOME (birth_time, _, description) =>
   171         let
   172           val active' = delete_thread thread active;
   173           val now = Time.now ()
   174           val cancelling' = (thread, (now, description)) :: cancelling;
   175           val message' =
   176             description ^ "\n" ^ message ^
   177             (if verbose then
   178                "Total time: " ^ Int.toString (Time.toMilliseconds
   179                                           (Time.- (now, birth_time))) ^ " ms.\n"
   180              else
   181                "")
   182           val messages' = message' :: messages;
   183           val store' = message' ::
   184             (if length store <= message_store_limit then store
   185              else #1 (chop message_store_limit store));
   186         in make_state manager timeout_heap active' cancelling' messages' store' end
   187     | NONE => state));
   188 
   189 
   190 (* main manager thread -- only one may exist *)
   191 
   192 val min_wait_time = Time.fromMilliseconds 300;
   193 val max_wait_time = Time.fromSeconds 10;
   194 
   195 (* This is a workaround for Proof General's off-by-a-few sendback display bug,
   196    whereby "pr" in "proof" is not highlighted. *)
   197 val break_into_chunks =
   198   map (replace_all "\n\n" "\000") #> maps (space_explode "\000")
   199 
   200 fun print_new_messages () =
   201   case Synchronized.change_result global_state
   202          (fn {manager, timeout_heap, active, cancelling, messages, store} =>
   203              (messages, make_state manager timeout_heap active cancelling []
   204                                    store)) of
   205     [] => ()
   206   | msgs =>
   207     msgs |> break_into_chunks
   208          |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs)
   209          |> List.app priority
   210 
   211 fun check_thread_manager params = Synchronized.change global_state
   212   (fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
   213     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
   214     else let val manager = SOME (Toplevel.thread false (fn () =>
   215       let
   216         fun time_limit timeout_heap =
   217           (case try Thread_Heap.min timeout_heap of
   218             NONE => Time.+ (Time.now (), max_wait_time)
   219           | SOME (time, _) => time);
   220 
   221         (*action: find threads whose timeout is reached, and interrupt cancelling threads*)
   222         fun action {manager, timeout_heap, active, cancelling, messages, store} =
   223           let val (timeout_threads, timeout_heap') =
   224             Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
   225           in
   226             if null timeout_threads andalso null cancelling
   227             then NONE
   228             else
   229               let
   230                 val _ = List.app (SimpleThread.interrupt o #1) cancelling;
   231                 val cancelling' = filter (Thread.isActive o #1) cancelling;
   232                 val state' = make_state manager timeout_heap' active cancelling' messages store;
   233               in SOME (map #2 timeout_threads, state') end
   234           end;
   235       in
   236         while Synchronized.change_result global_state
   237           (fn state as {timeout_heap, active, cancelling, messages, store, ...} =>
   238             if null active andalso null cancelling andalso null messages
   239             then (false, make_state NONE timeout_heap active cancelling messages store)
   240             else (true, state))
   241         do
   242           (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
   243             |> these
   244             |> List.app (unregister params "Timed out.");
   245             print_new_messages ();
   246             (*give threads some time to respond to interrupt*)
   247             OS.Process.sleep min_wait_time)
   248       end))
   249     in make_state manager timeout_heap active cancelling messages store end);
   250 
   251 
   252 (* register ATP thread *)
   253 
   254 fun register params birth_time death_time (thread, desc) =
   255  (Synchronized.change global_state
   256     (fn {manager, timeout_heap, active, cancelling, messages, store} =>
   257       let
   258         val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
   259         val active' = update_thread (thread, (birth_time, death_time, desc)) active;
   260         val state' = make_state manager timeout_heap' active' cancelling messages store;
   261       in state' end);
   262   check_thread_manager params);
   263 
   264 
   265 
   266 (** user commands **)
   267 
   268 (* kill ATPs *)
   269 
   270 fun kill_atps () = Synchronized.change global_state
   271   (fn {manager, timeout_heap, active, cancelling, messages, store} =>
   272     let
   273       val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
   274       val state' = make_state manager timeout_heap [] (killing @ cancelling) messages store;
   275     in state' end);
   276 
   277 
   278 (* running_atps *)
   279 
   280 fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
   281 
   282 fun running_atps () =
   283   let
   284     val {active, cancelling, ...} = Synchronized.value global_state;
   285 
   286     val now = Time.now ();
   287     fun running_info (_, (birth_time, death_time, desc)) =
   288       "Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
   289         seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc;
   290     fun cancelling_info (_, (deadth_time, desc)) =
   291       "Trying to interrupt thread since " ^ seconds (Time.- (now, deadth_time)) ^ ":\n" ^ desc;
   292 
   293     val running =
   294       if null active then "No ATPs running."
   295       else space_implode "\n\n" ("Running ATPs:" :: map running_info active);
   296     val interrupting =
   297       if null cancelling then ""
   298       else
   299         space_implode "\n\n"
   300           ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling);
   301 
   302   in priority (running ^ "\n" ^ interrupting) end;
   303 
   304 fun messages opt_limit =
   305   let
   306     val limit = the_default message_display_limit opt_limit;
   307     val {store, ...} = Synchronized.value global_state;
   308     val header =
   309       "Recent ATP messages" ^
   310         (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
   311   in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end
   312 
   313 
   314 (** The Sledgehammer **)
   315 
   316 (* named provers *)
   317 
   318 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ ".");
   319 
   320 structure Provers = Theory_Data
   321 (
   322   type T = (prover * stamp) Symtab.table;
   323   val empty = Symtab.empty;
   324   val extend = I;
   325   fun merge data : T = Symtab.merge (eq_snd op =) data
   326     handle Symtab.DUP dup => err_dup_prover dup;
   327 );
   328 
   329 fun add_prover (name, prover) thy =
   330   Provers.map (Symtab.update_new (name, (prover, stamp ()))) thy
   331     handle Symtab.DUP dup => err_dup_prover dup;
   332 
   333 fun get_prover thy name =
   334   Option.map #1 (Symtab.lookup (Provers.get thy) name);
   335 
   336 fun available_atps thy =
   337   priority ("Available ATPs: " ^
   338             commas (sort_strings (Symtab.keys (Provers.get thy))) ^ ".")
   339 
   340 
   341 (* start prover thread *)
   342 
   343 fun start_prover (params as {timeout, ...}) birth_time death_time i
   344                  relevance_override proof_state name =
   345   (case get_prover (Proof.theory_of proof_state) name of
   346     NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
   347   | SOME prover =>
   348       let
   349         val {context = ctxt, facts, goal} = Proof.goal proof_state;
   350         val n = Logic.count_prems (prop_of goal)
   351         val desc =
   352           "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
   353             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
   354 
   355         val _ = Toplevel.thread true (fn () =>
   356           let
   357             val _ = register params birth_time death_time (Thread.self (), desc)
   358             val problem =
   359               {subgoal = i, goal = (ctxt, (facts, goal)),
   360                relevance_override = relevance_override, axiom_clauses = NONE,
   361                filtered_clauses = NONE}
   362             val message = #message (prover params timeout problem)
   363               handle Sledgehammer_HOL_Clause.TRIVIAL =>
   364                   metis_line i n []
   365                 | ERROR msg => "Error: " ^ msg ^ ".\n";
   366             val _ = unregister params message (Thread.self ());
   367           in () end);
   368       in () end);
   369 
   370 
   371 (* Sledgehammer the given subgoal *)
   372 
   373 fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
   374                  proof_state =
   375   let
   376     val birth_time = Time.now ()
   377     val death_time = Time.+ (birth_time, timeout)
   378     val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
   379     val _ = priority "Sledgehammering..."
   380     val _ = List.app (start_prover params birth_time death_time i
   381                                    relevance_override proof_state) atps
   382   in () end
   383 
   384 end;