# HG changeset patch # User blanchet # Date 1307515663 -7200 # Node ID 30c141dc22d66466fec9418f566c807a1465046f # Parent 956895f9990478018c2f4372be408f79714c6c02 killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true" diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200 @@ -131,8 +131,7 @@ val type_constrs_of_terms : theory -> term list -> string list val prepare_atp_problem : Proof.context -> format -> formula_kind -> formula_kind -> type_sys - -> bool option -> bool -> bool -> term list -> term - -> ((string * locality) * term) list + -> bool -> bool -> term list -> term -> ((string * locality) * term) list -> string problem * string Symtab.table * int * int * (string * locality) list vector * int list * int Symtab.table val atp_problem_weights : string problem -> (string * real) list @@ -1833,9 +1832,10 @@ val conjsN = "Conjectures" val free_typesN = "Type variables" +val explicit_apply = NONE (* for experimental purposes *) + fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys - explicit_apply readable_names preproc hyp_ts concl_t - facts = + readable_names preproc hyp_ts concl_t facts = let val (format, type_sys) = choose_format [format] type_sys val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 08 08:47:43 2011 +0200 @@ -706,7 +706,7 @@ val ax_counts = Int_Tysubst_Table.empty |> fold (fn (ax_no, (_, (tysubst, _))) => - Int_Tysubst_Table.map_default ((ax_no, tysubst), 0) + Int_Tysubst_Table.map_default ((ax_no, [](*###*)), 0) (Integer.add 1)) substs |> Int_Tysubst_Table.dest val needed_axiom_props = diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 08 08:47:43 2011 +0200 @@ -167,7 +167,6 @@ fun prepare_metis_problem ctxt type_sys conj_clauses fact_clauses = let val type_sys = type_sys_from_string type_sys - val explicit_apply = NONE val clauses = conj_clauses @ fact_clauses |> (if polymorphism_of_type_sys type_sys = Polymorphic then @@ -188,8 +187,8 @@ val _ = tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) *) val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply - false false props @{prop False} [] + prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys false false props + @{prop False} [] (* val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_lines_for_atp_problem CNF atp_problem)) *) diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jun 08 08:47:43 2011 +0200 @@ -96,7 +96,6 @@ ("max_relevant", "smart"), ("max_mono_iters", "3"), ("max_new_mono_instances", "400"), - ("explicit_apply", "smart"), ("isar_proof", "false"), ("isar_shrink_factor", "1"), ("slicing", "true"), @@ -112,14 +111,13 @@ ("no_overlord", "overlord"), ("non_blocking", "blocking"), ("partial_types", "full_types"), - ("implicit_apply", "explicit_apply"), ("no_isar_proof", "isar_proof"), ("no_slicing", "slicing")] val params_for_minimize = ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters", - "max_new_mono_instances", "explicit_apply", "isar_proof", - "isar_shrink_factor", "timeout", "preplay_timeout"] + "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout", + "preplay_timeout"] val property_dependent_params = ["provers", "full_types", "timeout"] @@ -284,7 +282,6 @@ val max_relevant = lookup_option lookup_int "max_relevant" val max_mono_iters = lookup_int "max_mono_iters" val max_new_mono_instances = lookup_int "max_new_mono_instances" - val explicit_apply = lookup_option lookup_bool "explicit_apply" val isar_proof = lookup_bool "isar_proof" val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val slicing = mode <> Auto_Try andalso lookup_bool "slicing" @@ -299,9 +296,9 @@ provers = provers, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, type_sys = type_sys, - explicit_apply = explicit_apply, isar_proof = isar_proof, - isar_shrink_factor = isar_shrink_factor, slicing = slicing, - timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + slicing = slicing, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun get_params mode ctxt = extract_params mode (default_raw_params ctxt) diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jun 08 08:47:43 2011 +0200 @@ -47,7 +47,7 @@ fun print silent f = if silent then () else Output.urgent_message (f ()) fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, - max_new_mono_instances, type_sys, explicit_apply, isar_proof, + max_new_mono_instances, type_sys, isar_proof, isar_shrink_factor, preplay_timeout, ...} : params) silent (prover : prover) timeout i n state facts = let @@ -59,7 +59,7 @@ val {goal, ...} = Proof.goal state val params = {debug = debug, verbose = verbose, overlord = overlord, blocking = true, - provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, + provers = provers, type_sys = type_sys, relevance_thresholds = (1.01, 1.01), max_relevant = NONE, max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, @@ -73,16 +73,18 @@ val result as {outcome, used_facts, run_time_in_msecs, ...} = prover params (K (K "")) problem in - print silent (fn () => - case outcome of - SOME failure => string_for_failure failure - | NONE => "Found proof" ^ - (if length used_facts = length facts then "" - else " with " ^ n_facts used_facts) ^ - (case run_time_in_msecs of - SOME ms => - " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")" - | NONE => "") ^ "."); + print silent + (fn () => + case outcome of + SOME failure => string_for_failure failure + | NONE => + "Found proof" ^ + (if length used_facts = length facts then "" + else " with " ^ n_facts used_facts) ^ + (case run_time_in_msecs of + SOME ms => + " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")" + | NONE => "") ^ "."); result end diff -r 956895f99904 -r 30c141dc22d6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 08 08:47:43 2011 +0200 @@ -33,7 +33,6 @@ max_relevant: int option, max_mono_iters: int, max_new_mono_instances: int, - explicit_apply: bool option, isar_proof: bool, isar_shrink_factor: int, slicing: bool, @@ -301,7 +300,6 @@ max_relevant: int option, max_mono_iters: int, max_new_mono_instances: int, - explicit_apply: bool option, isar_proof: bool, isar_shrink_factor: int, slicing: bool, @@ -549,8 +547,8 @@ ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) ({debug, verbose, overlord, type_sys, max_relevant, max_mono_iters, - max_new_mono_instances, explicit_apply, isar_proof, - isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params) + max_new_mono_instances, isar_proof, isar_shrink_factor, slicing, + timeout, preplay_timeout, ...} : params) minimize_command ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = let @@ -655,9 +653,8 @@ val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_sys explicit_apply - (Config.get ctxt atp_readable_names) true hyp_ts concl_t - facts + type_sys (Config.get ctxt atp_readable_names) true hyp_ts + concl_t facts fun weights () = atp_problem_weights atp_problem val core = File.shell_path command ^ " " ^ diff -r 956895f99904 -r 30c141dc22d6 src/HOL/ex/atp_export.ML --- a/src/HOL/ex/atp_export.ML Wed Jun 08 08:47:43 2011 +0200 +++ b/src/HOL/ex/atp_export.ML Wed Jun 08 08:47:43 2011 +0200 @@ -102,11 +102,10 @@ val facts = facts0 |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) - val explicit_apply = NONE val (atp_problem, _, _, _, _, _, _) = ATP_Translate.prepare_atp_problem ctxt format - ATP_Problem.Axiom ATP_Problem.Axiom type_sys explicit_apply false true - [] @{prop False} facts + ATP_Problem.Axiom ATP_Problem.Axiom type_sys false true [] + @{prop False} facts val infers = facts0 |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th),