# HG changeset patch # User blanchet # Date 1271772289 -7200 # Node ID 5563c717638aec144e0d148a1f6ed30370dd8c68 # Parent 3ff99369517516a38beb71814bdb825e4429aa80# Parent 61159615a0c5351d2611cbd2df0d48a4161d2498 merged diff -r 3ff993695175 -r 5563c717638a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Apr 20 16:04:49 2010 +0200 @@ -391,7 +391,7 @@ |> 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 1 + val minimize = minimize_theorems params prover prover_name 1 val _ = log separator in case minimize st (these (!named_thms)) of diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 20 16:04:49 2010 +0200 @@ -15,10 +15,11 @@ overlord: bool, atps: string list, full_types: bool, + explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, convergence: real, - theory_const: bool option, + theory_relevant: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, @@ -57,6 +58,7 @@ structure ATP_Manager : ATP_MANAGER = struct +open Sledgehammer_Util open Sledgehammer_Fact_Filter open Sledgehammer_Proof_Reconstruct @@ -68,10 +70,11 @@ overlord: bool, atps: string list, full_types: bool, + explicit_apply: bool, respect_no_atp: bool, relevance_threshold: real, convergence: real, - theory_const: bool option, + theory_relevant: bool option, higher_order: bool option, follow_defs: bool, isar_proof: bool, @@ -189,14 +192,21 @@ val min_wait_time = Time.fromMilliseconds 300; val max_wait_time = Time.fromSeconds 10; +(* This is a workaround for Proof General's off-by-a-few sendback display bug, + whereby "pr" in "proof" is not highlighted. *) +val break_into_chunks = + map (replace_all "\n\n" "\000") #> maps (space_explode "\000") + fun print_new_messages () = - let val msgs = Synchronized.change_result global_state - (fn {manager, timeout_heap, active, cancelling, messages, store} => - (messages, make_state manager timeout_heap active cancelling [] store)) - in - if null msgs then () - else priority ("Sledgehammer: " ^ space_implode "\n\n" msgs) - end; + case Synchronized.change_result global_state + (fn {manager, timeout_heap, active, cancelling, messages, store} => + (messages, make_state manager timeout_heap active cancelling [] + store)) of + [] => () + | msgs => + msgs |> break_into_chunks + |> (fn msg :: msgs => "Sledgehammer: " ^ msg :: msgs) + |> List.app priority fun check_thread_manager params = Synchronized.change global_state (fn state as {manager, timeout_heap, active, cancelling, messages, store} => @@ -289,7 +299,7 @@ space_implode "\n\n" ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling); - in writeln (running ^ "\n" ^ interrupting) end; + in priority (running ^ "\n" ^ interrupting) end; fun messages opt_limit = let @@ -298,15 +308,14 @@ val header = "Recent ATP messages" ^ (if length store <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):"); - in writeln (space_implode "\n\n" (header :: #1 (chop limit store))) end; - + in List.app priority (header :: break_into_chunks (#1 (chop limit store))) end (** The Sledgehammer **) (* named provers *) -fun err_dup_prover name = error ("Duplicate prover: " ^ quote name); +fun err_dup_prover name = error ("Duplicate prover: " ^ quote name ^ "."); structure Provers = Theory_Data ( @@ -324,8 +333,9 @@ fun get_prover thy name = Option.map #1 (Symtab.lookup (Provers.get thy) name); -fun available_atps thy = Pretty.writeln - (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy)))); +fun available_atps thy = + priority ("Available ATPs: " ^ + commas (sort_strings (Symtab.keys (Provers.get thy))) ^ ".") (* start prover thread *) @@ -333,7 +343,7 @@ 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 ATP: " ^ quote name) + NONE => warning ("Unknown ATP: " ^ quote name ^ ".") | SOME prover => let val {context = ctxt, facts, goal} = Proof.goal proof_state; @@ -352,7 +362,7 @@ val message = #message (prover params timeout problem) handle Sledgehammer_HOL_Clause.TRIVIAL => metis_line i n [] - | ERROR msg => ("Error: " ^ msg); + | ERROR msg => "Error: " ^ msg ^ ".\n"; val _ = unregister params message (Thread.self ()); in () end); in () end); diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Tue Apr 20 16:04:49 2010 +0200 @@ -9,13 +9,9 @@ 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 - val linear_minimize : 'a minimize_fun - val binary_minimize : 'a minimize_fun val minimize_theorems : - params -> (string * thm list) minimize_fun -> prover -> string -> int - -> Proof.state -> (string * thm list) list + params -> prover -> string -> int -> Proof.state -> (string * thm list) list -> (string * thm list) list option * string end; @@ -27,62 +23,24 @@ open Sledgehammer_Proof_Reconstruct open ATP_Manager -type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list - (* Linear minimization algorithm *) -fun linear_minimize p s = +fun linear_minimize test s = let - fun aux [] needed = needed - | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x) - in aux s [] end; - -(* Binary minimalization *) - -local - fun isplit (l, r) [] = (l, r) - | isplit (l, r) [h] = (h :: l, r) - | isplit (l, r) (h1 :: h2 :: t) = isplit (h1 :: l, h2 :: r) t -in - fun split lst = isplit ([], []) lst -end - -local - fun min _ _ [] = raise Empty - | min _ _ [s0] = [s0] - | min p sup s = - let - val (l0, r0) = split s - in - if p (sup @ l0) then - min p sup l0 - else if p (sup @ r0) then - min p sup r0 - else - let - val l = min p (sup @ r0) l0 - val r = min p (sup @ l) r0 - in l @ r end - end -in - (* return a minimal subset v of s that satisfies p - @pre p(s) & ~p([]) & monotone(p) - @post v subset s & p(v) & - forall e in v. ~p(v \ e) - *) - fun binary_minimize p s = - case min p [] s of - [x] => if p [] then [] else [x] - | m => m -end + fun aux [] p = p + | aux (x :: xs) (needed, result) = + case test (xs @ needed) of + SOME result => aux xs (needed, result) + | NONE => aux xs (x :: needed, result) + in aux s end (* failure check and producing answer *) -datatype 'a prove_result = Success of 'a | Failure | Timeout | Error +datatype outcome = Success | Failure | Timeout | Error -val string_of_result = - fn Success _ => "Success" +val string_of_outcome = + fn Success => "Success" | Failure => "Failure" | Timeout => "Timeout" | Error => "Error" @@ -94,26 +52,19 @@ ("# Cannot determine problem status within resource limit", Timeout), ("Error", Error)] -fun produce_answer ({success, proof, internal_thm_names, filtered_clauses, ...} - : prover_result) = +fun outcome_of_result (result as {success, proof, ...} : prover_result) = if success then - (Success (Vector.foldr (op ::) [] internal_thm_names, filtered_clauses), - proof) - else - let - val failure = failure_strings |> get_first (fn (s, t) => - if String.isSubstring s proof then SOME (t, proof) else NONE) - in - (case failure of - SOME res => res - | NONE => (Failure, proof)) - end - + Success + else case get_first (fn (s, outcome) => + if String.isSubstring s proof then SOME outcome + else NONE) failure_strings of + SOME outcome => outcome + | NONE => Failure (* wrapper for calling external prover *) fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover - timeout subgoal state filtered name_thms_pairs = + timeout subgoal state filtered_clauses name_thms_pairs = let val num_theorems = length name_thms_pairs val _ = priority ("Testing " ^ string_of_int num_theorems ^ @@ -124,50 +75,61 @@ val problem = {subgoal = subgoal, 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 - + axiom_clauses = SOME axclauses, + filtered_clauses = SOME (the_default axclauses filtered_clauses)} + in + `outcome_of_result (prover params timeout problem) + |>> tap (priority o string_of_outcome) + end (* minimalization of thms *) -fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover - prover_name i state name_thms_pairs = +fun minimize_theorems (params as {minimize_timeout, isar_proof, modulus, + sorts, ...}) + prover atp_name i state name_thms_pairs = let val msecs = Time.toMilliseconds minimize_timeout + val n = length name_thms_pairs val _ = - priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^ - " theorems, ATP: " ^ prover_name ^ - ", time limit: " ^ string_of_int msecs ^ " ms") + priority ("Sledgehammer minimizer: ATP " ^ quote atp_name ^ + " with a time limit of " ^ string_of_int msecs ^ " ms.") val test_thms_fun = sledgehammer_test_theorems params prover minimize_timeout i state fun test_thms filtered thms = - case test_thms_fun filtered thms of (Success _, _) => true | _ => false - val n = state |> Proof.raw_goal |> #goal |> prop_of |> Logic.count_prems + case test_thms_fun filtered thms of + (Success, result) => SOME result + | _ => NONE + + val {context = ctxt, facts, goal} = Proof.goal state; + val n = Logic.count_prems (prop_of goal) in (* try prove first to check result and get used theorems *) (case test_thms_fun NONE name_thms_pairs of - (Success (used, filtered), _) => + (Success, result as {internal_thm_names, filtered_clauses, ...}) => let - val ordered_used = sort_distinct string_ord used + val used = internal_thm_names |> Vector.foldr (op ::) [] + |> sort_distinct string_ord val to_use = - if length ordered_used < length name_thms_pairs then - filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs + if length used < length name_thms_pairs then + filter (fn (name1, _) => List.exists (curry (op =) name1) used) + name_thms_pairs else name_thms_pairs - val min_thms = - if null to_use then [] - else gen_min (test_thms (SOME filtered)) to_use - val min_names = sort_distinct string_ord (map fst min_thms) + val (min_thms, {proof, internal_thm_names, ...}) = + linear_minimize (test_thms (SOME filtered_clauses)) to_use + ([], result) + val n = length min_thms val _ = priority (cat_lines - ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) - in (SOME min_thms, metis_line i n min_names) end + ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".") + in + (SOME min_thms, + proof_text isar_proof true modulus sorts atp_name proof + internal_thm_names ctxt goal i |> fst) + end | (Timeout, _) => (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ \option (e.g., \"timeout = " ^ string_of_int (10 + msecs div 1000) ^ " s\").") - | (Error, msg) => - (NONE, "Error in prover: " ^ msg) + | (Error, {message, ...}) => (NONE, "ATP error: " ^ message) | (Failure, _) => (* Failure sometimes mean timeout, unfortunately. *) (NONE, "Failure: No proof was found with the current time limit. You \ diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Apr 20 16:04:49 2010 +0200 @@ -48,7 +48,7 @@ arguments: Time.time -> string, failure_strs: string list, max_new_clauses: int, - prefers_theory_const: bool, + prefers_theory_relevant: bool, supports_isar_proofs: bool}; @@ -67,7 +67,7 @@ | (failure :: _) => SOME failure fun generic_prover overlord get_facts prepare write_file cmd args failure_strs - produce_answer name ({debug, full_types, ...} : params) + proof_text name ({debug, full_types, explicit_apply, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -128,7 +128,7 @@ if Config.get ctxt measure_runtime then split_time s else (s, 0) fun run_on probfile = if File.exists cmd then - write_file debug full_types probfile clauses + write_file full_types explicit_apply probfile clauses |> pair (apfst split_time' (bash_output (cmd_line probfile))) else error ("Bad executable: " ^ Path.implode cmd ^ "."); @@ -142,7 +142,7 @@ File.write (Path.explode (Path.implode probfile ^ "_proof")) ("% " ^ timestamp () ^ "\n" ^ proof) - val (((proof, atp_run_time_in_msecs), rc), conj_pos) = + val (((proof, atp_run_time_in_msecs), rc), _) = with_path cleanup export run_on (prob_pathname subgoal); (* Check for success and print out some information on failure. *) @@ -151,9 +151,7 @@ val (message, relevant_thm_names) = if is_some failure then ("ATP failed to find a proof.\n", []) else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", []) - else - (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th, - subgoal)); + else proof_text name proof internal_thm_names ctxt th subgoal in {success = success, message = message, relevant_thm_names = relevant_thm_names, @@ -167,21 +165,20 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, - prefers_theory_const, supports_isar_proofs}) + prefers_theory_relevant, supports_isar_proofs}) (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, isar_proof, + theory_relevant, higher_order, follow_defs, isar_proof, modulus, sorts, ...}) timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - (the_default prefers_theory_const theory_const)) - (prepare_clauses higher_order false) write_tptp_file command + (the_default prefers_theory_relevant theory_relevant)) + (prepare_clauses higher_order false) + (write_tptp_file (overlord andalso not isar_proof)) command (arguments timeout) failure_strs - (if supports_isar_proofs andalso isar_proof then - structured_isar_proof modulus sorts - else - metis_lemma_list false) name params; + (proof_text (supports_isar_proofs andalso isar_proof) false modulus sorts) + name params fun tptp_prover name p = (name, generic_tptp_prover (name, p)); @@ -201,7 +198,7 @@ failure_strs = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], max_new_clauses = 60, - prefers_theory_const = false, + prefers_theory_relevant = false, supports_isar_proofs = true} val vampire = tptp_prover "vampire" vampire_config @@ -218,7 +215,7 @@ "SZS status: ResourceOut", "SZS status ResourceOut", "# Cannot determine problem status"], max_new_clauses = 100, - prefers_theory_const = false, + prefers_theory_relevant = false, supports_isar_proofs = true} val e = tptp_prover "e" e_config @@ -227,29 +224,32 @@ fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, - prefers_theory_const, ...} : prover_config)) + prefers_theory_relevant, ...} : prover_config)) (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_const, higher_order, follow_defs, ...}) + theory_relevant, higher_order, follow_defs, ...}) timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses - (the_default prefers_theory_const theory_const)) + (the_default prefers_theory_relevant theory_relevant)) (prepare_clauses higher_order true) write_dfg_file command - (arguments timeout) failure_strs (metis_lemma_list true) name params; + (arguments timeout) failure_strs (metis_proof_text false false) + name params fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p)); +(* The "-VarWeight=3" option helps the higher-order problems, probably by + counteracting the presence of "hAPP". *) val spass_config : prover_config = {command = Path.explode "$SPASS_HOME/SPASS", arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ - " -FullRed=0 -DocProof -TimeLimit=" ^ + " -FullRed=0 -DocProof -VarWeight=3 -TimeLimit=" ^ string_of_int (generous_to_secs timeout)), failure_strs = ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."], max_new_clauses = 40, - prefers_theory_const = true, + prefers_theory_relevant = true, supports_isar_proofs = false} val spass = dfg_prover ("spass", spass_config) @@ -283,7 +283,7 @@ val remote_failure_strs = ["Remote-script could not extract proof"]; fun remote_prover_config prover_prefix args - ({failure_strs, max_new_clauses, prefers_theory_const, ...} + ({failure_strs, max_new_clauses, prefers_theory_relevant, ...} : prover_config) : prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = (fn timeout => @@ -291,7 +291,7 @@ the_system prover_prefix), failure_strs = remote_failure_strs @ failure_strs, max_new_clauses = max_new_clauses, - prefers_theory_const = prefers_theory_const, + prefers_theory_relevant = prefers_theory_relevant, supports_isar_proofs = false} val remote_vampire = diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Apr 20 16:04:49 2010 +0200 @@ -693,13 +693,19 @@ val unused = th_cls_pairs |> map_filter (fn (name, cls) => if common_thm used cls then NONE else SOME name) in - if null unused then () - else warning ("Metis: unused theorems " ^ commas_quote unused); + if not (common_thm used cls) then + warning "Metis: The goal is provable because the context is \ + \inconsistent." + else if not (null unused) then + warning ("Metis: Unused theorems: " ^ commas_quote unused + ^ ".") + else + (); case result of (_,ith)::_ => - (trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); + (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); [ith]) - | _ => (trace_msg (fn () => "Metis: no result"); + | _ => (trace_msg (fn () => "Metis: No result"); []) end | Metis.Resolution.Satisfiable _ => diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 20 16:04:49 2010 +0200 @@ -127,8 +127,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 theory_relevant th = + if theory_relevant then let val name = Context.theory_name (theory_of_thm th) val t = Const (name ^ ". 1", HOLogic.boolT) in t $ prop_of th end @@ -157,7 +157,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 theory_relevant 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.*) @@ -170,7 +170,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 theory_relevant thm, tab) end; (**** Actual Filtering Code ****) @@ -201,8 +201,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 (p as (thm, _)) = - (p, (consts_typs_of_term thy (const_prop_of theory_const thm))); +fun pair_consts_typs_axiom theory_relevant thy (p as (thm, _)) = + (p, (consts_typs_of_term thy (const_prop_of theory_relevant thm))); exception ConstFree; fun dest_ConstFree (Const aT) = aT @@ -254,8 +254,10 @@ fun relevant_clauses ctxt convergence follow_defs max_new (relevance_override as {add, del, only}) thy ctab = let - val add_thms = maps (ProofContext.get_fact ctxt) add - val del_thms = maps (ProofContext.get_fact ctxt) del + val thms_for_facts = + maps (maps (cnf_axiom thy) o ProofContext.get_fact ctxt) + val add_thms = thms_for_facts add + val del_thms = thms_for_facts del fun iter p rel_consts = let fun relevant ([], _) [] = [] (* Nothing added this iteration *) @@ -294,10 +296,10 @@ in iter end fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_const relevance_override thy axioms goals = + theory_relevant relevance_override thy axioms goals = if relevance_threshold > 0.0 then let - val const_tab = List.foldl (count_axiom_consts theory_const thy) + val const_tab = List.foldl (count_axiom_consts theory_relevant thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals val _ = @@ -306,7 +308,8 @@ val relevant = relevant_clauses ctxt convergence follow_defs max_new relevance_override thy const_tab relevance_threshold goal_const_tab - (map (pair_consts_typs_axiom theory_const thy) axioms) + (map (pair_consts_typs_axiom theory_relevant thy) + axioms) in trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant)); relevant @@ -365,11 +368,11 @@ val ths = filter_out bad_for_atp ths0; in if Facts.is_concealed facts name orelse null ths orelse - respect_no_atp andalso is_package_def name then I - else - (case find_first check_thms [name1, name2, name] of - NONE => I - | SOME a => cons (a, ths)) + (respect_no_atp andalso is_package_def name) then + I + else case find_first check_thms [name1, name2, name] of + NONE => I + | SOME a => cons (a, ths) end); in valid_facts global_facts @ valid_facts local_facts end; @@ -502,7 +505,7 @@ | SOME b => not b fun get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new theory_const + higher_order follow_defs max_new theory_relevant (relevance_override as {add, only, ...}) (ctxt, (chain_ths, th)) goal_cls = if (only andalso null add) orelse relevance_threshold > 1.0 then @@ -517,7 +520,7 @@ |> remove_unwanted_clauses in relevance_filter ctxt relevance_threshold convergence follow_defs max_new - theory_const relevance_override thy included_cls + theory_relevant relevance_override thy included_cls (map prop_of goal_cls) end @@ -527,7 +530,8 @@ let (* add chain thms *) val chain_cls = - cnf_rules_pairs thy (filter check_named (map pairname chain_ths)) + cnf_rules_pairs thy (filter check_named + (map (`Thm.get_name_hint) chain_ths)) val axcls = chain_cls @ axcls val extra_cls = chain_cls @ extra_cls val is_FO = is_first_order thy higher_order goal_cls diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 20 16:04:49 2010 +0200 @@ -10,7 +10,6 @@ val trace_msg: (unit -> string) -> unit val skolem_prefix: string val cnf_axiom: theory -> thm -> thm list - val pairname: thm -> string * thm val multi_base_blacklist: string list val bad_for_atp: thm -> bool val type_has_topsort: typ -> bool @@ -370,7 +369,7 @@ val update_cache = ThmCache.map o apfst o Thmtab.update; fun mark_seen name = ThmCache.map (apsnd (Symtab.update (name, ()))); -(*Exported function to convert Isabelle theorems into axiom clauses*) +(* Convert Isabelle theorems into axiom clauses. *) fun cnf_axiom thy th0 = let val th = Thm.transfer thy th0 in case lookup_cache thy th of @@ -379,11 +378,6 @@ end; -(**** Rules from the context ****) - -fun pairname th = (Thm.get_name_hint th, th); - - (**** Translate a set of theorems into CNF ****) fun pair_name_cls k (n, []) = [] diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Apr 20 16:04:49 2010 +0200 @@ -4,7 +4,7 @@ Storing/printing FOL clauses and arity clauses. Typed equality is treated differently. -FIXME: combine with res_hol_clause! +FIXME: combine with sledgehammer_hol_clause! *) signature SLEDGEHAMMER_FOL_CLAUSE = @@ -57,12 +57,14 @@ val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arity_clause list val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list - val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table - val add_classrel_clause_preds : classrel_clause * int Symtab.table -> int Symtab.table + val add_type_sort_preds: typ -> int Symtab.table -> int Symtab.table + val add_classrel_clause_preds : + classrel_clause -> int Symtab.table -> int Symtab.table val class_of_arityLit: arLit -> class - val add_arity_clause_preds: arity_clause * int Symtab.table -> int Symtab.table - val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table - val add_arity_clause_funcs: arity_clause * int Symtab.table -> int Symtab.table + val add_arity_clause_preds: arity_clause -> int Symtab.table -> int Symtab.table + val add_fol_type_funcs: fol_type -> int Symtab.table -> int Symtab.table + val add_arity_clause_funcs: + arity_clause -> int Symtab.table -> int Symtab.table val init_functab: int Symtab.table val dfg_sign: bool -> string -> string val dfg_of_typeLit: bool -> type_literal -> string @@ -102,7 +104,7 @@ val tconst_prefix = "tc_"; val class_prefix = "class_"; -fun union_all xss = List.foldl (uncurry (union (op =))) [] xss; +fun union_all xss = fold (union (op =)) xss [] (* Provide readable names for the more common symbolic functions *) val const_trans_table = @@ -218,7 +220,8 @@ type name = string * string type name_pool = string Symtab.table * string Symtab.table -fun empty_name_pool debug = if debug then SOME (`I Symtab.empty) else NONE +fun empty_name_pool readable_names = + if readable_names then SOME (`I Symtab.empty) else NONE fun pool_map f xs = fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs @@ -240,7 +243,7 @@ fun translate_first_char f s = String.str (f (String.sub (s, 0))) ^ String.extract (s, 1, NONE) -fun clean_short_name full_name s = +fun readable_name full_name s = let val s = s |> Long_Name.base_name |> fold remove_all ["\<^sub>", "\<^bsub>", "\<^esub>", "\<^isub>"] @@ -249,7 +252,8 @@ (s' |> rev |> implode |> String.translate - (fn c => if Char.isAlphaNum c then String.str c else "")) + (fn c => if Char.isAlphaNum c orelse c = #"_" then String.str c + else "")) ^ replicate_string (String.size s - length s') "_" val s' = if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s' @@ -267,8 +271,8 @@ | nice_name (full_name, desired_name) (SOME the_pool) = case Symtab.lookup (fst the_pool) full_name of SOME nice_name => (nice_name, SOME the_pool) - | NONE => add_nice_name full_name (clean_short_name full_name desired_name) - 0 the_pool + | NONE => add_nice_name full_name (readable_name full_name desired_name) 0 + the_pool |> apsnd SOME (**** Definitions and functions for FOL clauses, for conversion to TPTP or DFG @@ -315,7 +319,7 @@ | pred_of_sort (LTFree (s,ty)) = (s,1) (*Given a list of sorted type variables, return a list of type literals.*) -fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts); +fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) [] (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear. * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a @@ -373,11 +377,11 @@ (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs thy [] supers = [] | class_pairs thy subs supers = - let val class_less = Sorts.class_less(Sign.classes_of thy) - fun add_super sub (super,pairs) = - if class_less (sub,super) then (sub,super)::pairs else pairs - fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers - in List.foldl add_supers [] subs end; + let + val class_less = Sorts.class_less (Sign.classes_of thy) + fun add_super sub super = class_less (sub, super) ? cons (sub, super) + fun add_supers sub = fold (add_super sub) supers + in fold add_supers subs [] end fun make_classrel_clause (sub,super) = ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super, @@ -402,18 +406,18 @@ arity_clause dfg (class::seen) n (tcons,ars) fun multi_arity_clause dfg [] = [] - | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) = - arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists + | multi_arity_clause dfg ((tcons, ars) :: tc_arlists) = + arity_clause dfg [] 1 (tcons, ars) @ multi_arity_clause dfg tc_arlists (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy provided its arguments have the corresponding sorts.*) fun type_class_pairs thy tycons classes = let val alg = Sign.classes_of thy - fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class] - fun add_class tycon (class,pairs) = - (class, domain_sorts(tycon,class))::pairs - handle Sorts.CLASS_ERROR _ => pairs - fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes) + fun domain_sorts tycon = Sorts.mg_domain alg tycon o single + fun add_class tycon class = + cons (class, domain_sorts tycon class) + handle Sorts.CLASS_ERROR _ => I + fun try_classes tycon = (tycon, fold (add_class tycon) classes []) in map try_classes tycons end; (*Proving one (tycon, class) membership may require proving others, so iterate.*) @@ -435,35 +439,35 @@ (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong function (it flags repeated declarations of a function, even with the same arity)*) -fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs; +fun update_many keypairs = fold Symtab.update keypairs -fun add_type_sort_preds (T, preds) = - update_many (preds, map pred_of_sort (sorts_on_typs T)); +val add_type_sort_preds = update_many o map pred_of_sort o sorts_on_typs -fun add_classrel_clause_preds (ClassrelClause {subclass,superclass,...}, preds) = - Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); +fun add_classrel_clause_preds (ClassrelClause {subclass, superclass, ...}) = + Symtab.update (subclass, 1) #> Symtab.update (superclass, 1) fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass | class_of_arityLit (TVarLit (tclass, _)) = tclass; -fun add_arity_clause_preds (ArityClause {conclLit,premLits,...}, preds) = - let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits) - fun upd (class,preds) = Symtab.update (class,1) preds - in List.foldl upd preds classes end; +fun add_arity_clause_preds (ArityClause {conclLit, premLits, ...}) = + let + val classes = map (make_type_class o class_of_arityLit) + (conclLit :: premLits) + in fold (Symtab.update o rpair 1) classes end; (*** Find occurrences of functions in clauses ***) -fun add_foltype_funcs (TyVar _, funcs) = funcs - | add_foltype_funcs (TyFree (s, _), funcs) = Symtab.update (s, 0) funcs - | add_foltype_funcs (TyConstr ((s, _), tys), funcs) = - List.foldl add_foltype_funcs (Symtab.update (s, length tys) funcs) tys; +fun add_fol_type_funcs (TyVar _) = I + | add_fol_type_funcs (TyFree (s, _)) = Symtab.update (s, 0) + | add_fol_type_funcs (TyConstr ((s, _), tys)) = + Symtab.update (s, length tys) #> fold add_fol_type_funcs tys (*TFrees are recorded as constants*) fun add_type_sort_funcs (TVar _, funcs) = funcs | add_type_sort_funcs (TFree (a, _), funcs) = Symtab.update (make_fixed_type_var a, 0) funcs -fun add_arity_clause_funcs (ArityClause {conclLit,...}, funcs) = +fun add_arity_clause_funcs (ArityClause {conclLit,...}) funcs = let val TConsLit (_, tcons, tvars) = conclLit in Symtab.update (tcons, length tvars) funcs end; diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Apr 20 16:04:49 2010 +0200 @@ -34,13 +34,12 @@ val get_helper_clauses : bool -> theory -> bool -> hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list -> hol_clause list - val write_tptp_file : bool -> bool -> Path.T -> + val write_tptp_file : bool -> bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> - int * int + classrel_clause list * arity_clause list -> unit val write_dfg_file : bool -> bool -> Path.T -> hol_clause list * hol_clause list * hol_clause list * hol_clause list * - classrel_clause list * arity_clause list -> int * int + classrel_clause list * arity_clause list -> unit end structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = @@ -51,19 +50,19 @@ open Sledgehammer_Fact_Preprocessor (* Parameter "full_types" below indicates that full type information is to be -exported *) + exported. -(* If true, each function will be directly applied to as many arguments as - possible, avoiding use of the "apply" operator. Use of hBOOL is also - minimized. *) -val minimize_applies = true; + If "explicit_apply" is false, each function will be directly applied to as + many arguments as possible, avoiding use of the "apply" operator. Use of + hBOOL is also minimized. +*) fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c); (*True if the constant ever appears outside of the top-level position in literals. If false, the constant always receives all of its arguments and is used as a predicate.*) -fun needs_hBOOL const_needs_hBOOL c = - not minimize_applies orelse +fun needs_hBOOL explicit_apply const_needs_hBOOL c = + explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c); @@ -174,13 +173,13 @@ end; -fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = - let val cls = make_clause dfg thy (id, name, Axiom, th) - in - if isTaut cls then pairs else (name,cls)::pairs - end; +fun add_axiom_clause dfg thy (th, (name, id)) = + let val cls = make_clause dfg thy (id, name, Axiom, th) in + not (isTaut cls) ? cons (name, cls) + end -fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; +fun make_axiom_clauses dfg thy clauses = + fold (add_axiom_clause dfg thy) clauses [] fun make_conjecture_clauses_aux _ _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = @@ -212,9 +211,10 @@ val type_wrapper = "ti"; -fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) = - needs_hBOOL const_needs_hBOOL c - | head_needs_hBOOL _ _ = true; +fun head_needs_hBOOL explicit_apply const_needs_hBOOL + (CombConst ((c, _), _, _)) = + needs_hBOOL explicit_apply const_needs_hBOOL c + | head_needs_hBOOL _ _ _ = true fun wrap_type full_types (s, ty) pool = if full_types then @@ -224,8 +224,11 @@ else (s, pool) -fun wrap_type_if full_types cnh (head, s, tp) = - if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s +fun wrap_type_if full_types explicit_apply cnh (head, s, tp) = + if head_needs_hBOOL explicit_apply cnh head then + wrap_type full_types (s, tp) + else + pair s fun apply ss = "hAPP" ^ paren_pack ss; @@ -253,18 +256,22 @@ | string_of_application _ _ (CombVar (name, _), args) pool = nice_name name pool |>> (fn s => string_apply (s, args)) -fun string_of_combterm (params as (full_types, cma, cnh)) t pool = +fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t + pool = let val (head, args) = strip_combterm_comb t val (ss, pool) = pool_map (string_of_combterm params) args pool val (s, pool) = string_of_application full_types cma (head, ss) pool - in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end + in + wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t) + pool + end (*Boolean-valued terms are here converted to literals.*) fun boolify params c = string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single -fun string_of_predicate (params as (_, _, cnh)) t = +fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t = case t of (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) => (* DFG only: new TPTP prefers infix equality *) @@ -273,7 +280,8 @@ | _ => case #1 (strip_combterm_comb t) of CombConst ((s, _), _, _) => - (if needs_hBOOL cnh s then boolify else string_of_combterm) params t + (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm) + params t | _ => boolify params t @@ -341,51 +349,53 @@ (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars; +fun add_types tvars = fold add_fol_type_funcs tvars -fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars), (funcs, preds)) = +fun add_decls (full_types, explicit_apply, cma, cnh) + (CombConst ((c, _), _, tvars)) (funcs, preds) = if c = "equal" then - (addtypes tvars funcs, preds) + (add_types tvars funcs, preds) else let val arity = min_arity_of cma c 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) - else (addtypes tvars funcs, addit preds) + if needs_hBOOL explicit_apply cnh c then + (add_types tvars (addit funcs), preds) + else + (add_types tvars funcs, addit preds) end - | add_decls _ (CombVar (_,ctp), (funcs, preds)) = - (add_foltype_funcs (ctp,funcs), preds) - | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); + | add_decls _ (CombVar (_, ctp)) (funcs, preds) = + (add_fol_type_funcs ctp funcs, preds) + | add_decls params (CombApp (P, Q)) decls = + decls |> add_decls params P |> add_decls params Q -fun add_literal_decls params (Literal (_,c), decls) = add_decls params (c,decls); +fun add_literal_decls params (Literal (_, c)) = add_decls params c -fun add_clause_decls params (HOLClause {literals, ...}, decls) = - List.foldl (add_literal_decls params) decls literals +fun add_clause_decls params (HOLClause {literals, ...}) decls = + fold (add_literal_decls params) literals decls handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") fun decls_of_clauses params clauses arity_clauses = - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) init_functab) - val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty - val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) - in - (Symtab.dest (List.foldl add_arity_clause_funcs functab arity_clauses), - Symtab.dest predtab) - end; + let val functab = init_functab |> Symtab.update (type_wrapper, 2) + |> Symtab.update ("hAPP", 2) + val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1) + val (functab, predtab) = + (functab, predtab) |> fold (add_clause_decls params) clauses + |>> fold add_arity_clause_funcs arity_clauses + in (Symtab.dest functab, Symtab.dest predtab) end -fun add_clause_preds (HOLClause {ctypes_sorts, ...}, preds) = - List.foldl add_type_sort_preds preds ctypes_sorts +fun add_clause_preds (HOLClause {ctypes_sorts, ...}) preds = + fold add_type_sort_preds ctypes_sorts preds handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = - Symtab.dest - (List.foldl add_classrel_clause_preds - (List.foldl add_arity_clause_preds - (List.foldl add_clause_preds Symtab.empty clauses) - arity_clauses) - clsrel_clauses) - + Symtab.empty + |> fold add_clause_preds clauses + |> fold add_arity_clause_preds arity_clauses + |> fold add_classrel_clause_preds clsrel_clauses + |> Symtab.dest (**********************************************************************) (* write clauses to files *) @@ -395,22 +405,19 @@ Symtab.make [("c_COMBI", 0), ("c_COMBK", 0), ("c_COMBB", 0), ("c_COMBC", 0), ("c_COMBS", 0)]; -fun count_combterm (CombConst ((c, _), _, _), ct) = - (case Symtab.lookup ct c of NONE => ct (*no counter*) - | SOME n => Symtab.update (c,n+1) ct) - | count_combterm (CombVar _, ct) = ct - | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); +fun count_combterm (CombConst ((c, _), _, _)) = + Symtab.map_entry c (Integer.add 1) + | count_combterm (CombVar _) = I + | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 -fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); +fun count_literal (Literal (_, t)) = count_combterm t -fun count_clause (HOLClause {literals, ...}, ct) = - List.foldl count_literal ct literals; +fun count_clause (HOLClause {literals, ...}) = fold count_literal literals -fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}, ct) = - if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals - else ct; +fun count_user_clause user_lemmas (HOLClause {axiom_name, literals, ...}) = + member (op =) user_lemmas axiom_name ? fold count_literal literals -fun cnf_helper_thms thy = cnf_rules_pairs thy o map pairname +fun cnf_helper_thms thy = cnf_rules_pairs thy o map (`Thm.get_name_hint) fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = if isFO then @@ -418,8 +425,8 @@ else let val axclauses = map #2 (make_axiom_clauses dfg thy axcls) - val ct0 = List.foldl count_clause init_counters conjectures - val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses + val ct = init_counters |> fold count_clause conjectures + |> fold (count_user_clause user_lemmas) axclauses fun needed c = the (Symtab.lookup ct c) > 0 val IK = if needed "c_COMBI" orelse needed "c_COMBK" then cnf_helper_thms thy [@{thm COMBI_def}, @{thm COMBK_def}] @@ -440,15 +447,16 @@ fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) = let val (head, args) = strip_combterm_comb t val n = length args - val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL) + val (const_min_arity, const_needs_hBOOL) = + (const_min_arity, const_needs_hBOOL) + |> fold (count_constants_term false) args in case head of CombConst ((a, _),_,_) => (*predicate or function version of "equal"?*) let val a = if a="equal" andalso not toplev then "c_fequal" else a - val const_min_arity = Symtab.map_default (a, n) (Integer.min n) const_min_arity in - if toplev then (const_min_arity, const_needs_hBOOL) - else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL)) + (const_min_arity |> Symtab.map_default (a, n) (Integer.min n), + const_needs_hBOOL |> not toplev ? Symtab.update (a, true)) end | _ => (const_min_arity, const_needs_hBOOL) end; @@ -461,64 +469,74 @@ (const_min_arity, const_needs_hBOOL) = fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); -fun display_arity const_needs_hBOOL (c,n) = +fun display_arity explicit_apply const_needs_hBOOL (c,n) = trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ - (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else "")); + (if needs_hBOOL explicit_apply const_needs_hBOOL c then + " needs hBOOL" + else + "")) -fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) = - if minimize_applies then +fun count_constants explicit_apply + (conjectures, _, extra_clauses, helper_clauses, _, _) = + if not explicit_apply then let val (const_min_arity, const_needs_hBOOL) = fold count_constants_clause conjectures (Symtab.empty, Symtab.empty) |> fold count_constants_clause extra_clauses |> fold count_constants_clause helper_clauses - val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity)) + val _ = List.app (display_arity explicit_apply const_needs_hBOOL) + (Symtab.dest (const_min_arity)) in (const_min_arity, const_needs_hBOOL) end else (Symtab.empty, Symtab.empty); +fun header () = + "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ + "% " ^ timestamp () ^ "\n" + (* TPTP format *) -fun write_tptp_file debug full_types file clauses = +fun write_tptp_file readable_names full_types explicit_apply file clauses = let fun section _ [] = [] | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss - val pool = empty_name_pool debug + val pool = empty_name_pool readable_names val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants clauses - val params = (full_types, cma, cnh) + val (cma, cnh) = count_constants explicit_apply clauses + val params = (full_types, explicit_apply, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip - val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) + val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss []) val (ax_clss, pool) = pool_map (apfst fst oo tptp_clause params) axclauses pool val classrel_clss = map tptp_classrel_clause classrel_clauses val arity_clss = map tptp_arity_clause arity_clauses val (helper_clss, pool) = pool_map (apfst fst oo tptp_clause params) helper_clauses pool - val _ = - File.write_list file ( - "% This file was generated by Isabelle (most likely Sledgehammer)\n" ^ - "% " ^ timestamp () ^ "\n" :: - section "Relevant fact" ax_clss @ - section "Type variable" tfree_clss @ - section "Conjecture" conjecture_clss @ - section "Class relationship" classrel_clss @ - section "Arity declaration" arity_clss @ - section "Helper fact" helper_clss) - in (length axclauses + 1, length tfree_clss + length conjecture_clss) - end; + in + File.write_list file + (header () :: + section "Relevant fact" ax_clss @ + section "Type variable" tfree_clss @ + section "Conjecture" conjecture_clss @ + section "Class relationship" classrel_clss @ + section "Arity declaration" arity_clss @ + section "Helper fact" helper_clss) + end (* DFG format *) -fun write_dfg_file debug full_types file clauses = +fun write_dfg_file full_types explicit_apply file clauses = let - val pool = empty_name_pool debug + (* Some of the helper functions below are not name-pool-aware. However, + there's no point in adding name pool support if the DFG format is on its + way out anyway. *) + val pool = NONE val (conjectures, axclauses, _, helper_clauses, classrel_clauses, arity_clauses) = clauses - val (cma, cnh) = count_constants clauses - val params = (full_types, cma, cnh) + val (cma, cnh) = count_constants explicit_apply clauses + val params = (full_types, explicit_apply, cma, cnh) val ((conjecture_clss, tfree_litss), pool) = pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip and probname = Path.implode (Path.base file) @@ -526,30 +544,25 @@ val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) val (helper_clauses_strs, pool) = pool_map (apfst fst oo dfg_clause params) helper_clauses pool - val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses + val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses - val _ = - File.write_list file ( - string_of_start probname :: - string_of_descrip probname :: - string_of_symbols (string_of_funcs funcs) - (string_of_preds (cl_preds @ ty_preds)) :: - "list_of_clauses(axioms, cnf).\n" :: - axstrs @ - map dfg_classrel_clause classrel_clauses @ - map dfg_arity_clause arity_clauses @ - helper_clauses_strs @ - ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ - tfree_clss @ - conjecture_clss @ - ["end_of_list.\n\n", - (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*) - "list_of_settings(SPASS).\n{*\nset_flag(VarWeight, 3).\n*}\nend_of_list.\n\n", - "end_problem.\n"]) - in - (length axclauses + length classrel_clauses + length arity_clauses + - length helper_clauses + 1, length tfree_clss + length conjecture_clss) + File.write_list file + (header () :: + string_of_start probname :: + string_of_descrip probname :: + string_of_symbols (string_of_funcs funcs) + (string_of_preds (cl_preds @ ty_preds)) :: + "list_of_clauses(axioms, cnf).\n" :: + axstrs @ + map dfg_classrel_clause classrel_clauses @ + map dfg_arity_clause arity_clauses @ + helper_clauses_strs @ + ["end_of_list.\n\nlist_of_clauses(conjectures, cnf).\n"] @ + tfree_clss @ + conjecture_clss @ + ["end_of_list.\n\n", + "end_problem.\n"]) end end; diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 20 16:04:49 2010 +0200 @@ -41,10 +41,11 @@ [("debug", "false"), ("verbose", "false"), ("overlord", "false"), + ("explicit_apply", "false"), ("respect_no_atp", "true"), ("relevance_threshold", "50"), ("convergence", "320"), - ("theory_const", "smart"), + ("theory_relevant", "smart"), ("higher_order", "smart"), ("follow_defs", "false"), ("isar_proof", "false"), @@ -58,9 +59,10 @@ [("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), + ("implicit_apply", "explicit_apply"), ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), - ("no_theory_const", "theory_const"), + ("theory_irrelevant", "theory_relevant"), ("first_order", "higher_order"), ("dont_follow_defs", "follow_defs"), ("metis_proof", "isar_proof"), @@ -146,11 +148,12 @@ val overlord = lookup_bool "overlord" val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" + val explicit_apply = lookup_bool "explicit_apply" val respect_no_atp = lookup_bool "respect_no_atp" val relevance_threshold = 0.01 * Real.fromInt (lookup_int "relevance_threshold") val convergence = 0.01 * Real.fromInt (lookup_int "convergence") - val theory_const = lookup_bool_option "theory_const" + val theory_relevant = lookup_bool_option "theory_relevant" val higher_order = lookup_bool_option "higher_order" val follow_defs = lookup_bool "follow_defs" val isar_proof = lookup_bool "isar_proof" @@ -160,11 +163,12 @@ val minimize_timeout = lookup_time "minimize_timeout" in {debug = debug, verbose = verbose, overlord = overlord, atps = atps, - full_types = full_types, respect_no_atp = respect_no_atp, - relevance_threshold = relevance_threshold, convergence = convergence, - theory_const = theory_const, higher_order = higher_order, - follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus, - sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout} + full_types = full_types, explicit_apply = explicit_apply, + respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, + convergence = convergence, theory_relevant = theory_relevant, + higher_order = higher_order, follow_defs = follow_defs, + isar_proof = isar_proof, modulus = modulus, sorts = sorts, + timeout = timeout, minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy) @@ -183,27 +187,27 @@ fun get_time_limit_arg s = (case Int.fromString s of SOME t => Time.fromSeconds t - | NONE => error ("Invalid time limit: " ^ quote s)) + | 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)) + | n => error ("Invalid argument: " ^ n ^ ".")) 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.toMilliseconds timeout) ^ " ms"])] + (override_params @ + [("atps", [atp]), + ("minimize_timeout", + [string_of_int (Time.toMilliseconds timeout) ^ " ms"])]) val prover = (case get_prover thy atp of SOME prover => prover - | NONE => error ("Unknown ATP: " ^ quote atp)) + | NONE => error ("Unknown ATP: " ^ quote atp ^ ".")) val name_thms_pairs = theorems_from_refs ctxt fact_refs in - writeln (#2 (minimize_theorems params linear_minimize prover atp i state - name_thms_pairs)) + priority (#2 (minimize_theorems params prover atp i state name_thms_pairs)) end val runN = "run" diff -r 3ff993695175 -r 5563c717638a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 20 15:17:18 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 20 16:04:49 2010 +0200 @@ -14,10 +14,15 @@ val strip_prefix: string -> string -> string option val is_proof_well_formed: string -> bool val metis_line: int -> int -> string list -> string - val metis_lemma_list: bool -> string -> - string * string vector * (int * int) * Proof.context * thm * int -> string * string list - val structured_isar_proof: int -> bool -> string -> - string * string vector * (int * int) * Proof.context * thm * int -> string * string list + val metis_proof_text: + bool -> bool -> string -> string -> string vector -> Proof.context -> thm + -> int -> string * string list + val isar_proof_text: + bool -> int -> bool -> string -> string -> string vector -> Proof.context + -> thm -> int -> string * string list + val proof_text: + bool -> bool -> int -> bool -> string -> string -> string vector + -> Proof.context -> thm -> int -> string * string list end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -493,45 +498,22 @@ exists (fn s => String.isSubstring s proof) end_proof_strs (* === EXTRACTING LEMMAS === *) -(* lines have the form "cnf(108, axiom, ...", -the number (108) has to be extracted)*) -fun get_step_nums false extract = +(* A list consisting of the first number in each line is returned. + TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the + number (108) is extracted. + DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is + extracted. *) +fun get_step_nums proof_extract = let val toks = String.tokens (not o Char.isAlphaNum) fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) = Int.fromString ntok + | inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *) | inputno _ = NONE - val lines = split_lines extract + val lines = split_lines proof_extract in map_filter (inputno o toks) lines end -(*String contains multiple lines. We want those of the form - "253[0:Inp] et cetera..." - A list consisting of the first number in each line is returned. *) -| get_step_nums true proofextract = - let val toks = String.tokens (not o Char.isAlphaNum) - fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok - | inputno _ = NONE - val lines = split_lines proofextract - in map_filter (inputno o toks) lines end -(*extracting lemmas from tstp-output between the lines from above*) -fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = - let - (* get the names of axioms from their numbers*) - fun get_axiom_names thm_names step_nums = - let - val last_axiom = Vector.length thm_names - fun is_axiom n = n <= last_axiom - fun is_conj n = n >= fst conj_count andalso - n < fst conj_count + snd conj_count - fun getname i = Vector.sub(thm_names, i-1) - in - (sort_distinct string_ord (filter (fn x => x <> "??.unknown") - (map getname (filter is_axiom step_nums))), - exists is_conj step_nums) - end - in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end; - (*Used to label theorems chained into the sledgehammer call*) val chained_hint = "CHAINED"; val kill_chained = filter_out (curry (op =) chained_hint) @@ -546,29 +528,33 @@ fun metis_line i n xs = "Try this command: " ^ Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" -fun minimize_line _ [] = "" - | minimize_line name xs = +fun minimize_line _ _ [] = "" + | minimize_line isar_proof atp_name xs = "To minimize the number of lemmas, try this command: " ^ Markup.markup Markup.sendback - ("sledgehammer minimize [atp = " ^ name ^ "] (" ^ + ("sledgehammer minimize [atp = " ^ atp_name ^ + (if isar_proof then ", isar_proof" else "") ^ "] (" ^ space_implode " " xs ^ ")") ^ ".\n" -fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) = +fun metis_proof_text isar_proof minimal atp_name proof thm_names + (_ : Proof.context) goal i = let - val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result + val lemmas = + proof |> get_proof_extract + |> get_step_nums + |> filter (fn i => i <= Vector.length thm_names) + |> map (fn i => Vector.sub (thm_names, i - 1)) + |> filter (fn x => x <> "??.unknown") + |> sort_distinct string_ord val n = Logic.count_prems (prop_of goal) val xs = kill_chained lemmas in - (metis_line i n xs ^ minimize_line name xs ^ - (if used_conj then - "" - else - "\nWarning: The goal is provable because the context is inconsistent."), + (metis_line i n xs ^ + (if minimal then "" else minimize_line isar_proof atp_name xs), kill_chained lemmas) - end; + end -fun structured_isar_proof modulus sorts name - (result as (proof, thm_names, conj_count, ctxt, goal, i)) = +fun isar_proof_text minimal modulus sorts atp_name proof thm_names ctxt goal i = let (* We could use "split_lines", but it can return blank lines. *) val lines = String.tokens (equal #"\n"); @@ -576,7 +562,8 @@ String.translate (fn c => if Char.isSpace c then "" else str c) val extract = get_proof_extract proof val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) - val (one_line_proof, lemma_names) = metis_lemma_list false name result + val (one_line_proof, lemma_names) = + metis_proof_text true minimal atp_name proof thm_names ctxt goal i val tokens = String.tokens (fn c => c = #" ") one_line_proof val isar_proof = if member (op =) tokens chained_hint then "" @@ -588,4 +575,8 @@ lemma_names) end +fun proof_text isar_proof minimal modulus sorts = + if isar_proof then isar_proof_text minimal modulus sorts + else metis_proof_text isar_proof minimal + end;