# HG changeset patch # User wenzelm # Date 1255560929 -7200 # Node ID 34f66c9dd8a2cb0ddfa4929470187336a5964334 # Parent 9491bec2059545152ec5084ac26673ac9b693593 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps; diff -r 9491bec20595 -r 34f66c9dd8a2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Oct 14 23:44:37 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 00:55:29 2009 +0200 @@ -286,8 +286,8 @@ fun get_atp thy args = AList.lookup (op =) args proverK - |> the_default (hd (space_explode " " (ATP_Manager.get_atps ()))) - |> (fn name => (name, the (ATP_Manager.get_prover name thy))) + |> the_default (hd (ATP_Manager.get_atps ())) (* FIXME partial *) + |> (fn name => (name, the (ATP_Manager.get_prover name thy))) (* FIXME partial *) local @@ -301,8 +301,7 @@ val (ctxt, goal) = Proof.get_goal st val ctxt' = if is_none dir then ctxt else Config.put ATP_Wrapper.destdir (the dir) ctxt - val atp = prover (ATP_Wrapper.atp_problem_of_goal - (ATP_Manager.get_full_types ()) 1 (ctxt', goal)) + val atp = prover (ATP_Wrapper.atp_problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal)) val time_limit = (case hard_timeout of @@ -448,7 +447,7 @@ fun invoke args = let - val _ = ATP_Manager.set_full_types (AList.defined (op =) args full_typesK) + val _ = ATP_Manager.full_types := AList.defined (op =) args full_typesK in Mirabelle.register (init, sledgehammer_action args, done) end end diff -r 9491bec20595 -r 34f66c9dd8a2 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Oct 14 23:44:37 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 00:55:29 2009 +0200 @@ -10,14 +10,11 @@ signature ATP_MANAGER = sig - val get_atps: unit -> string - val set_atps: string -> unit - val get_max_atps: unit -> int - val set_max_atps: int -> unit - val get_timeout: unit -> int - val set_timeout: int -> unit - val get_full_types: unit -> bool - val set_full_types: bool -> unit + val atps: string Unsynchronized.ref + val get_atps: unit -> string list + val max_atps: int Unsynchronized.ref + val timeout: int Unsynchronized.ref + val full_types: bool Unsynchronized.ref val kill: unit -> unit val info: unit -> unit val messages: int option -> unit @@ -35,27 +32,13 @@ val message_store_limit = 20; val message_display_limit = 5; -local +val atps = Unsynchronized.ref "e spass remote_vampire"; +fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps); -val atps = Unsynchronized.ref "e spass remote_vampire"; val max_atps = Unsynchronized.ref 5; (* ~1 means infinite number of atps *) val timeout = Unsynchronized.ref 60; val full_types = Unsynchronized.ref false; -in - -fun get_atps () = CRITICAL (fn () => ! atps); -fun set_atps str = CRITICAL (fn () => atps := str); - -fun get_max_atps () = CRITICAL (fn () => ! max_atps); -fun set_max_atps number = CRITICAL (fn () => max_atps := number); - -fun get_timeout () = CRITICAL (fn () => ! timeout); -fun set_timeout time = CRITICAL (fn () => timeout := time); - -fun get_full_types () = CRITICAL (fn () => ! full_types); -fun set_full_types bool = CRITICAL (fn () => full_types := bool); - val _ = ProofGeneralPgip.add_preference Preferences.category_proof (Preferences.string_pref atps @@ -76,8 +59,6 @@ (Preferences.bool_pref full_types "ATP: full types" "ATPs will use full type information"); -end; - (** thread management **) @@ -144,7 +125,7 @@ (* kill excessive atp threads *) fun excessive_atps active = - let val max = get_max_atps () + let val max = ! max_atps in length active > max andalso max > ~1 end; local @@ -337,16 +318,16 @@ val _ = SimpleThread.fork true (fn () => let val _ = register birthtime deadtime (Thread.self (), desc) - val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i - (Proof.get_goal proof_state) + val problem = + ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state) val result = let val ATP_Wrapper.Prover_Result {success, message, ...} = - prover problem (get_timeout ()) + prover problem (! timeout) in (success, message) end - handle ResHolClause.TOO_TRIVIAL - => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis") - | ERROR msg - => (false, "Error: " ^ msg) + handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *) + (true, "Empty clause: Try this command: " ^ + Markup.markup Markup.sendback "apply metis") + | ERROR msg => (false, "Error: " ^ msg) val _ = unregister result (Thread.self ()) in () end handle Interrupt => ()) in () end); @@ -356,11 +337,9 @@ fun sledgehammer names proof_state = let - val provers = - if null names then String.tokens (Symbol.is_ascii_blank o String.str) (get_atps ()) - else names + val provers = if null names then get_atps () else names val birthtime = Time.now () - val deadtime = Time.+ (birthtime, Time.fromSeconds (get_timeout ())) + val deadtime = Time.+ (birthtime, Time.fromSeconds (! timeout)) in List.app (fn name => start_prover name birthtime deadtime 1 proof_state) provers end; diff -r 9491bec20595 -r 34f66c9dd8a2 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Oct 14 23:44:37 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 00:55:29 2009 +0200 @@ -126,7 +126,7 @@ val _ = debug_fn (fn () => print_names name_thm_pairs) val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val problem = ATP_Wrapper.ATP_Problem { - with_full_types = ATP_Manager.get_full_types (), + with_full_types = ! ATP_Manager.full_types, subgoal = subgoalno, goal = Proof.get_goal state, axiom_clauses = SOME axclauses,