src/HOL/Tools/ATP_Manager/atp_manager.ML
changeset 35969 c9565298df9e
parent 35867 16279c4c7a33
child 36058 8256d5a185bd
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 24 14:43:35 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 24 14:49:32 2010 +0100
     1.3 @@ -1,71 +1,92 @@
     1.4  (*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
     1.5      Author:     Fabian Immler, TU Muenchen
     1.6      Author:     Makarius
     1.7 +    Author:     Jasmin Blanchette, TU Muenchen
     1.8  
     1.9  Central manager component for ATP threads.
    1.10  *)
    1.11  
    1.12  signature ATP_MANAGER =
    1.13  sig
    1.14 +  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    1.15 +  type params =
    1.16 +    {debug: bool,
    1.17 +     verbose: bool,
    1.18 +     atps: string list,
    1.19 +     full_types: bool,
    1.20 +     relevance_threshold: real,
    1.21 +     higher_order: bool option,
    1.22 +     respect_no_atp: bool,
    1.23 +     follow_defs: bool,
    1.24 +     isar_proof: bool,
    1.25 +     timeout: Time.time,
    1.26 +     minimize_timeout: Time.time}
    1.27    type problem =
    1.28 -   {with_full_types: bool,
    1.29 -    subgoal: int,
    1.30 -    goal: Proof.context * (thm list * thm),
    1.31 -    axiom_clauses: (thm * (string * int)) list option,
    1.32 -    filtered_clauses: (thm * (string * int)) list option}
    1.33 -  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
    1.34 +    {subgoal: int,
    1.35 +     goal: Proof.context * (thm list * thm),
    1.36 +     relevance_override: relevance_override,
    1.37 +     axiom_clauses: (thm * (string * int)) list option,
    1.38 +     filtered_clauses: (thm * (string * int)) list option}
    1.39    type prover_result =
    1.40 -   {success: bool,
    1.41 -    message: string,
    1.42 -    theorem_names: string list,
    1.43 -    runtime: int,
    1.44 -    proof: string,
    1.45 -    internal_thm_names: string Vector.vector,
    1.46 -    filtered_clauses: (thm * (string * int)) list}
    1.47 -  type prover = int -> problem -> prover_result
    1.48 +    {success: bool,
    1.49 +     message: string,
    1.50 +     relevant_thm_names: string list,
    1.51 +     atp_run_time_in_msecs: int,
    1.52 +     proof: string,
    1.53 +     internal_thm_names: string Vector.vector,
    1.54 +     filtered_clauses: (thm * (string * int)) list}
    1.55 +  type prover = params -> Time.time -> problem -> prover_result
    1.56  
    1.57    val atps: string Unsynchronized.ref
    1.58 -  val get_atps: unit -> string list
    1.59    val timeout: int Unsynchronized.ref
    1.60    val full_types: bool Unsynchronized.ref
    1.61 -  val kill: unit -> unit
    1.62 -  val info: unit -> unit
    1.63 +  val kill_atps: unit -> unit
    1.64 +  val running_atps: unit -> unit
    1.65    val messages: int option -> unit
    1.66    val add_prover: string * prover -> theory -> theory
    1.67    val get_prover: theory -> string -> prover option
    1.68 -  val print_provers: theory -> unit
    1.69 -  val sledgehammer: string list -> Proof.state -> unit
    1.70 +  val available_atps: theory -> unit
    1.71 +  val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
    1.72  end;
    1.73  
    1.74  structure ATP_Manager : ATP_MANAGER =
    1.75  struct
    1.76  
    1.77 -(** problems, results, and provers **)
    1.78 +type relevance_override = Sledgehammer_Fact_Filter.relevance_override
    1.79 +
    1.80 +(** parameters, problems, results, and provers **)
    1.81 +
    1.82 +(* TODO: "theory_const", "blacklist_filter", "convergence" *)
    1.83 +type params =
    1.84 +  {debug: bool,
    1.85 +   verbose: bool,
    1.86 +   atps: string list,
    1.87 +   full_types: bool,
    1.88 +   relevance_threshold: real,
    1.89 +   higher_order: bool option,
    1.90 +   respect_no_atp: bool,
    1.91 +   follow_defs: bool,
    1.92 +   isar_proof: bool,
    1.93 +   timeout: Time.time,
    1.94 +   minimize_timeout: Time.time}
    1.95  
    1.96  type problem =
    1.97 - {with_full_types: bool,
    1.98 -  subgoal: int,
    1.99 -  goal: Proof.context * (thm list * thm),
   1.100 -  axiom_clauses: (thm * (string * int)) list option,
   1.101 -  filtered_clauses: (thm * (string * int)) list option};
   1.102 -
   1.103 -fun problem_of_goal with_full_types subgoal goal : problem =
   1.104 - {with_full_types = with_full_types,
   1.105 -  subgoal = subgoal,
   1.106 -  goal = goal,
   1.107 -  axiom_clauses = NONE,
   1.108 -  filtered_clauses = NONE};
   1.109 +  {subgoal: int,
   1.110 +   goal: Proof.context * (thm list * thm),
   1.111 +   relevance_override: relevance_override,
   1.112 +   axiom_clauses: (thm * (string * int)) list option,
   1.113 +   filtered_clauses: (thm * (string * int)) list option};
   1.114  
   1.115  type prover_result =
   1.116 - {success: bool,
   1.117 -  message: string,
   1.118 -  theorem_names: string list,  (*relevant theorems*)
   1.119 -  runtime: int,  (*user time of the ATP, in milliseconds*)
   1.120 -  proof: string,
   1.121 -  internal_thm_names: string Vector.vector,
   1.122 -  filtered_clauses: (thm * (string * int)) list};
   1.123 +  {success: bool,
   1.124 +   message: string,
   1.125 +   relevant_thm_names: string list,
   1.126 +   atp_run_time_in_msecs: int,
   1.127 +   proof: string,
   1.128 +   internal_thm_names: string Vector.vector,
   1.129 +   filtered_clauses: (thm * (string * int)) list};
   1.130  
   1.131 -type prover = int -> problem -> prover_result;
   1.132 +type prover = params -> Time.time -> problem -> prover_result;
   1.133  
   1.134  
   1.135  (** preferences **)
   1.136 @@ -74,8 +95,6 @@
   1.137  val message_display_limit = 5;
   1.138  
   1.139  val atps = Unsynchronized.ref "e spass remote_vampire";
   1.140 -fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
   1.141 -
   1.142  val timeout = Unsynchronized.ref 60;
   1.143  val full_types = Unsynchronized.ref false;
   1.144  
   1.145 @@ -218,9 +237,9 @@
   1.146  
   1.147  (** user commands **)
   1.148  
   1.149 -(* kill *)
   1.150 +(* kill ATPs *)
   1.151  
   1.152 -fun kill () = Synchronized.change global_state
   1.153 +fun kill_atps () = Synchronized.change global_state
   1.154    (fn {manager, timeout_heap, active, cancelling, messages, store} =>
   1.155      let
   1.156        val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
   1.157 @@ -228,11 +247,11 @@
   1.158      in state' end);
   1.159  
   1.160  
   1.161 -(* info *)
   1.162 +(* running_atps *)
   1.163  
   1.164  fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
   1.165  
   1.166 -fun info () =
   1.167 +fun running_atps () =
   1.168    let
   1.169      val {active, cancelling, ...} = Synchronized.value global_state;
   1.170  
   1.171 @@ -287,44 +306,51 @@
   1.172  fun get_prover thy name =
   1.173    Option.map #1 (Symtab.lookup (Provers.get thy) name);
   1.174  
   1.175 -fun print_provers thy = Pretty.writeln
   1.176 -  (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
   1.177 +fun available_atps thy = Pretty.writeln
   1.178 +  (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
   1.179  
   1.180  
   1.181  (* start prover thread *)
   1.182  
   1.183 -fun start_prover name birth_time death_time i proof_state =
   1.184 +fun start_prover (params as {timeout, ...}) birth_time death_time i
   1.185 +                 relevance_override proof_state name =
   1.186    (case get_prover (Proof.theory_of proof_state) name of
   1.187 -    NONE => warning ("Unknown external prover: " ^ quote name)
   1.188 +    NONE => warning ("Unknown ATP: " ^ quote name)
   1.189    | SOME prover =>
   1.190        let
   1.191          val {context = ctxt, facts, goal} = Proof.goal proof_state;
   1.192          val desc =
   1.193 -          "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
   1.194 +          "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
   1.195              Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
   1.196  
   1.197          val _ = Toplevel.thread true (fn () =>
   1.198            let
   1.199              val _ = register birth_time death_time (Thread.self (), desc);
   1.200 -            val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
   1.201 -            val message = #message (prover (! timeout) problem)
   1.202 +            val problem =
   1.203 +              {subgoal = i, goal = (ctxt, (facts, goal)),
   1.204 +               relevance_override = relevance_override, axiom_clauses = NONE,
   1.205 +               filtered_clauses = NONE}
   1.206 +            val message = #message (prover params timeout problem)
   1.207                handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
   1.208 -                  "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
   1.209 +                  "Try this command: " ^
   1.210 +                  Markup.markup Markup.sendback "by metis" ^ "."
   1.211                  | ERROR msg => ("Error: " ^ msg);
   1.212              val _ = unregister message (Thread.self ());
   1.213            in () end);
   1.214        in () end);
   1.215  
   1.216  
   1.217 -(* sledghammer for first subgoal *)
   1.218 +(* Sledgehammer the given subgoal *)
   1.219  
   1.220 -fun sledgehammer names proof_state =
   1.221 +fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
   1.222 +                 proof_state =
   1.223    let
   1.224 -    val provers = if null names then get_atps () else names;
   1.225 -    val birth_time = Time.now ();
   1.226 -    val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout));
   1.227 -    val _ = kill ();   (*RACE wrt. other invocations of sledgehammer*)
   1.228 -    val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
   1.229 -  in () end;
   1.230 +    val birth_time = Time.now ()
   1.231 +    val death_time = Time.+ (birth_time, timeout)
   1.232 +    val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
   1.233 +    val _ = priority "Sledgehammering..."
   1.234 +    val _ = List.app (start_prover params birth_time death_time i
   1.235 +                                   relevance_override proof_state) atps
   1.236 +  in () end
   1.237  
   1.238  end;