# HG changeset patch # User wenzelm # Date 1255600167 -7200 # Node ID 72d48e333b77d0dfb3547d6b4a6f8d4b1c123392 # Parent 51d450f278ce3db532a00da1bd08356098b1263b eliminated extraneous wrapping of public records; tuned; diff -r 51d450f278ce -r 72d48e333b77 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 11:23:03 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 15 11:49:27 2009 +0200 @@ -307,8 +307,7 @@ (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val (ATP_Wrapper.Prover_Result {success, message, theorem_names, - runtime=time_atp, ...}, time_isa) = + val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) = time_limit (Mirabelle.cpu_time atp) timeout in if success then (message, SH_OK (time_isa, time_atp, theorem_names)) diff -r 51d450f278ce -r 72d48e333b77 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 11:23:03 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Oct 15 11:49:27 2009 +0200 @@ -325,7 +325,7 @@ 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 (! timeout); + let val {success, message, ...} = prover problem (! timeout); in (success, message) end handle ResHolClause.TOO_TRIVIAL => (* FIXME !? *) (true, "Empty clause: Try this command: " ^ diff -r 51d450f278ce -r 72d48e333b77 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 11:23:03 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Oct 15 11:49:27 2009 +0200 @@ -97,10 +97,10 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer result = +fun produce_answer (result: ATP_Wrapper.prover_result) = let - val ATP_Wrapper.Prover_Result {success, message, proof=result_string, - internal_thm_names=thm_name_vec, filtered_clauses=filtered, ...} = result + val {success, message, proof = result_string, + internal_thm_names = thm_name_vec, filtered_clauses = filtered, ...} = result in if success then (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string) @@ -125,12 +125,12 @@ 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 = ATP_Wrapper.ATP_Problem { - with_full_types = ! ATP_Manager.full_types, + val problem = + {with_full_types = ! ATP_Manager.full_types, subgoal = subgoalno, goal = Proof.get_goal state, axiom_clauses = SOME axclauses, - filtered_clauses = filtered } + filtered_clauses = filtered} val (result, proof) = produce_answer (prover problem time_limit) val _ = println (string_of_result result) val _ = debug proof diff -r 51d450f278ce -r 72d48e333b77 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 15 11:23:03 2009 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Oct 15 11:49:27 2009 +0200 @@ -12,28 +12,27 @@ val setup: theory -> theory (*prover configuration, problem format, and prover result*) - datatype prover_config = Prover_Config of { - command: Path.T, + type prover_config = + {command: Path.T, arguments: int -> string, max_new_clauses: int, insert_theory_const: bool, - emit_structured_proof: bool } - datatype atp_problem = ATP_Problem of { - with_full_types: bool, + emit_structured_proof: bool} + type atp_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 - datatype prover_result = Prover_Result of { - success: bool, + filtered_clauses: (thm * (string * int)) list option} + val atp_problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> atp_problem + type prover_result = + {success: bool, message: string, theorem_names: string list, runtime: int, proof: string, internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list } + filtered_clauses: (thm * (string * int)) list} type prover = atp_problem -> int -> prover_result (*common provers*) @@ -67,37 +66,37 @@ (* prover configuration, problem format, and prover result *) -datatype prover_config = Prover_Config of { - command: Path.T, +type prover_config = + {command: Path.T, arguments: int -> string, max_new_clauses: int, insert_theory_const: bool, - emit_structured_proof: bool } + emit_structured_proof: bool}; -datatype atp_problem = ATP_Problem of { - with_full_types: bool, +type atp_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 } + filtered_clauses: (thm * (string * int)) list option}; -fun atp_problem_of_goal with_full_types subgoal goal = ATP_Problem { - with_full_types = with_full_types, +fun atp_problem_of_goal with_full_types subgoal goal : atp_problem = + {with_full_types = with_full_types, subgoal = subgoal, goal = goal, axiom_clauses = NONE, - filtered_clauses = NONE } + filtered_clauses = NONE}; -datatype prover_result = Prover_Result of { - success: bool, +type prover_result = + {success: bool, message: string, - theorem_names: string list, (* relevant theorems *) - runtime: int, (* user time of the ATP, in milliseconds *) + theorem_names: string list, (*relevant theorems*) + runtime: int, (*user time of the ATP, in milliseconds*) proof: string, internal_thm_names: string Vector.vector, - filtered_clauses: (thm * (string * int)) list } + filtered_clauses: (thm * (string * int)) list}; -type prover = atp_problem -> int -> prover_result +type prover = atp_problem -> int -> prover_result; (* basic template *) @@ -106,7 +105,7 @@ Exn.capture f path |> tap (fn _ => cleanup path) |> Exn.release - |> tap (after path) + |> tap (after path); fun external_prover relevance_filter preparer writer cmd args find_failure produce_answer axiom_clauses filtered_clauses name subgoalno goal = @@ -178,9 +177,9 @@ (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)) val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof) in - Prover_Result {success=success, message=message, - theorem_names=real_thm_names, runtime=time, proof=proof, - internal_thm_names = thm_names, filtered_clauses=the_filtered_clauses} + {success = success, message = message, + theorem_names = real_thm_names, runtime = time, proof = proof, + internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses} end @@ -188,10 +187,9 @@ fun gen_tptp_prover (name, prover_config) problem timeout = let - val Prover_Config {max_new_clauses, insert_theory_const, - emit_structured_proof, command, arguments} = prover_config - val ATP_Problem {with_full_types, subgoal, goal, axiom_clauses, - filtered_clauses} = problem + val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} = + prover_config + val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem in external_prover (ResAtp.get_relevant max_new_clauses insert_theory_const) @@ -201,7 +199,7 @@ (arguments timeout) ResReconstruct.find_failure (if emit_structured_proof then ResReconstruct.structured_proof - else ResReconstruct.lemma_list false) + else ResReconstruct.lemma_list false) axiom_clauses filtered_clauses name @@ -212,6 +210,7 @@ fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config)) + (** common provers **) (* Vampire *) @@ -221,13 +220,13 @@ val vampire_max_new_clauses = 60 val vampire_insert_theory_const = false -fun vampire_prover_config full = Prover_Config { - command = Path.explode "$VAMPIRE_HOME/vampire", +fun vampire_prover_config full : prover_config = + {command = Path.explode "$VAMPIRE_HOME/vampire", arguments = (fn timeout => "--output_syntax tptp --mode casc" ^ " -t " ^ string_of_int timeout), max_new_clauses = vampire_max_new_clauses, insert_theory_const = vampire_insert_theory_const, - emit_structured_proof = full } + emit_structured_proof = full} val vampire = tptp_prover ("vampire", vampire_prover_config false) val vampire_full = tptp_prover ("vampire_full", vampire_prover_config true) @@ -238,13 +237,13 @@ val eprover_max_new_clauses = 100 val eprover_insert_theory_const = false -fun eprover_config full = Prover_Config { - command = Path.explode "$E_HOME/eproof", +fun eprover_config full : prover_config = + {command = Path.explode "$E_HOME/eproof", arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^ " --silent --cpu-limit=" ^ string_of_int timeout), max_new_clauses = eprover_max_new_clauses, insert_theory_const = eprover_insert_theory_const, - emit_structured_proof = full } + emit_structured_proof = full} val eprover = tptp_prover ("e", eprover_config false) val eprover_full = tptp_prover ("e_full", eprover_config true) @@ -255,20 +254,19 @@ val spass_max_new_clauses = 40 val spass_insert_theory_const = true -fun spass_config insert_theory_const = Prover_Config { - command = Path.explode "$SPASS_HOME/SPASS", +fun spass_config insert_theory_const: prover_config = + {command = Path.explode "$SPASS_HOME/SPASS", arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout), max_new_clauses = spass_max_new_clauses, insert_theory_const = insert_theory_const, - emit_structured_proof = false } + emit_structured_proof = false} fun gen_dfg_prover (name, prover_config) problem timeout = let - val Prover_Config {max_new_clauses, insert_theory_const, - emit_structured_proof, command, arguments} = prover_config - val ATP_Problem {with_full_types, subgoal, goal, axiom_clauses, - filtered_clauses} = problem + val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} = + prover_config + val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem in external_prover (ResAtp.get_relevant max_new_clauses insert_theory_const) @@ -316,13 +314,13 @@ NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP") | SOME sys => sys) -fun remote_prover_config prover_prefix args max_new insert_tc = Prover_Config { - command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", +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), max_new_clauses = max_new, insert_theory_const = insert_tc, - emit_structured_proof = false } + emit_structured_proof = false} val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const)