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