# HG changeset patch # User blanchet # Date 1272360287 -7200 # Node ID 8a5c99a1c965f65b9549abf1bf1646b8d7deb66d # Parent 69004340f53ce8a051a8daf68ca926a034625e5c remove "higher_order" option from Sledgehammer -- the "smart" default is good enough diff -r 69004340f53c -r 8a5c99a1c965 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 27 10:51:39 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Apr 27 11:24:47 2010 +0200 @@ -22,7 +22,6 @@ relevance_threshold: real, convergence: real, theory_relevant: bool option, - higher_order: bool option, follow_defs: bool, isar_proof: bool, shrink_factor: int, @@ -83,7 +82,6 @@ relevance_threshold: real, convergence: real, theory_relevant: bool option, - higher_order: bool option, follow_defs: bool, isar_proof: bool, shrink_factor: int, diff -r 69004340f53c -r 8a5c99a1c965 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Apr 27 10:51:39 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Apr 27 11:24:47 2010 +0200 @@ -233,14 +233,13 @@ (name, {home, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) (params as {debug, overlord, respect_no_atp, relevance_threshold, - convergence, theory_relevant, higher_order, follow_defs, - isar_proof, ...}) + convergence, theory_relevant, follow_defs, isar_proof, ...}) minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_axiom_clauses + follow_defs max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses higher_order false) + (prepare_clauses false) (write_tptp_file (debug andalso overlord)) home executable (arguments timeout) proof_delims known_failures name params minimize_command @@ -305,13 +304,13 @@ (name, {home, executable, arguments, proof_delims, known_failures, max_axiom_clauses, prefers_theory_relevant}) (params as {overlord, respect_no_atp, relevance_threshold, convergence, - theory_relevant, higher_order, follow_defs, ...}) + theory_relevant, follow_defs, ...}) minimize_command timeout = generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_axiom_clauses + follow_defs max_axiom_clauses (the_default prefers_theory_relevant theory_relevant)) - (prepare_clauses higher_order true) write_dfg_file home executable + (prepare_clauses true) write_dfg_file home executable (arguments timeout) proof_delims known_failures name params minimize_command diff -r 69004340f53c -r 8a5c99a1c965 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 27 10:51:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Apr 27 11:24:47 2010 +0200 @@ -10,6 +10,7 @@ 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, @@ -19,15 +20,15 @@ val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list val get_relevant_facts : - bool -> real -> real -> bool option -> bool -> int -> bool - -> relevance_override -> Proof.context * (thm list * 'a) -> thm list + bool -> real -> real -> 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 * - (hol_clause list * hol_clause list * hol_clause list * - hol_clause list * classrel_clause list * arity_clause list) + val prepare_clauses : + bool -> thm list -> thm list -> (thm * (axiom_name * hol_clause_id)) list + -> (thm * (axiom_name * hol_clause_id)) list -> theory + -> axiom_name vector + * (hol_clause list * hol_clause list * hol_clause list * + hol_clause list * classrel_clause list * arity_clause list) end; structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = @@ -500,13 +501,10 @@ 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 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 is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of fun get_relevant_facts respect_no_atp relevance_threshold convergence - higher_order follow_defs max_new theory_relevant + 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 @@ -514,7 +512,7 @@ else let val thy = ProofContext.theory_of ctxt - val is_FO = is_first_order thy higher_order goal_cls + val is_FO = is_first_order thy goal_cls val included_cls = get_all_lemmas respect_no_atp ctxt |> cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy is_FO @@ -527,7 +525,7 @@ (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) -fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy = +fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy = let (* add chain thms *) val chain_cls = @@ -535,7 +533,7 @@ (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 + val is_FO = is_first_order thy goal_cls val ccls = subtract_cls extra_cls goal_cls val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls val ccltms = map prop_of ccls diff -r 69004340f53c -r 8a5c99a1c965 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 27 10:51:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Apr 27 11:24:47 2010 +0200 @@ -96,7 +96,6 @@ ("relevance_threshold", "50"), ("convergence", "320"), ("theory_relevant", "smart"), - ("higher_order", "smart"), ("follow_defs", "false"), ("isar_proof", "false"), ("shrink_factor", "1"), @@ -113,14 +112,13 @@ ("implicit_apply", "explicit_apply"), ("ignore_no_atp", "respect_no_atp"), ("theory_irrelevant", "theory_relevant"), - ("first_order", "higher_order"), ("dont_follow_defs", "follow_defs"), ("metis_proof", "isar_proof"), ("no_sorts", "sorts")] val params_for_minimize = ["debug", "verbose", "overlord", "full_types", "explicit_apply", - "higher_order", "isar_proof", "shrink_factor", "sorts", "minimize_timeout"] + "isar_proof", "shrink_factor", "sorts", "minimize_timeout"] val property_dependent_params = ["atps", "full_types", "timeout"] @@ -200,7 +198,6 @@ 0.01 * Real.fromInt (lookup_int "relevance_threshold") val convergence = 0.01 * Real.fromInt (lookup_int "convergence") 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" val shrink_factor = Int.max (1, lookup_int "shrink_factor") @@ -212,9 +209,9 @@ 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, shrink_factor = shrink_factor, sorts = sorts, - timeout = timeout, minimize_timeout = minimize_timeout} + follow_defs = follow_defs, isar_proof = isar_proof, + shrink_factor = shrink_factor, sorts = sorts, timeout = timeout, + minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy)