# HG changeset patch # User wenzelm # Date 1255621770 -7200 # Node ID e95a4be101a891893421fe85b6ba5e773011dd27 # Parent 3c19b98a35cd04c1008966da72ee3b5299fdcb4f natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system; diff -r 3c19b98a35cd -r e95a4be101a8 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 17:06:19 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 17:49:30 2009 +0200 @@ -301,14 +301,14 @@ 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.full_types) 1 (ctxt', goal)) + val problem = ATP_Wrapper.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', goal); val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) = - time_limit (Mirabelle.cpu_time atp) timeout + time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout in if success then (message, SH_OK (time_isa, time_atp, theorem_names)) else (message, SH_FAIL(time_isa, time_atp)) diff -r 3c19b98a35cd -r e95a4be101a8 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 17:06:19 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 17:49:30 2009 +0200 @@ -323,9 +323,9 @@ let val _ = register birthtime deadtime (Thread.self (), desc); val problem = - ATP_Wrapper.atp_problem_of_goal (! full_types) i (Proof.get_goal proof_state); + ATP_Wrapper.problem_of_goal (! full_types) i (Proof.get_goal proof_state); val result = - let val {success, message, ...} = prover problem (! timeout); + let val {success, message, ...} = prover (! timeout) problem; in (success, message) end handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *) (true, "Empty clause: Try this command: " ^ diff -r 3c19b98a35cd -r e95a4be101a8 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 17:06:19 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 17:49:30 2009 +0200 @@ -110,7 +110,7 @@ goal = Proof.get_goal state, axiom_clauses = SOME axclauses, filtered_clauses = filtered} - val (result, proof) = produce_answer (prover problem time_limit) + val (result, proof) = produce_answer (prover time_limit problem) val _ = priority (string_of_result result) in (result, proof) diff -r 3c19b98a35cd -r e95a4be101a8 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 15 17:06:19 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 15 17:49:30 2009 +0200 @@ -18,13 +18,13 @@ max_new_clauses: int, insert_theory_const: bool, emit_structured_proof: bool} - type atp_problem = + type problem = {with_full_types: bool, subgoal: int, goal: Proof.context * (thm list * thm), axiom_clauses: (thm * (string * int)) list option, filtered_clauses: (thm * (string * int)) list option} - val atp_problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> atp_problem + val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem type prover_result = {success: bool, message: string, @@ -33,7 +33,7 @@ proof: string, internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list} - type prover = atp_problem -> int -> prover_result + type prover = int -> problem -> prover_result (*common provers*) val vampire: string * prover @@ -73,14 +73,14 @@ insert_theory_const: bool, emit_structured_proof: bool}; -type atp_problem = +type problem = {with_full_types: bool, subgoal: int, goal: Proof.context * (thm list * thm), axiom_clauses: (thm * (string * int)) list option, filtered_clauses: (thm * (string * int)) list option}; -fun atp_problem_of_goal with_full_types subgoal goal : atp_problem = +fun problem_of_goal with_full_types subgoal goal : problem = {with_full_types = with_full_types, subgoal = subgoal, goal = goal, @@ -96,7 +96,7 @@ internal_thm_names: string Vector.vector, filtered_clauses: (thm * (string * int)) list}; -type prover = atp_problem -> int -> prover_result; +type prover = int -> problem -> prover_result; (* basic template *) @@ -185,7 +185,7 @@ (* generic TPTP-based provers *) -fun gen_tptp_prover (name, prover_config) problem timeout = +fun gen_tptp_prover (name, prover_config) timeout problem = let val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} = prover_config; @@ -262,7 +262,7 @@ insert_theory_const = insert_theory_const, emit_structured_proof = false}; -fun gen_dfg_prover (name, prover_config: prover_config) problem timeout = +fun gen_dfg_prover (name, prover_config: prover_config) timeout problem = let val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem @@ -306,7 +306,7 @@ (if null systems then get_systems () else systems) |> `(find_first (String.isPrefix prefix))); -fun get_the_system prefix = +fun the_system prefix = (case get_system prefix of NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP") | SOME sys => sys); @@ -314,7 +314,7 @@ fun remote_prover_config prover_prefix args max_new insert_tc: prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = - (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ get_the_system prover_prefix), + (fn timeout => args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix), max_new_clauses = max_new, insert_theory_const = insert_tc, emit_structured_proof = false};