# HG changeset patch # User wenzelm # Date 1255556677 -7200 # Node ID 9491bec2059545152ec5084ac26673ac9b693593 # Parent 2218b970325aafad0fc8f1e3ea2ee90db982dab1 modernized structure names; diff -r 2218b970325a -r 9491bec20595 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Wed Oct 14 23:13:38 2009 +0200 +++ b/src/HOL/ATP_Linkup.thy Wed Oct 14 23:44:37 2009 +0200 @@ -96,26 +96,26 @@ use "Tools/res_reconstruct.ML" setup ResReconstruct.setup use "Tools/res_atp.ML" -use "Tools/ATP_Manager/atp_wrapper.ML" setup AtpWrapper.setup +use "Tools/ATP_Manager/atp_wrapper.ML" setup ATP_Wrapper.setup use "Tools/ATP_Manager/atp_manager.ML" use "Tools/ATP_Manager/atp_minimal.ML" text {* basic provers *} -setup {* AtpManager.add_prover AtpWrapper.spass *} -setup {* AtpManager.add_prover AtpWrapper.vampire *} -setup {* AtpManager.add_prover AtpWrapper.eprover *} +setup {* ATP_Manager.add_prover ATP_Wrapper.spass *} +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire *} +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover *} text {* provers with stuctured output *} -setup {* AtpManager.add_prover AtpWrapper.vampire_full *} -setup {* AtpManager.add_prover AtpWrapper.eprover_full *} +setup {* ATP_Manager.add_prover ATP_Wrapper.vampire_full *} +setup {* ATP_Manager.add_prover ATP_Wrapper.eprover_full *} text {* on some problems better results *} -setup {* AtpManager.add_prover AtpWrapper.spass_no_tc *} +setup {* ATP_Manager.add_prover ATP_Wrapper.spass_no_tc *} text {* remote provers via SystemOnTPTP *} -setup {* AtpManager.add_prover AtpWrapper.remote_vampire *} -setup {* AtpManager.add_prover AtpWrapper.remote_spass *} -setup {* AtpManager.add_prover AtpWrapper.remote_eprover *} +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_vampire *} +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *} +setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *} diff -r 2218b970325a -r 9491bec20595 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Oct 14 23:13:38 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Oct 14 23:44:37 2009 +0200 @@ -286,8 +286,8 @@ fun get_atp thy args = AList.lookup (op =) args proverK - |> the_default (hd (space_explode " " (AtpManager.get_atps ()))) - |> (fn name => (name, the (AtpManager.get_prover name thy))) + |> the_default (hd (space_explode " " (ATP_Manager.get_atps ()))) + |> (fn name => (name, the (ATP_Manager.get_prover name thy))) local @@ -300,15 +300,15 @@ let val (ctxt, goal) = Proof.get_goal st val ctxt' = if is_none dir then ctxt - else Config.put AtpWrapper.destdir (the dir) ctxt - val atp = prover (AtpWrapper.atp_problem_of_goal - (AtpManager.get_full_types ()) 1 (ctxt', goal)) + 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 time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val (AtpWrapper.Prover_Result {success, message, theorem_names, + val (ATP_Wrapper.Prover_Result {success, message, theorem_names, runtime=time_atp, ...}, time_isa) = time_limit (Mirabelle.cpu_time atp) timeout in @@ -372,7 +372,7 @@ let val n0 = length (these (!named_thms)) val (prover_name, prover) = get_atp (Proof.theory_of st) args - val minimize = AtpMinimal.minimalize prover prover_name + val minimize = ATP_Minimal.minimalize prover prover_name val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) @@ -448,7 +448,7 @@ fun invoke args = let - val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK) + val _ = ATP_Manager.set_full_types (AList.defined (op =) args full_typesK) in Mirabelle.register (init, sledgehammer_action args, done) end end diff -r 2218b970325a -r 9491bec20595 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Oct 14 23:13:38 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Oct 14 23:44:37 2009 +0200 @@ -21,13 +21,13 @@ val kill: unit -> unit val info: unit -> unit val messages: int option -> unit - val add_prover: string * AtpWrapper.prover -> theory -> theory + val add_prover: string * ATP_Wrapper.prover -> theory -> theory val print_provers: theory -> unit - val get_prover: string -> theory -> AtpWrapper.prover option + val get_prover: string -> theory -> ATP_Wrapper.prover option val sledgehammer: string list -> Proof.state -> unit end; -structure AtpManager: ATP_MANAGER = +structure ATP_Manager: ATP_MANAGER = struct (** preferences **) @@ -302,7 +302,7 @@ structure Provers = TheoryDataFun ( - type T = (AtpWrapper.prover * stamp) Symtab.table + type T = (ATP_Wrapper.prover * stamp) Symtab.table val empty = Symtab.empty val copy = I val extend = I @@ -337,10 +337,10 @@ val _ = SimpleThread.fork true (fn () => let val _ = register birthtime deadtime (Thread.self (), desc) - val problem = AtpWrapper.atp_problem_of_goal (get_full_types ()) i + val problem = ATP_Wrapper.atp_problem_of_goal (get_full_types ()) i (Proof.get_goal proof_state) val result = - let val AtpWrapper.Prover_Result {success, message, ...} = + let val ATP_Wrapper.Prover_Result {success, message, ...} = prover problem (get_timeout ()) in (success, message) end handle ResHolClause.TOO_TRIVIAL diff -r 2218b970325a -r 9491bec20595 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Oct 14 23:13:38 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Oct 14 23:44:37 2009 +0200 @@ -6,11 +6,11 @@ signature ATP_MINIMAL = sig - val minimalize: AtpWrapper.prover -> string -> int -> Proof.state -> + val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state -> (string * thm list) list -> ((string * thm list) list * int) option * string end -structure AtpMinimal: ATP_MINIMAL = +structure ATP_Minimal: ATP_MINIMAL = struct (* output control *) @@ -99,7 +99,7 @@ fun produce_answer result = let - val AtpWrapper.Prover_Result {success, message, proof=result_string, + val ATP_Wrapper.Prover_Result {success, message, proof=result_string, internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result in if success then @@ -116,6 +116,7 @@ end end + (* wrapper for calling external prover *) fun sh_test_thms prover time_limit subgoalno state filtered name_thms_pairs = @@ -124,8 +125,8 @@ val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val _ = debug_fn (fn () => print_names name_thm_pairs) val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs - val problem = AtpWrapper.ATP_Problem { - with_full_types = AtpManager.get_full_types (), + val problem = ATP_Wrapper.ATP_Problem { + with_full_types = ATP_Manager.get_full_types (), subgoal = subgoalno, goal = Proof.get_goal state, axiom_clauses = SOME axclauses, @@ -224,7 +225,7 @@ let val (prover_name, time_limit) = get_options args val prover = - case AtpManager.get_prover prover_name (Proof.theory_of state) of + case ATP_Manager.get_prover prover_name (Proof.theory_of state) of SOME prover => prover | NONE => error ("Unknown prover: " ^ quote prover_name) val name_thms_pairs = get_thms (Proof.context_of state) thm_names diff -r 2218b970325a -r 9491bec20595 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Oct 14 23:13:38 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Oct 14 23:44:37 2009 +0200 @@ -49,7 +49,7 @@ val refresh_systems: unit -> unit end; -structure AtpWrapper: ATP_WRAPPER = +structure ATP_Wrapper: ATP_WRAPPER = struct (** generic ATP wrapper **)