# HG changeset patch # User blanchet # Date 1269536191 -3600 # Node ID 142c3784a42b26674292417f404e9972b24d0c51 # Parent b88e061754a1c65b7858c678b7a2614adaac5ee6# Parent 4f24a4e9af4a0f7d56271596b39896d78af3f09a merged diff -r b88e061754a1 -r 142c3784a42b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/IsaMakefile Thu Mar 25 17:56:31 2010 +0100 @@ -322,6 +322,7 @@ Tools/Sledgehammer/sledgehammer_hol_clause.ML \ Tools/Sledgehammer/sledgehammer_isar.ML \ Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \ + Tools/Sledgehammer/sledgehammer_util.ML \ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ diff -r b88e061754a1 -r 142c3784a42b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 25 17:56:31 2010 +0100 @@ -280,7 +280,8 @@ fun get_atp thy args = let - fun default_atp_name () = hd (ATP_Manager.get_atps ()) + fun default_atp_name () = + hd (#atps (Sledgehammer_Isar.default_params thy [])) handle Empty => error "No ATP available." fun get_prover name = (case ATP_Manager.get_prover thy name of @@ -302,22 +303,28 @@ fun run_sh prover hard_timeout timeout dir st = let val {context = ctxt, facts, goal} = Proof.goal st + val thy = ProofContext.theory_of ctxt val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I) val ctxt' = ctxt |> change_dir dir |> Config.put ATP_Wrapper.measure_runtime true - val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal)); - + val params = Sledgehammer_Isar.default_params thy [] + val problem = + {subgoal = 1, goal = (ctxt', (facts, goal)), + relevance_override = {add = [], del = [], only = false}, + axiom_clauses = NONE, filtered_clauses = NONE} val time_limit = (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result, - time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout + val ({success, message, relevant_thm_names, + atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result, + time_isa) = time_limit (Mirabelle.cpu_time + (prover params (Time.fromSeconds timeout))) problem in - if success then (message, SH_OK (time_isa, time_atp, theorem_names)) - else (message, SH_FAIL(time_isa, time_atp)) + if success then (message, SH_OK (time_isa, time_atp, relevant_thm_names)) + else (message, SH_FAIL (time_isa, time_atp)) end handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, [])) | ERROR msg => ("error: " ^ msg, SH_ERROR) @@ -375,16 +382,19 @@ fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) = let open ATP_Minimal + open Sledgehammer_Isar + val thy = Proof.theory_of st val n0 = length (these (!named_thms)) - val (prover_name, prover) = get_atp (Proof.theory_of st) args - val minimize = minimize_theorems linear_minimize prover prover_name + val (prover_name, prover) = get_atp thy args val timeout = AList.lookup (op =) args minimize_timeoutK |> Option.map (fst o read_int o explode) |> the_default 5 + val params = default_params thy [("minimize_timeout", Int.toString timeout)] + val minimize = minimize_theorems params linear_minimize prover prover_name val _ = log separator in - case minimize timeout st (these (!named_thms)) of + case minimize st (these (!named_thms)) of (SOME named_thms', msg) => (change_data id inc_min_succs; change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0)); diff -r b88e061754a1 -r 142c3784a42b src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Sledgehammer.thy Thu Mar 25 17:56:31 2010 +0100 @@ -12,6 +12,7 @@ uses "Tools/polyhash.ML" "~~/src/Tools/Metis/metis.ML" + "Tools/Sledgehammer/sledgehammer_util.ML" ("Tools/Sledgehammer/sledgehammer_fol_clause.ML") ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML") ("Tools/Sledgehammer/sledgehammer_hol_clause.ML") diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Mar 25 17:56:31 2010 +0100 @@ -1,71 +1,92 @@ (* 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 params = + {debug: bool, + verbose: bool, + atps: string list, + full_types: bool, + relevance_threshold: real, + higher_order: bool option, + respect_no_atp: bool, + follow_defs: bool, + isar_proof: bool, + timeout: Time.time, + minimize_timeout: Time.time} 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 problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option} 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} - type prover = int -> problem -> prover_result + {success: bool, + message: string, + relevant_thm_names: string list, + atp_run_time_in_msecs: int, + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list} + type prover = params -> Time.time -> problem -> prover_result val atps: string Unsynchronized.ref - val get_atps: unit -> string list val timeout: int Unsynchronized.ref val full_types: bool Unsynchronized.ref - val kill: unit -> unit - val info: unit -> unit + 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 option - val print_provers: theory -> unit - val sledgehammer: string list -> Proof.state -> unit + val available_atps: theory -> unit + val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit end; structure ATP_Manager : ATP_MANAGER = struct -(** problems, results, and provers **) +type relevance_override = Sledgehammer_Fact_Filter.relevance_override + +(** parameters, problems, results, and provers **) + +(* TODO: "theory_const", "blacklist_filter", "convergence" *) +type params = + {debug: bool, + verbose: bool, + atps: string list, + full_types: bool, + relevance_threshold: real, + higher_order: bool option, + respect_no_atp: bool, + follow_defs: bool, + isar_proof: bool, + timeout: Time.time, + minimize_timeout: Time.time} 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 problem_of_goal with_full_types subgoal goal : problem = - {with_full_types = with_full_types, - subgoal = subgoal, - goal = goal, - axiom_clauses = NONE, - filtered_clauses = NONE}; + {subgoal: int, + goal: Proof.context * (thm list * thm), + relevance_override: relevance_override, + axiom_clauses: (thm * (string * int)) list option, + filtered_clauses: (thm * (string * int)) list option}; type prover_result = - {success: bool, - message: string, - 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}; + {success: bool, + message: string, + relevant_thm_names: string list, + atp_run_time_in_msecs: int, + proof: string, + internal_thm_names: string Vector.vector, + filtered_clauses: (thm * (string * int)) list}; -type prover = int -> problem -> prover_result; +type prover = params -> Time.time -> problem -> prover_result; (** preferences **) @@ -74,8 +95,6 @@ val message_display_limit = 5; val atps = Unsynchronized.ref "e spass remote_vampire"; -fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps); - val timeout = Unsynchronized.ref 60; val full_types = Unsynchronized.ref false; @@ -218,9 +237,9 @@ (** user commands **) -(* kill *) +(* kill ATPs *) -fun kill () = Synchronized.change global_state +fun kill_atps () = Synchronized.change global_state (fn {manager, timeout_heap, active, cancelling, messages, store} => let val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active; @@ -228,11 +247,11 @@ in state' end); -(* info *) +(* running_atps *) fun seconds time = string_of_int (Time.toSeconds time) ^ "s"; -fun info () = +fun running_atps () = let val {active, cancelling, ...} = Synchronized.value global_state; @@ -287,44 +306,51 @@ fun get_prover thy name = Option.map #1 (Symtab.lookup (Provers.get thy) name); -fun print_provers thy = Pretty.writeln - (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy)))); +fun available_atps thy = Pretty.writeln + (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy)))); (* start prover thread *) -fun start_prover name birth_time death_time i proof_state = +fun start_prover (params as {timeout, ...}) birth_time death_time i + relevance_override proof_state name = (case get_prover (Proof.theory_of proof_state) name of - NONE => warning ("Unknown external prover: " ^ quote name) + NONE => warning ("Unknown ATP: " ^ quote name) | SOME prover => let val {context = ctxt, facts, goal} = Proof.goal proof_state; val desc = - "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ + "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); val _ = Toplevel.thread true (fn () => let val _ = register birth_time death_time (Thread.self (), desc); - val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal)); - val message = #message (prover (! timeout) problem) + val problem = + {subgoal = i, goal = (ctxt, (facts, goal)), + relevance_override = relevance_override, axiom_clauses = NONE, + filtered_clauses = NONE} + val message = #message (prover params timeout problem) handle Sledgehammer_HOL_Clause.TRIVIAL => (* FIXME !? *) - "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis" + "Try this command: " ^ + Markup.markup Markup.sendback "by metis" ^ "." | ERROR msg => ("Error: " ^ msg); val _ = unregister message (Thread.self ()); in () end); in () end); -(* sledghammer for first subgoal *) +(* Sledgehammer the given subgoal *) -fun sledgehammer names proof_state = +fun sledgehammer (params as {atps, timeout, ...}) i relevance_override + proof_state = let - val provers = if null names then get_atps () else names; - val birth_time = Time.now (); - val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout)); - val _ = kill (); (*RACE wrt. other invocations of sledgehammer*) - val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers; - in () end; + val birth_time = Time.now () + val death_time = Time.+ (birth_time, timeout) + val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *) + val _ = priority "Sledgehammering..." + val _ = List.app (start_prover params birth_time death_time i + relevance_override proof_state) atps + in () end end; diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Thu Mar 25 17:56:31 2010 +0100 @@ -6,6 +6,7 @@ signature ATP_MINIMAL = sig + type params = ATP_Manager.params type prover = ATP_Manager.prover type prover_result = ATP_Manager.prover_result type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list @@ -13,7 +14,7 @@ val linear_minimize : 'a minimize_fun val binary_minimize : 'a minimize_fun val minimize_theorems : - (string * thm list) minimize_fun -> prover -> string -> int + params -> (string * thm list) minimize_fun -> prover -> string -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -109,8 +110,8 @@ (* wrapper for calling external prover *) -fun sledgehammer_test_theorems prover time_limit subgoalno state filtered - name_thms_pairs = +fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover + timeout subgoalno state filtered name_thms_pairs = let val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") @@ -118,26 +119,26 @@ val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = - {with_full_types = ! ATP_Manager.full_types, - subgoal = subgoalno, - goal = (ctxt, (facts, goal)), - axiom_clauses = SOME axclauses, - filtered_clauses = filtered} - val (result, proof) = produce_answer (prover time_limit problem) + {subgoal = subgoalno, goal = (ctxt, (facts, goal)), + relevance_override = {add = [], del = [], only = false}, + axiom_clauses = SOME axclauses, filtered_clauses = filtered} + val (result, proof) = produce_answer (prover params timeout problem) val _ = priority (string_of_result result) in (result, proof) end (* minimalization of thms *) -fun minimize_theorems gen_min prover prover_name time_limit state - name_thms_pairs = +fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover + prover_name state name_thms_pairs = let + val msecs = Time.toMilliseconds minimize_timeout val _ = priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ - " theorems, prover: " ^ prover_name ^ - ", time limit: " ^ string_of_int time_limit ^ " seconds") - val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state + " theorems, ATP: " ^ prover_name ^ + ", time limit: " ^ string_of_int msecs ^ " ms") + val test_thms_fun = + sledgehammer_test_theorems params prover minimize_timeout 1 state fun test_thms filtered thms = case test_thms_fun filtered thms of (Success _, _) => true | _ => false in @@ -157,18 +158,22 @@ val _ = priority (cat_lines ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in - (SOME min_thms, "Try this command: " ^ - Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")")) + (SOME min_thms, + "Try this command: " ^ + Markup.markup Markup.sendback + ("by (metis " ^ space_implode " " min_names ^ ")") + ^ ".") end | (Timeout, _) => (NONE, "Timeout: You may need to increase the time limit of " ^ - string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ") + string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".") | (Error, msg) => (NONE, "Error in prover: " ^ msg) | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) handle Sledgehammer_HOL_Clause.TRIVIAL => - (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") + (SOME [], "Trivial: Try this command: " ^ + Markup.markup Markup.sendback "by metis" ^ ".") | ERROR msg => (NONE, "Error: " ^ msg) end diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Mar 25 17:56:31 2010 +0100 @@ -20,6 +20,7 @@ structure ATP_Wrapper : ATP_WRAPPER = struct +open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct @@ -43,11 +44,11 @@ type prover_config = {command: Path.T, - arguments: int -> string, + arguments: Time.time -> string, failure_strs: string list, max_new_clauses: int, - insert_theory_const: bool, - emit_structured_proof: bool}; + add_theory_const: bool, + supports_isar_proofs: bool}; (* basic template *) @@ -64,24 +65,25 @@ else SOME "Ill-formed ATP output" | (failure :: _) => SOME failure -fun external_prover relevance_filter prepare write cmd args failure_strs - produce_answer name ({with_full_types, subgoal, goal, axiom_clauses, - filtered_clauses}: problem) = +fun generic_prover get_facts prepare write cmd args failure_strs produce_answer + name ({full_types, ...} : params) + ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} + : problem) = let (* get clauses and prepare them for writing *) val (ctxt, (chain_ths, th)) = goal; val thy = ProofContext.theory_of ctxt; val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; - val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal); + val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal); val the_filtered_clauses = (case filtered_clauses of - NONE => relevance_filter goal goal_cls + NONE => get_facts relevance_override goal goal_cls | SOME fcls => fcls); val the_axiom_clauses = (case axiom_clauses of NONE => the_filtered_clauses | SOME axcls => axcls); - val (thm_names, clauses) = + val (internal_thm_names, clauses) = prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; (* path to unique problem file *) @@ -121,7 +123,7 @@ if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists cmd then - write with_full_types probfile clauses + write full_types probfile clauses |> pair (apfst split_time' (bash_output (cmd_line probfile))) else error ("Bad executable: " ^ Path.implode cmd); @@ -131,21 +133,24 @@ if destdir' = "" then () else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof; - val (((proof, time), rc), conj_pos) = + val (((proof, atp_run_time_in_msecs), rc), conj_pos) = with_path cleanup export run_on (prob_pathname subgoal); (* check for success and print out some information on failure *) val failure = find_failure failure_strs proof; val success = rc = 0 andalso is_none failure; - val (message, real_thm_names) = + val (message, relevant_thm_names) = if is_some failure then ("External prover failed.", []) else if rc <> 0 then ("External prover failed: " ^ proof, []) - else apfst (fn s => "Try this command: " ^ s) - (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal)); + else + (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, + subgoal)); in {success = success, message = message, - theorem_names = real_thm_names, runtime = time, proof = proof, - internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses} + relevant_thm_names = relevant_thm_names, + atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, + internal_thm_names = internal_thm_names, + filtered_clauses = the_filtered_clauses} end; @@ -153,96 +158,87 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, - insert_theory_const, emit_structured_proof}) timeout = - external_prover (get_relevant_facts max_new_clauses insert_theory_const) - (prepare_clauses false) write_tptp_file command (arguments timeout) - failure_strs - (if emit_structured_proof then structured_isar_proof - else metis_lemma_list false) name; + add_theory_const, supports_isar_proofs}) + (params as {relevance_threshold, higher_order, follow_defs, isar_proof, + ...}) timeout = + generic_prover + (get_relevant_facts relevance_threshold higher_order follow_defs + max_new_clauses add_theory_const) + (prepare_clauses higher_order false) write_tptp_file command + (arguments timeout) failure_strs + (if supports_isar_proofs andalso isar_proof then structured_isar_proof + else metis_lemma_list false) name params; -fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p)); +fun tptp_prover name p = (name, generic_tptp_prover (name, p)); (** common provers **) (* Vampire *) -(*NB: Vampire does not work without explicit timelimit*) - -val vampire_failure_strs = - ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; -val vampire_max_new_clauses = 60; -val vampire_insert_theory_const = false; +(* NB: Vampire does not work without explicit time limit. *) -fun vampire_prover_config isar : prover_config = - {command = Path.explode "$VAMPIRE_HOME/vampire", - arguments = (fn timeout => "--output_syntax tptp --mode casc" ^ - " -t " ^ string_of_int timeout), - failure_strs = vampire_failure_strs, - max_new_clauses = vampire_max_new_clauses, - insert_theory_const = vampire_insert_theory_const, - emit_structured_proof = isar}; - -val vampire = tptp_prover ("vampire", vampire_prover_config false); -val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true); +val vampire_config : prover_config = + {command = Path.explode "$VAMPIRE_HOME/vampire", + arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ + string_of_int (Time.toSeconds timeout)), + failure_strs = + ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], + max_new_clauses = 60, + add_theory_const = false, + supports_isar_proofs = true} +val vampire = tptp_prover "vampire" vampire_config (* E prover *) -val eprover_failure_strs = - ["SZS status: Satisfiable", "SZS status Satisfiable", - "SZS status: ResourceOut", "SZS status ResourceOut", - "# Cannot determine problem status"]; -val eprover_max_new_clauses = 100; -val eprover_insert_theory_const = false; - -fun eprover_config isar : 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), - failure_strs = eprover_failure_strs, - max_new_clauses = eprover_max_new_clauses, - insert_theory_const = eprover_insert_theory_const, - emit_structured_proof = isar}; - -val eprover = tptp_prover ("e", eprover_config false); -val eprover_isar = tptp_prover ("e_isar", eprover_config true); +val e_config : prover_config = + {command = Path.explode "$E_HOME/eproof", + arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ + \-tAutoDev --silent --cpu-limit=" ^ + string_of_int (Time.toSeconds timeout)), + failure_strs = + ["SZS status: Satisfiable", "SZS status Satisfiable", + "SZS status: ResourceOut", "SZS status ResourceOut", + "# Cannot determine problem status"], + max_new_clauses = 100, + add_theory_const = false, + supports_isar_proofs = true} +val e = tptp_prover "e" e_config (* SPASS *) -val spass_failure_strs = - ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", - "SPASS beiseite: Maximal number of loops exceeded."]; -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", - arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ - " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout), - failure_strs = spass_failure_strs, - max_new_clauses = spass_max_new_clauses, - insert_theory_const = insert_theory_const, - emit_structured_proof = false}; - fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, - insert_theory_const, ...} : prover_config)) timeout = - external_prover - (get_relevant_facts max_new_clauses insert_theory_const) - (prepare_clauses true) - write_dfg_file - command - (arguments timeout) - failure_strs - (metis_lemma_list true) - name; + add_theory_const, ...} : prover_config)) + (params as {relevance_threshold, higher_order, follow_defs, ...}) + timeout = + generic_prover + (get_relevant_facts relevance_threshold higher_order follow_defs + max_new_clauses add_theory_const) + (prepare_clauses higher_order true) write_dfg_file command + (arguments timeout) failure_strs (metis_lemma_list true) name params; fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); -val spass = dfg_prover ("spass", spass_config spass_insert_theory_const); -val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false); +fun spass_config_for add_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 (Time.toSeconds timeout)), + failure_strs = + ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", + "SPASS beiseite: Maximal number of loops exceeded."], + max_new_clauses = 40, + add_theory_const = add_theory_const, + supports_isar_proofs = false}; + +val spass_config = spass_config_for true +val spass = dfg_prover ("spass", spass_config) + +val spass_no_tc_config = spass_config_for false +val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config) (* remote prover invocation via SystemOnTPTP *) @@ -251,10 +247,12 @@ fun get_systems () = let - val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w") + val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w" in - if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) - else split_lines answer + if rc <> 0 then + error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) + else + split_lines answer end; fun refresh_systems_on_tptp () = @@ -271,27 +269,34 @@ val remote_failure_strs = ["Remote-script could not extract proof"]; -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 " ^ the_system prover_prefix), - failure_strs = remote_failure_strs, - max_new_clauses = max_new, - insert_theory_const = insert_tc, - emit_structured_proof = false}; +fun remote_prover_config prover_prefix args max_new_clauses add_theory_const + : prover_config = + {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", + arguments = (fn timeout => + args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^ + the_system prover_prefix), + failure_strs = remote_failure_strs, + max_new_clauses = max_new_clauses, + add_theory_const = add_theory_const, + supports_isar_proofs = false} -val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config - "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const); +val remote_vampire = + tptp_prover "remote_vampire" + (remote_prover_config "Vampire---9" "" + (#max_new_clauses vampire_config) (#add_theory_const vampire_config)) -val remote_eprover = tptp_prover ("remote_e", remote_prover_config - "EP---" "" eprover_max_new_clauses eprover_insert_theory_const); +val remote_e = + tptp_prover "remote_e" + (remote_prover_config "EP---" "" + (#max_new_clauses e_config) (#add_theory_const e_config)) -val remote_spass = tptp_prover ("remote_spass", remote_prover_config - "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const); +val remote_spass = + tptp_prover "remote_spass" + (remote_prover_config "SPASS---" "-x" + (#max_new_clauses spass_config) (#add_theory_const spass_config)) val provers = - [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc, - remote_vampire, remote_spass, remote_eprover] + [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e] val prover_setup = fold add_prover provers val setup = diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Mar 25 17:56:31 2010 +0100 @@ -346,7 +346,7 @@ fun monotonicity_message Ts extra = let val ss = map (quote o string_for_type ctxt) Ts in "The type" ^ plural_s_for_list ss ^ " " ^ - space_implode " " (serial_commas "and" ss) ^ " " ^ + space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^ (if none_true monos then "passed the monotonicity test" else @@ -684,7 +684,8 @@ options in print ("Try again with " ^ - space_implode " " (serial_commas "and" ss) ^ + space_implode " " + (Sledgehammer_Util.serial_commas "and" ss) ^ " to confirm that the " ^ das_wort_model ^ " is genuine.") end diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Mar 25 17:56:31 2010 +0100 @@ -24,6 +24,8 @@ open Nitpick_Nut open Nitpick +structure K = OuterKeyword and P = OuterParse + val auto = Unsynchronized.ref false; val _ = @@ -34,48 +36,48 @@ type raw_param = string * string list val default_default_params = - [("card", ["1\8"]), - ("iter", ["0,1,2,4,8,12,16,24"]), - ("bits", ["1,2,3,4,6,8,10,12"]), - ("bisim_depth", ["7"]), - ("box", ["smart"]), - ("finitize", ["smart"]), - ("mono", ["smart"]), - ("std", ["true"]), - ("wf", ["smart"]), - ("sat_solver", ["smart"]), - ("batch_size", ["smart"]), - ("blocking", ["true"]), - ("falsify", ["true"]), - ("user_axioms", ["smart"]), - ("assms", ["true"]), - ("merge_type_vars", ["false"]), - ("binary_ints", ["smart"]), - ("destroy_constrs", ["true"]), - ("specialize", ["true"]), - ("skolemize", ["true"]), - ("star_linear_preds", ["true"]), - ("uncurry", ["true"]), - ("fast_descrs", ["true"]), - ("peephole_optim", ["true"]), - ("timeout", ["30 s"]), - ("tac_timeout", ["500 ms"]), - ("sym_break", ["20"]), - ("sharing_depth", ["3"]), - ("flatten_props", ["false"]), - ("max_threads", ["0"]), - ("verbose", ["false"]), - ("debug", ["false"]), - ("overlord", ["false"]), - ("show_all", ["false"]), - ("show_skolems", ["true"]), - ("show_datatypes", ["false"]), - ("show_consts", ["false"]), - ("format", ["1"]), - ("max_potential", ["1"]), - ("max_genuine", ["1"]), - ("check_potential", ["false"]), - ("check_genuine", ["false"])] + [("card", "1\8"), + ("iter", "0,1,2,4,8,12,16,24"), + ("bits", "1,2,3,4,6,8,10,12"), + ("bisim_depth", "7"), + ("box", "smart"), + ("finitize", "smart"), + ("mono", "smart"), + ("std", "true"), + ("wf", "smart"), + ("sat_solver", "smart"), + ("batch_size", "smart"), + ("blocking", "true"), + ("falsify", "true"), + ("user_axioms", "smart"), + ("assms", "true"), + ("merge_type_vars", "false"), + ("binary_ints", "smart"), + ("destroy_constrs", "true"), + ("specialize", "true"), + ("skolemize", "true"), + ("star_linear_preds", "true"), + ("uncurry", "true"), + ("fast_descrs", "true"), + ("peephole_optim", "true"), + ("timeout", "30 s"), + ("tac_timeout", "500 ms"), + ("sym_break", "20"), + ("sharing_depth", "3"), + ("flatten_props", "false"), + ("max_threads", "0"), + ("debug", "false"), + ("verbose", "false"), + ("overlord", "false"), + ("show_all", "false"), + ("show_skolems", "true"), + ("show_datatypes", "false"), + ("show_consts", "false"), + ("format", "1"), + ("max_potential", "1"), + ("max_genuine", "1"), + ("check_potential", "false"), + ("check_genuine", "false")] val negated_params = [("dont_box", "box"), @@ -97,8 +99,8 @@ ("full_descrs", "fast_descrs"), ("no_peephole_optim", "peephole_optim"), ("dont_flatten_props", "flatten_props"), + ("no_debug", "debug"), ("quiet", "verbose"), - ("no_debug", "debug"), ("no_overlord", "overlord"), ("dont_show_all", "show_all"), ("hide_skolems", "show_skolems"), @@ -119,7 +121,7 @@ (* string * 'a -> unit *) fun check_raw_param (s, _) = if is_known_raw_param s then () - else error ("Unknown parameter " ^ quote s ^ ".") + else error ("Unknown parameter: " ^ quote s ^ ".") (* string -> string option *) fun unnegate_param_name name = @@ -139,20 +141,15 @@ | NONE => (name, value) structure Data = Theory_Data( - type T = {params: raw_param list} - val empty = {params = rev default_default_params} + type T = raw_param list + val empty = default_default_params |> map (apsnd single) val extend = I - fun merge ({params = ps1}, {params = ps2}) : T = - {params = AList.merge (op =) (K true) (ps1, ps2)}) + fun merge p : T = AList.merge (op =) (K true) p) (* raw_param -> theory -> theory *) -fun set_default_raw_param param thy = - let val {params} = Data.get thy in - Data.put {params = AList.update (op =) (unnegate_raw_param param) params} - thy - end +val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param (* theory -> raw_param list *) -val default_raw_params = #params o Data.get +val default_raw_params = Data.get (* string -> bool *) fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\") @@ -164,26 +161,6 @@ s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ stringify_raw_param_value (s2 :: ss) -(* bool -> string -> string -> bool option *) -fun bool_option_from_string option name s = - (case s of - "smart" => if option then NONE else raise Option - | "false" => SOME false - | "true" => SOME true - | "" => SOME true - | _ => raise Option) - handle Option.Option => - let val ss = map quote ((option ? cons "smart") ["true", "false"]) in - error ("Parameter " ^ quote name ^ " must be assigned " ^ - space_implode " " (serial_commas "or" ss) ^ ".") - end -(* bool -> raw_param list -> bool option -> string -> bool option *) -fun general_lookup_bool option raw_params default_value name = - case AList.lookup (op =) raw_params name of - SOME s => s |> stringify_raw_param_value - |> bool_option_from_string option name - | NONE => default_value - (* int -> string -> int *) fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s)) @@ -192,14 +169,19 @@ let val override_params = map unnegate_raw_param override_params val raw_params = rev override_params @ rev default_params + (* string -> string *) val lookup = Option.map stringify_raw_param_value o AList.lookup (op =) raw_params - (* string -> string *) - fun lookup_string name = the_default "" (lookup name) + val lookup_string = the_default "" o lookup + (* bool -> bool option -> string -> bool option *) + fun general_lookup_bool option default_value name = + case lookup name of + SOME s => Sledgehammer_Util.parse_bool_option option name s + | NONE => default_value (* string -> bool *) - val lookup_bool = the o general_lookup_bool false raw_params (SOME false) + val lookup_bool = the o general_lookup_bool false (SOME false) (* string -> bool option *) - val lookup_bool_option = general_lookup_bool true raw_params NONE + val lookup_bool_option = general_lookup_bool true NONE (* string -> string option -> int *) fun do_int name value = case value of @@ -253,7 +235,8 @@ :: map (fn (name, value) => (SOME (read (String.extract (name, size prefix + 1, NONE))), value |> stringify_raw_param_value - |> bool_option_from_string false name |> the)) + |> Sledgehammer_Util.parse_bool_option false name + |> the)) (filter (String.isPrefix (prefix ^ " ") o fst) raw_params) (* (string -> 'a) -> string -> ('a option * bool option) list *) fun lookup_bool_option_assigns read prefix = @@ -261,28 +244,13 @@ :: map (fn (name, value) => (SOME (read (String.extract (name, size prefix + 1, NONE))), value |> stringify_raw_param_value - |> bool_option_from_string true name)) + |> Sledgehammer_Util.parse_bool_option true name)) (filter (String.isPrefix (prefix ^ " ") o fst) raw_params) (* string -> Time.time option *) fun lookup_time name = case lookup name of NONE => NONE - | SOME "none" => NONE - | SOME s => - let - val msecs = - case space_explode " " s of - [s1, "min"] => 60000 * the (Int.fromString s1) - | [s1, "s"] => 1000 * the (Int.fromString s1) - | [s1, "ms"] => the (Int.fromString s1) - | _ => 0 - in - if msecs <= 0 then - error ("Parameter " ^ quote name ^ " must be assigned a positive \ - \time value (e.g., \"60 s\", \"200 ms\") or \"none\".") - else - SOME (Time.fromMilliseconds msecs) - end + | SOME s => Sledgehammer_Util.parse_time_option name s (* string -> term list *) val lookup_term_list = AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt @@ -368,22 +336,18 @@ extract_params (ProofContext.init thy) false (default_raw_params thy) o map (apsnd single) -(* OuterParse.token list -> string * OuterParse.token list *) -val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " " - -(* OuterParse.token list -> string list * OuterParse.token list *) -val scan_value = - Scan.repeat1 (OuterParse.minus >> single - || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name) - || OuterParse.$$$ "," |-- OuterParse.number >> prefix "," - >> single) >> flat - -(* OuterParse.token list -> raw_param * OuterParse.token list *) -val scan_param = - scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these) -(* OuterParse.token list -> raw_param list option * OuterParse.token list *) -val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param - --| OuterParse.$$$ "]") +(* P.token list -> string * P.token list *) +val parse_key = Scan.repeat1 P.typ_group >> space_implode " " +(* P.token list -> string list * P.token list *) +val parse_value = + Scan.repeat1 (P.minus >> single + || Scan.repeat1 (Scan.unless P.minus P.name) + || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat +(* P.token list -> raw_param * P.token list *) +val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) [] +(* P.token list -> raw_param list * P.token list *) +val parse_params = + Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") [] (* Proof.context -> ('a -> 'a) -> 'a -> 'a *) fun handle_exceptions ctxt f x = @@ -423,7 +387,6 @@ | Refute.REFUTE (loc, details) => error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".") - (* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *) fun pick_nits override_params auto i step state = let @@ -445,21 +408,20 @@ else (Toplevel.thread true (fn () => (go (); ())); (false, state)) end -(* raw_param list option * int option -> Toplevel.transition - -> Toplevel.transition *) -fun nitpick_trans (opt_params, opt_i) = +(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *) +fun nitpick_trans (params, i) = Toplevel.keep (fn st => - (pick_nits (these opt_params) false (the_default 1 opt_i) - (Toplevel.proof_position_of st) (Toplevel.proof_of st); ())) + (pick_nits params false i (Toplevel.proof_position_of st) + (Toplevel.proof_of st); ())) (* raw_param -> string *) fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value -(* raw_param list option -> Toplevel.transition -> Toplevel.transition *) -fun nitpick_params_trans opt_params = +(* raw_param list -> Toplevel.transition -> Toplevel.transition *) +fun nitpick_params_trans params = Toplevel.theory - (fold set_default_raw_param (these opt_params) + (fold set_default_raw_param params #> tap (fn thy => writeln ("Default parameters for Nitpick:\n" ^ (case rev (default_raw_params thy) of @@ -469,18 +431,18 @@ params |> map string_for_raw_param |> sort_strings |> cat_lines))))) -(* OuterParse.token list - -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *) -val scan_nitpick_command = - (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans -val scan_nitpick_params_command = scan_params #>> nitpick_params_trans +(* P.token list + -> (Toplevel.transition -> Toplevel.transition) * P.token list *) +val parse_nitpick_command = + (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans +val parse_nitpick_params_command = parse_params #>> nitpick_params_trans val _ = OuterSyntax.improper_command "nitpick" "try to find a counterexample for a given subgoal using Kodkod" - OuterKeyword.diag scan_nitpick_command + K.diag parse_nitpick_command val _ = OuterSyntax.command "nitpick_params" "set and display the default parameters for Nitpick" - OuterKeyword.thy_decl scan_nitpick_params_command + K.thy_decl parse_nitpick_params_command (* Proof.state -> bool * Proof.state *) fun auto_nitpick state = diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Mar 25 17:56:31 2010 +0100 @@ -194,8 +194,11 @@ else []) in - if null ss then [] - else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks + if null ss then + [] + else + Sledgehammer_Util.serial_commas "and" ss + |> map Pretty.str |> Pretty.breaks end (* scope -> string *) diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Mar 25 17:56:31 2010 +0100 @@ -46,7 +46,6 @@ val triple_lookup : (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option val is_substring_of : string -> string -> bool - val serial_commas : string -> string list -> string list val plural_s : int -> string val plural_s_for_list : 'a list -> string val flip_polarity : polarity -> polarity @@ -233,13 +232,6 @@ not (Substring.isEmpty (snd (Substring.position needle (Substring.full stack)))) -(* string -> string list -> string list *) -fun serial_commas _ [] = ["??"] - | serial_commas _ [s] = [s] - | serial_commas conj [s1, s2] = [s1, conj, s2] - | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] - | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss - (* int -> string *) fun plural_s n = if n = 1 then "" else "s" (* 'a list -> string *) diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Mar 25 17:56:31 2010 +0100 @@ -9,12 +9,19 @@ type axiom_name = Sledgehammer_HOL_Clause.axiom_name type hol_clause = Sledgehammer_HOL_Clause.hol_clause type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id + type relevance_override = + {add: Facts.ref list, + del: Facts.ref list, + only: bool} + val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list - val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> - (thm * (string * int)) list - val prepare_clauses : bool -> thm list -> thm list -> + val get_relevant_facts : + real -> bool option -> bool -> int -> bool -> relevance_override + -> Proof.context * (thm list * 'a) -> thm list + -> (thm * (string * int)) list + val prepare_clauses : bool option -> bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list -> (thm * (axiom_name * hol_clause_id)) list -> theory -> axiom_name vector * @@ -29,29 +36,21 @@ open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause -type axiom_name = axiom_name -type hol_clause = hol_clause -type hol_clause_id = hol_clause_id +type relevance_override = + {add: Facts.ref list, + del: Facts.ref list, + only: bool} (********************************************************************) (* some settings for both background automatic ATP calling procedure*) (* and also explicit ATP invocation methods *) (********************************************************************) -(* Translation mode can be auto-detected, or forced to be first-order or - higher-order *) -datatype mode = Auto | Fol | Hol; - -val translation_mode = Auto; - (*** background linkup ***) val run_blacklist_filter = true; (*** relevance filter parameters ***) -val run_relevance_filter = true; -val pass_mark = 0.5; val convergence = 3.2; (*Higher numbers allow longer inference chains*) -val follow_defs = false; (*Follow definitions. Makes problems bigger.*) (***************************************************************) (* Relevance Filtering *) @@ -139,8 +138,8 @@ (*Inserts a dummy "constant" referring to the theory name, so that relevance takes the given theory into account.*) -fun const_prop_of theory_const th = - if theory_const then +fun const_prop_of add_theory_const th = + if add_theory_const then let val name = Context.theory_name (theory_of_thm th) val t = Const (name ^ ". 1", HOLogic.boolT) in t $ prop_of th end @@ -169,7 +168,7 @@ structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord); -fun count_axiom_consts theory_const thy ((thm,_), tab) = +fun count_axiom_consts add_theory_const thy ((thm,_), tab) = let fun count_const (a, T, tab) = let val (c, cts) = const_with_typ thy (a,T) in (*Two-dimensional table update. Constant maps to types maps to count.*) @@ -182,7 +181,7 @@ count_term_consts (t, count_term_consts (u, tab)) | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab) | count_term_consts (_, tab) = tab - in count_term_consts (const_prop_of theory_const thm, tab) end; + in count_term_consts (const_prop_of add_theory_const thm, tab) end; (**** Actual Filtering Code ****) @@ -214,8 +213,8 @@ let val tab = add_term_consts_typs_rm thy (t, null_const_tab) in Symtab.fold add_expand_pairs tab [] end; -fun pair_consts_typs_axiom theory_const thy (thm,name) = - ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm))); +fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) = + (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm))); exception ConstFree; fun dest_ConstFree (Const aT) = aT @@ -234,9 +233,10 @@ end handle ConstFree => false in - case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) => - defs lhs rhs - | _ => false + case tm of + @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => + defs lhs rhs + | _ => false end; type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list); @@ -263,8 +263,12 @@ end end; -fun relevant_clauses max_new thy ctab p rel_consts = - let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) +fun relevant_clauses ctxt follow_defs max_new + (relevance_override as {add, del, only}) thy ctab p + rel_consts = + let val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) | relevant (newpairs,rejects) [] = let val (newrels,more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels @@ -272,11 +276,17 @@ val newp = p + (1.0-p) / convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); - (map #1 newrels) @ - (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) + map #1 newrels @ + relevant_clauses ctxt follow_defs max_new relevance_override thy ctab + newp rel_consts' (more_rejects @ rejects) end - | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = - let val weight = clause_weight ctab rel_consts consts_typs + | relevant (newrels, rejects) + ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = + let + val weight = if member Thm.eq_thm del_thms thm then 0.0 + else if member Thm.eq_thm add_thms thm then 1.0 + else if only then 0.0 + else clause_weight ctab rel_consts consts_typs in if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ @@ -285,23 +295,30 @@ else relevant (newrels, ax::rejects) axs end in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); - relevant ([],[]) + relevant ([],[]) end; -fun relevance_filter max_new theory_const thy axioms goals = - if run_relevance_filter andalso pass_mark >= 0.1 - then - let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms +fun relevance_filter ctxt relevance_threshold follow_defs max_new + add_theory_const relevance_override thy axioms goals = + if relevance_threshold > 0.0 then + let + val const_tab = List.foldl (count_axiom_consts add_theory_const thy) + Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals - val _ = trace_msg (fn () => ("Initial constants: " ^ - space_implode ", " (Symtab.keys goal_const_tab))); - val rels = relevant_clauses max_new thy const_tab (pass_mark) - goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms) - in - trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels))); - rels - end - else axioms; + val _ = + trace_msg (fn () => "Initial constants: " ^ + commas (Symtab.keys goal_const_tab)) + val relevant = + relevant_clauses ctxt follow_defs max_new relevance_override thy + const_tab relevance_threshold goal_const_tab + (map (pair_consts_typs_axiom add_theory_const thy) + axioms) + in + trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); + relevant + end + else + axioms; (***************************************************************) (* Retrieving and filtering lemmas *) @@ -526,34 +543,37 @@ likely to lead to unsound proofs.*) fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls; -fun is_first_order thy goal_cls = - case translation_mode of - Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls) - | Fol => true - | Hol => false +fun is_first_order thy higher_order goal_cls = + case higher_order of + NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls) + | SOME b => not b -fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls = +fun get_relevant_facts relevance_threshold higher_order follow_defs max_new + add_theory_const relevance_override + (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt - val is_FO = is_first_order thy goal_cls + val is_FO = is_first_order thy higher_order goal_cls val included_cls = get_all_lemmas ctxt |> cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy is_FO |> remove_unwanted_clauses in - relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) + relevance_filter ctxt relevance_threshold follow_defs max_new + add_theory_const relevance_override thy included_cls + (map prop_of goal_cls) end; (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy = +fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy = let (* add chain thms *) val chain_cls = cnf_rules_pairs thy (filter check_named (map pairname chain_ths)) val axcls = chain_cls @ axcls val extra_cls = chain_cls @ extra_cls - val is_FO = is_first_order thy goal_cls + val is_FO = is_first_order thy higher_order goal_cls val ccls = subtract_cls goal_cls extra_cls val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls val ccltms = map prop_of ccls diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Thu Mar 25 17:56:31 2010 +0100 @@ -51,9 +51,9 @@ conclusion variable to False.*) fun transform_elim th = case concl_of th of (*conclusion variable*) - Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) => + @{const Trueprop} $ (v as Var (_, @{typ bool})) => Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th - | v as Var(_, Type("prop",[])) => + | v as Var(_, @{typ prop}) => Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th | _ => th; @@ -76,7 +76,7 @@ fun declare_skofuns s th = let val nref = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) = + fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) = (*Existential: declare a Skolem function, then insert into body and continue*) let val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref) @@ -95,20 +95,20 @@ Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end - | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx = + | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p, [])) a in dec_sko (subst_bound (Free (fname, T), p)) thx end - | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx) - | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx + | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx) + | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx) + | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx | dec_sko t thx = thx (*Do nothing otherwise*) in fn thy => dec_sko (Thm.prop_of th) ([], thy) end; (*Traverse a theorem, accumulating Skolem function definitions.*) fun assume_skofuns s th = let val sko_count = Unsynchronized.ref 0 (* FIXME ??? *) - fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs = + fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs = (*Existential: declare a Skolem function, then insert into body and continue*) let val skos = map (#1 o Logic.dest_equals) defs (*existing sko fns*) val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*) @@ -123,13 +123,13 @@ in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end - | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs = + | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p,[])) a in dec_sko (subst_bound (Free(fname,T), p)) defs end - | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs) - | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs + | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs) + | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs | dec_sko t defs = defs (*Do nothing otherwise*) in dec_sko (prop_of th) [] end; @@ -156,7 +156,7 @@ fun strip_lambdas 0 th = th | strip_lambdas n th = case prop_of th of - _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) => + _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) => strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x)) | _ => th; @@ -171,7 +171,7 @@ let val thy = theory_of_cterm ct val Abs(x,_,body) = term_of ct - val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) + val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct) val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} in @@ -262,8 +262,9 @@ val (chilbert,cabs) = Thm.dest_comb ch val thy = Thm.theory_of_cterm chilbert val t = Thm.term_of chilbert - val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T - | _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) + val T = case t of + Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T + | _ => raise THM ("skolem_of_def: expected Eps", 0, [def]) val cex = Thm.cterm_of thy (HOLogic.exists_const T) val ex_tm = c_mkTrueprop (Thm.capply cex cabs) and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees))); @@ -289,7 +290,7 @@ map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); -(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***) +(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***) val max_lambda_nesting = 3; @@ -320,7 +321,8 @@ fun is_strange_thm th = case head_of (concl_of th) of - Const (a, _) => (a <> "Trueprop" andalso a <> "==") + Const (a, _) => (a <> @{const_name Trueprop} andalso + a <> @{const_name "=="}) | _ => false; fun bad_for_atp th = @@ -328,9 +330,10 @@ orelse exists_type type_has_topsort (prop_of th) orelse is_strange_thm th; +(* FIXME: put other record thms here, or declare as "no_atp" *) val multi_base_blacklist = - ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm", - "cases","ext_cases"]; (* FIXME put other record thms here, or declare as "no_atp" *) + ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits", + "split_asm", "cases", "ext_cases"]; (*Keep the full complexity of the original name*) fun flatten_name s = space_implode "_X" (Long_Name.explode s); diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Thu Mar 25 17:56:31 2010 +0100 @@ -48,7 +48,7 @@ open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor -(* Parameter t_full below indicates that full type information is to be +(* Parameter "full_types" below indicates that full type information is to be exported *) (* If true, each function will be directly applied to as many arguments as @@ -210,10 +210,8 @@ fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c | head_needs_hBOOL _ _ = true; -fun wrap_type t_full (s, tp) = - if t_full then - type_wrapper ^ paren_pack [s, string_of_fol_type tp] - else s; +fun wrap_type full_types (s, tp) = + if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s; fun apply ss = "hAPP" ^ paren_pack ss; @@ -224,7 +222,7 @@ (*Apply an operator to the argument strings, using either the "apply" operator or direct function application.*) -fun string_of_applic t_full cma (CombConst (c, _, tvars), args) = +fun string_of_applic full_types cma (CombConst (c, _, tvars), args) = let val c = if c = "equal" then "c_fequal" else c val nargs = min_arity_of cma c val args1 = List.take(args, nargs) @@ -232,21 +230,22 @@ Int.toString nargs ^ " but is applied to " ^ space_implode ", " args) val args2 = List.drop(args, nargs) - val targs = if not t_full then map string_of_fol_type tvars else [] + val targs = if full_types then [] else map string_of_fol_type tvars in string_apply (c ^ paren_pack (args1@targs), args2) end | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) | string_of_applic _ _ _ = error "string_of_applic"; -fun wrap_type_if t_full cnh (head, s, tp) = - if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s; +fun wrap_type_if full_types cnh (head, s, tp) = + if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s; -fun string_of_combterm (params as (t_full, cma, cnh)) t = +fun string_of_combterm (params as (full_types, cma, cnh)) t = let val (head, args) = strip_combterm_comb t - in wrap_type_if t_full cnh (head, - string_of_applic t_full cma (head, map (string_of_combterm (params)) args), - type_of_combterm t) + in wrap_type_if full_types cnh (head, + string_of_applic full_types cma + (head, map (string_of_combterm (params)) args), + type_of_combterm t) end; (*Boolean-valued terms are here converted to literals.*) @@ -318,11 +317,11 @@ fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; -fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = +fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = if c = "equal" then (addtypes tvars funcs, preds) else let val arity = min_arity_of cma c - val ntys = if not t_full then length tvars else 0 + val ntys = if not full_types then length tvars else 0 val addit = Symtab.update(c, arity+ntys) in if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds) @@ -452,12 +451,12 @@ (* TPTP format *) -fun write_tptp_file t_full file clauses = +fun write_tptp_file full_types file clauses = let val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses - val params = (t_full, cma, cnh) + val params = (full_types, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) val _ = @@ -474,12 +473,12 @@ (* DFG format *) -fun write_dfg_file t_full file clauses = +fun write_dfg_file full_types file clauses = let val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses val (cma, cnh) = count_constants clauses - val params = (t_full, cma, cnh) + val params = (full_types, cma, cnh) val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) and probname = Path.implode (Path.base file) val axstrs = map (#1 o (clause2dfg params)) axclauses diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Mar 25 17:56:31 2010 +0100 @@ -4,84 +4,292 @@ Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax. *) -structure Sledgehammer_Isar : sig end = +signature SLEDGEHAMMER_ISAR = +sig + type params = ATP_Manager.params + + val default_params : theory -> (string * string) list -> params +end; + +structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct +open Sledgehammer_Util open ATP_Manager open ATP_Minimal +open ATP_Wrapper structure K = OuterKeyword and P = OuterParse -val _ = - OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill)); +fun add_to_relevance_override ns : relevance_override = + {add = ns, del = [], only = false} +fun del_from_relevance_override ns : relevance_override = + {add = [], del = ns, only = false} +fun only_relevance_override ns : relevance_override = + {add = ns, del = [], only = true} +val default_relevance_override = add_to_relevance_override [] +fun merge_relevance_override_pairwise r1 r2 : relevance_override = + {add = #add r1 @ #add r2, del = #del r1 @ #del r2, + only = #only r1 orelse #only r2} +fun merge_relevance_overrides rs = + fold merge_relevance_override_pairwise rs default_relevance_override -val _ = - OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info)); +type raw_param = string * string list + +val default_default_params = + [("debug", "false"), + ("verbose", "false"), + ("relevance_threshold", "50"), + ("higher_order", "smart"), + ("respect_no_atp", "true"), + ("follow_defs", "false"), + ("isar_proof", "false"), + ("minimize_timeout", "5 s")] -val _ = - OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag - (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> - (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit))); +val negated_params = + [("no_debug", "debug"), + ("quiet", "verbose"), + ("partial_types", "full_types"), + ("first_order", "higher_order"), + ("ignore_no_atp", "respect_no_atp"), + ("dont_follow_defs", "follow_defs"), + ("metis_proof", "isar_proof")] + +val property_dependent_params = ["atps", "full_types", "timeout"] + +fun is_known_raw_param s = + AList.defined (op =) default_default_params s orelse + AList.defined (op =) negated_params s orelse + member (op =) property_dependent_params s -val _ = - OuterSyntax.improper_command "print_atps" "print external provers" K.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o - Toplevel.keep (print_provers o Toplevel.theory_of))); +fun check_raw_param (s, _) = + if is_known_raw_param s then () + else error ("Unknown parameter: " ^ quote s ^ ".") + +fun unnegate_raw_param (name, value) = + case AList.lookup (op =) negated_params name of + SOME name' => (name', case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value) + | NONE => (name, value) + +structure Data = Theory_Data( + type T = raw_param list + val empty = default_default_params |> map (apsnd single) + val extend = I + fun merge p : T = AList.merge (op =) (K true) p) -val _ = - OuterSyntax.command "sledgehammer" - "search for first-order proof using automatic theorem provers" K.diag - (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (sledgehammer names o Toplevel.proof_of))); +val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param +fun default_raw_params thy = + [("atps", [!atps]), + ("full_types", [if !full_types then "true" else "false"]), + ("timeout", [string_of_int (!timeout) ^ " s"])] @ + Data.get thy -val default_minimize_prover = "remote_vampire" -val default_minimize_time_limit = 5 +val infinity_time_in_secs = 60 * 60 * 24 * 365 +val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) -fun atp_minimize_command args thm_names state = +fun extract_params thy default_params override_params = let - fun theorems_from_names ctxt = - map (fn (name, interval) => + val override_params = map unnegate_raw_param override_params + val raw_params = rev override_params @ rev default_params + val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params + val lookup_string = the_default "" o lookup + fun general_lookup_bool option default_value name = + case lookup name of + SOME s => parse_bool_option option name s + | NONE => default_value + val lookup_bool = the o general_lookup_bool false (SOME false) + val lookup_bool_option = general_lookup_bool true NONE + fun lookup_time name = + the_timeout (case lookup name of + NONE => NONE + | SOME s => parse_time_option name s) + fun lookup_int name = + case lookup name of + NONE => 0 + | SOME s => case Int.fromString s of + SOME n => n + | NONE => error ("Parameter " ^ quote name ^ + " must be assigned an integer value.") + val debug = lookup_bool "debug" + val verbose = debug orelse lookup_bool "verbose" + val atps = lookup_string "atps" |> space_explode " " + val full_types = lookup_bool "full_types" + val relevance_threshold = + 0.01 * Real.fromInt (lookup_int "relevance_threshold") + val higher_order = lookup_bool_option "higher_order" + val respect_no_atp = lookup_bool "respect_no_atp" + val follow_defs = lookup_bool "follow_defs" + val isar_proof = lookup_bool "isar_proof" + val timeout = lookup_time "timeout" + val minimize_timeout = lookup_time "minimize_timeout" + in + {debug = debug, verbose = verbose, atps = atps, full_types = full_types, + relevance_threshold = relevance_threshold, higher_order = higher_order, + respect_no_atp = respect_no_atp, follow_defs = follow_defs, + isar_proof = isar_proof, timeout = timeout, + minimize_timeout = minimize_timeout} + end + +fun get_params thy = extract_params thy (default_raw_params thy) +fun default_params thy = get_params thy o map (apsnd single) + +fun atp_minimize_command override_params old_style_args fact_refs state = + let + val thy = Proof.theory_of state + val ctxt = Proof.context_of state + fun theorems_from_refs ctxt = + map (fn fact_ref => let - val thmref = Facts.Named ((name, Position.none), interval) - val ths = ProofContext.get_fact ctxt thmref - val name' = Facts.string_of_ref thmref + val ths = ProofContext.get_fact ctxt fact_ref + val name' = Facts.string_of_ref fact_ref in (name', ths) end) - fun get_time_limit_arg time_string = - (case Int.fromString time_string of - SOME t => t - | NONE => error ("Invalid time limit: " ^ quote time_string)) + fun get_time_limit_arg s = + (case Int.fromString s of + SOME t => Time.fromSeconds t + | NONE => error ("Invalid time limit: " ^ quote s)) fun get_opt (name, a) (p, t) = (case name of "time" => (p, get_time_limit_arg a) | "atp" => (a, t) | n => error ("Invalid argument: " ^ n)) - fun get_options args = - fold get_opt args (default_minimize_prover, default_minimize_time_limit) - val (prover_name, time_limit) = get_options args + val {atps, minimize_timeout, ...} = get_params thy override_params + val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout) + val params = + get_params thy + [("atps", [atp]), + ("minimize_timeout", + [string_of_int (Time.toSeconds timeout) ^ " s"])] val prover = - (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of + (case get_prover thy atp of SOME prover => prover - | NONE => error ("Unknown prover: " ^ quote prover_name)) - val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names + | NONE => error ("Unknown ATP: " ^ quote atp)) + val name_thms_pairs = theorems_from_refs ctxt fact_refs in - writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit - state name_thms_pairs)) + writeln (#2 (minimize_theorems params linear_minimize prover atp state + name_thms_pairs)) + end + +val runN = "run" +val minimizeN = "minimize" +val messagesN = "messages" +val available_atpsN = "available_atps" +val running_atpsN = "running_atps" +val kill_atpsN = "kill_atps" +val refresh_tptpN = "refresh_tptp" +val helpN = "help" + +val addN = "add" +val delN = "del" +val onlyN = "only" + +fun hammer_away override_params subcommand opt_i relevance_override state = + let + val thy = Proof.theory_of state + val _ = List.app check_raw_param override_params + in + if subcommand = runN then + sledgehammer (get_params thy override_params) (the_default 1 opt_i) + relevance_override state + else if subcommand = minimizeN then + atp_minimize_command override_params [] (#add relevance_override) state + else if subcommand = messagesN then + messages opt_i + else if subcommand = available_atpsN then + available_atps thy + else if subcommand = running_atpsN then + running_atps () + else if subcommand = kill_atpsN then + kill_atps () + else if subcommand = refresh_tptpN then + refresh_systems_on_tptp () + else + error ("Unknown subcommand: " ^ quote subcommand ^ ".") end -local structure K = OuterKeyword and P = OuterParse in +fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) = + Toplevel.keep (hammer_away params subcommand opt_i relevance_override + o Toplevel.proof_of) + +fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value + +fun sledgehammer_params_trans params = + Toplevel.theory + (fold set_default_raw_param params + #> tap (fn thy => + writeln ("Default parameters for Sledgehammer:\n" ^ + (case rev (default_raw_params thy) of + [] => "none" + | params => + (map check_raw_param params; + params |> map string_for_raw_param + |> sort_strings |> cat_lines))))) -val parse_args = - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] -val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel) +val parse_key = Scan.repeat1 P.typ_group >> space_implode " " +val parse_value = Scan.repeat1 P.xname +val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) [] +val parse_params = Scan.optional (Args.bracks (P.list parse_param)) [] +val parse_fact_refs = + Scan.repeat1 (Scan.unless (P.name -- Args.colon) + (P.xname -- Scan.option Attrib.thm_sel) + >> (fn (name, interval) => + Facts.Named ((name, Position.none), interval))) +val parse_relevance_chunk = + (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override) + || (Args.del |-- Args.colon |-- parse_fact_refs + >> del_from_relevance_override) + || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override) +val parse_relevance_override = + Scan.optional (Args.parens + (Scan.optional (parse_fact_refs >> only_relevance_override) + default_relevance_override + -- Scan.repeat parse_relevance_chunk) + >> op :: >> merge_relevance_overrides) + default_relevance_override +val parse_sledgehammer_command = + (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override + -- Scan.option P.nat) #>> sledgehammer_trans +val parse_sledgehammer_params_command = + parse_params #>> sledgehammer_params_trans + +val parse_minimize_args = + Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname))) + [] +val _ = + OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps)) +val _ = + OuterSyntax.improper_command "atp_info" + "print information about managed provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps)) +val _ = + OuterSyntax.improper_command "atp_messages" + "print recent messages issued by managed provers" K.diag + (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> + (fn limit => Toplevel.no_timing + o Toplevel.imperative (fn () => messages limit))) +val _ = + OuterSyntax.improper_command "print_atps" "print external provers" K.diag + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (available_atps o Toplevel.theory_of))) +val _ = + OuterSyntax.improper_command "atp_minimize" + "minimize theorem list with external prover" K.diag + (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) => + Toplevel.no_timing o Toplevel.unknown_proof o + Toplevel.keep (atp_minimize_command [] args fact_refs + o Toplevel.proof_of))) val _ = - OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag - (parse_args -- parse_thm_names >> (fn (args, thm_names) => - Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of))) - -end + OuterSyntax.improper_command "sledgehammer" + "search for first-order proof using automatic theorem provers" K.diag + parse_sledgehammer_command +val _ = + OuterSyntax.command "sledgehammer_params" + "set and display the default parameters for Sledgehammer" K.thy_decl + parse_sledgehammer_params_command end; diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 24 22:30:33 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Mar 25 17:56:31 2010 +0100 @@ -339,18 +339,18 @@ let val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt) - fun have_or_show "show" _ = "show \"" - | have_or_show have lname = have ^ " " ^ lname ^ ": \"" + fun have_or_show "show" _ = " show \"" + | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" fun do_line _ (lname, t, []) = (* No deps: it's a conjecture clause, with no proof. *) (case permuted_clause t ctms of - SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" + SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", [t])) | do_line have (lname, t, deps) = have_or_show have lname ^ string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^ - "\"\n by (metis " ^ space_implode " " deps ^ ")\n" + "\"\n by (metis " ^ space_implode " " deps ^ ")\n" fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] | do_lines ((lname, t, deps) :: lines) = do_line "have" (lname, t, deps) :: do_lines lines @@ -535,18 +535,20 @@ val kill_chained = filter_out (curry (op =) chained_hint) (* metis-command *) -fun metis_line [] = "apply metis" - | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" +fun metis_line [] = "by metis" + | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")" -(* atp_minimize [atp=] *) fun minimize_line _ [] = "" - | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ - Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ - space_implode " " (kill_chained lemmas)) + | minimize_line name lemmas = + "To minimize the number of lemmas, try this command:\n" ^ + Markup.markup Markup.sendback + ("sledgehammer minimize [atps = " ^ name ^ "] (" ^ + space_implode " " (kill_chained lemmas) ^ ")") ^ "." fun metis_lemma_list dfg name result = let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in - (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^ + ("Try this command: " ^ + Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^ minimize_line name lemmas ^ (if used_conj then "" @@ -570,8 +572,11 @@ if member (op =) tokens chained_hint then "" else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names in - (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof, - lemma_names) + (* Hack: The " \n" shouldn't be part of the markup. This is a workaround + for a strange ProofGeneral bug, whereby the first two letters of the word + "proof" are not highlighted. *) + (one_line_proof ^ "\n\nStructured proof:" ^ + Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names) end end; diff -r b88e061754a1 -r 142c3784a42b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Mar 25 17:56:31 2010 +0100 @@ -0,0 +1,53 @@ +(* Title: HOL/Sledgehammer/sledgehammer_util.ML + Author: Jasmin Blanchette, TU Muenchen + +General-purpose functions used by the Sledgehammer modules. +*) + +signature SLEDGEHAMMER_UTIL = +sig + val serial_commas : string -> string list -> string list + val parse_bool_option : bool -> string -> string -> bool option + val parse_time_option : string -> string -> Time.time option +end; + +structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = +struct + +fun serial_commas _ [] = ["??"] + | serial_commas _ [s] = [s] + | serial_commas conj [s1, s2] = [s1, conj, s2] + | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3] + | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss + +fun parse_bool_option option name s = + (case s of + "smart" => if option then NONE else raise Option + | "false" => SOME false + | "true" => SOME true + | "" => SOME true + | _ => raise Option) + handle Option.Option => + let val ss = map quote ((option ? cons "smart") ["true", "false"]) in + error ("Parameter " ^ quote name ^ " must be assigned " ^ + space_implode " " (serial_commas "or" ss) ^ ".") + end + +fun parse_time_option _ "none" = NONE + | parse_time_option name s = + let + val msecs = + case space_explode " " s of + [s1, "min"] => 60000 * the (Int.fromString s1) + | [s1, "s"] => 1000 * the (Int.fromString s1) + | [s1, "ms"] => the (Int.fromString s1) + | _ => 0 + in + if msecs <= 0 then + error ("Parameter " ^ quote name ^ " must be assigned a positive time \ + \value (e.g., \"60 s\", \"200 ms\") or \"none\".") + else + SOME (Time.fromMilliseconds msecs) + end + +end;