--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jul 27 17:43:11 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Central manager component for ATP threads.
-*)
-
-signature ATP_MANAGER =
-sig
- type relevance_override = Sledgehammer_Fact_Filter.relevance_override
- type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
- type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- atps: string list,
- full_types: bool,
- explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- theory_relevant: bool option,
- defs_relevant: bool,
- isar_proof: bool,
- isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
- type problem =
- {subgoal: int,
- goal: Proof.context * (thm list * thm),
- relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
- datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
- type prover_result =
- {outcome: failure option,
- message: string,
- pool: string Symtab.table,
- used_thm_names: string list,
- atp_run_time_in_msecs: int,
- output: string,
- proof: string,
- internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
- filtered_clauses: (string * thm) list}
- type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
-
- val kill_atps: unit -> unit
- val running_atps: unit -> unit
- val messages: int option -> unit
- val add_prover: string * prover -> theory -> theory
- val get_prover: theory -> string -> prover
- val available_atps: theory -> unit
- val start_prover_thread :
- params -> int -> int -> relevance_override -> (string -> minimize_command)
- -> Proof.state -> string -> unit
-end;
-
-structure ATP_Manager : ATP_MANAGER =
-struct
-
-open Metis_Clauses
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
-
-(** The Sledgehammer **)
-
-val das_Tool = "Sledgehammer"
-
-fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
-fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
-val messages = Async_Manager.thread_messages das_Tool "ATP"
-
-(** problems, results, provers, etc. **)
-
-type params =
- {debug: bool,
- verbose: bool,
- overlord: bool,
- atps: string list,
- full_types: bool,
- explicit_apply: bool,
- relevance_threshold: real,
- relevance_convergence: real,
- theory_relevant: bool option,
- defs_relevant: bool,
- isar_proof: bool,
- isar_shrink_factor: int,
- timeout: Time.time,
- minimize_timeout: Time.time}
-
-type problem =
- {subgoal: int,
- goal: Proof.context * (thm list * thm),
- relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
-
-datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | MalformedInput | MalformedOutput | UnknownError
-
-type prover_result =
- {outcome: failure option,
- message: string,
- pool: string Symtab.table,
- used_thm_names: string list,
- atp_run_time_in_msecs: int,
- output: string,
- proof: string,
- internal_thm_names: string Vector.vector,
- conjecture_shape: int list,
- filtered_clauses: (string * thm) list}
-
-type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
-
-(* named provers *)
-
-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 => error ("Duplicate ATP: " ^ quote name ^ ".")
-);
-
-fun add_prover (name, prover) thy =
- Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
- handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
-
-fun get_prover thy name =
- the (Symtab.lookup (Data.get thy) name) |> fst
- handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
-
-fun available_atps thy =
- priority ("Available ATPs: " ^
- commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
-
-
-(* start prover thread *)
-
-fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
- relevance_override minimize_command proof_state name =
- let
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, timeout)
- val prover = get_prover (Proof.theory_of proof_state) name
- val {context = ctxt, facts, goal} = Proof.goal proof_state;
- val desc =
- "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
- Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
- in
- Async_Manager.launch das_Tool verbose birth_time death_time desc
- (fn () =>
- let
- val problem =
- {subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
- in
- prover params (minimize_command name) timeout problem |> #message
- handle ERROR message => "Error: " ^ message ^ "\n"
- end)
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Jul 27 17:49:16 2010 +0200
@@ -0,0 +1,171 @@
+(* Title: HOL/Tools/ATP_Manager/atp_manager.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Central manager component for ATP threads.
+*)
+
+signature ATP_MANAGER =
+sig
+ type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+ type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
+ type params =
+ {debug: bool,
+ verbose: bool,
+ overlord: bool,
+ atps: string list,
+ full_types: bool,
+ explicit_apply: bool,
+ relevance_threshold: real,
+ relevance_convergence: real,
+ theory_relevant: bool option,
+ defs_relevant: bool,
+ isar_proof: bool,
+ isar_shrink_factor: int,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
+ type problem =
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
+ datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
+ type prover_result =
+ {outcome: failure option,
+ message: string,
+ pool: string Symtab.table,
+ used_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ output: string,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
+ type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
+
+ val kill_atps: unit -> unit
+ val running_atps: unit -> unit
+ val messages: int option -> unit
+ val add_prover: string * prover -> theory -> theory
+ val get_prover: theory -> string -> prover
+ val available_atps: theory -> unit
+ val start_prover_thread :
+ params -> int -> int -> relevance_override -> (string -> minimize_command)
+ -> Proof.state -> string -> unit
+end;
+
+structure ATP_Manager : ATP_MANAGER =
+struct
+
+open Metis_Clauses
+open Sledgehammer_Fact_Filter
+open Sledgehammer_Proof_Reconstruct
+
+(** The Sledgehammer **)
+
+val das_Tool = "Sledgehammer"
+
+fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
+fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
+val messages = Async_Manager.thread_messages das_Tool "ATP"
+
+(** problems, results, provers, etc. **)
+
+type params =
+ {debug: bool,
+ verbose: bool,
+ overlord: bool,
+ atps: string list,
+ full_types: bool,
+ explicit_apply: bool,
+ relevance_threshold: real,
+ relevance_convergence: real,
+ theory_relevant: bool option,
+ defs_relevant: bool,
+ isar_proof: bool,
+ isar_shrink_factor: int,
+ timeout: Time.time,
+ minimize_timeout: Time.time}
+
+type problem =
+ {subgoal: int,
+ goal: Proof.context * (thm list * thm),
+ relevance_override: relevance_override,
+ axiom_clauses: (string * thm) list option,
+ filtered_clauses: (string * thm) list option}
+
+datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | MalformedInput | MalformedOutput | UnknownError
+
+type prover_result =
+ {outcome: failure option,
+ message: string,
+ pool: string Symtab.table,
+ used_thm_names: string list,
+ atp_run_time_in_msecs: int,
+ output: string,
+ proof: string,
+ internal_thm_names: string Vector.vector,
+ conjecture_shape: int list,
+ filtered_clauses: (string * thm) list}
+
+type prover =
+ params -> minimize_command -> Time.time -> problem -> prover_result
+
+(* named provers *)
+
+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 => error ("Duplicate ATP: " ^ quote name ^ ".")
+);
+
+fun add_prover (name, prover) thy =
+ Data.map (Symtab.update_new (name, (prover, stamp ()))) thy
+ handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
+
+fun get_prover thy name =
+ the (Symtab.lookup (Data.get thy) name) |> fst
+ handle Option.Option => error ("Unknown ATP: " ^ name ^ ".")
+
+fun available_atps thy =
+ priority ("Available ATPs: " ^
+ commas (sort_strings (Symtab.keys (Data.get thy))) ^ ".")
+
+
+(* start prover thread *)
+
+fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
+ relevance_override minimize_command proof_state name =
+ let
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, timeout)
+ val prover = get_prover (Proof.theory_of proof_state) name
+ val {context = ctxt, facts, goal} = Proof.goal proof_state;
+ val desc =
+ "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
+ in
+ Async_Manager.launch das_Tool verbose birth_time death_time desc
+ (fn () =>
+ let
+ val problem =
+ {subgoal = i, goal = (ctxt, (facts, goal)),
+ relevance_override = relevance_override, axiom_clauses = NONE,
+ filtered_clauses = NONE}
+ in
+ prover params (minimize_command name) timeout problem |> #message
+ handle ERROR message => "Error: " ^ message ^ "\n"
+ end)
+ end
+
+end;