# HG changeset patch # User blanchet # Date 1273868990 -7200 # Node ID ff01d3ae9ad451e4cdcc691e9507f7745ace4198 # Parent 538cf3fdfe4de103cfa543f682894efec2729689 renamed options diff -r 538cf3fdfe4d -r ff01d3ae9ad4 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 22:28:39 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 22:29:50 2010 +0200 @@ -24,7 +24,7 @@ theory_relevant: bool option, defs_relevant: bool, isar_proof: bool, - shrink_factor: int, + isar_shrink_factor: int, timeout: Time.time, minimize_timeout: Time.time} type problem = @@ -83,7 +83,7 @@ theory_relevant: bool option, defs_relevant: bool, isar_proof: bool, - shrink_factor: int, + isar_shrink_factor: int, timeout: Time.time, minimize_timeout: Time.time} diff -r 538cf3fdfe4d -r ff01d3ae9ad4 src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:28:39 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 22:29:50 2010 +0200 @@ -112,8 +112,8 @@ fun generic_prover overlord get_facts prepare write_file home_var executable args proof_delims known_failures name - ({debug, full_types, explicit_apply, isar_proof, shrink_factor, ...} - : params) minimize_command + ({debug, full_types, explicit_apply, isar_proof, isar_shrink_factor, + ...} : params) minimize_command ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -218,7 +218,8 @@ case outcome of NONE => proof_text isar_proof - (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape) + (pool, debug, full_types, isar_shrink_factor, ctxt, + conjecture_shape) (minimize_command, proof, internal_thm_names, th, subgoal) | SOME failure => (string_for_failure failure ^ "\n", []) in diff -r 538cf3fdfe4d -r ff01d3ae9ad4 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:28:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:29:50 2010 +0200 @@ -69,7 +69,7 @@ (* minimalization of thms *) fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout, - isar_proof, shrink_factor, ...}) + isar_proof, isar_shrink_factor, ...}) i n state name_thms_pairs = let val thy = Proof.theory_of state @@ -110,7 +110,8 @@ in (SOME min_thms, proof_text isar_proof - (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape) + (pool, debug, full_types, isar_shrink_factor, ctxt, + conjecture_shape) (K "", proof, internal_thm_names, goal, i) |> fst) end | {outcome = SOME TimedOut, ...} => diff -r 538cf3fdfe4d -r ff01d3ae9ad4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 22:28:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 22:29:50 2010 +0200 @@ -98,7 +98,7 @@ ("theory_relevant", "smart"), ("defs_relevant", "false"), ("isar_proof", "false"), - ("shrink_factor", "1"), + ("isar_shrink_factor", "1"), ("minimize_timeout", "5 s")] val alias_params = @@ -116,7 +116,7 @@ val params_for_minimize = ["debug", "verbose", "overlord", "full_types", "explicit_apply", - "isar_proof", "shrink_factor", "minimize_timeout"] + "isar_proof", "isar_shrink_factor", "minimize_timeout"] val property_dependent_params = ["atps", "full_types", "timeout"] @@ -199,7 +199,7 @@ val theory_relevant = lookup_bool_option "theory_relevant" val defs_relevant = lookup_bool "defs_relevant" val isar_proof = lookup_bool "isar_proof" - val shrink_factor = Int.max (1, lookup_int "shrink_factor") + val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = lookup_time "timeout" val minimize_timeout = lookup_time "minimize_timeout" in @@ -208,8 +208,8 @@ respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, relevance_convergence = relevance_convergence, theory_relevant = theory_relevant, defs_relevant = defs_relevant, - isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout, - minimize_timeout = minimize_timeout} + isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, + timeout = timeout, minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy) diff -r 538cf3fdfe4d -r ff01d3ae9ad4 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 22:28:39 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri May 14 22:29:50 2010 +0200 @@ -569,7 +569,7 @@ fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) = (j, line :: lines) - | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees + | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees (Inference (num, t, deps)) (j, lines) = (j + 1, if is_axiom_clause_number thm_names num orelse @@ -579,7 +579,7 @@ not (exists_subterm (is_bad_free frees) t) andalso not (is_trivial_formula t) andalso (null lines orelse (* last line must be kept *) - (length deps >= 2 andalso j mod shrink_factor = 0))) then + (length deps >= 2 andalso j mod isar_shrink_factor = 0))) then Inference (num, t, deps) :: lines (* keep line *) else map (replace_deps_in_line (num, deps)) lines) (* drop line *) @@ -674,7 +674,7 @@ forall_vars t, ByMetis (fold (add_fact_from_dep thm_names) deps ([], []))) -fun proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof +fun proof_from_atp_proof pool ctxt full_types isar_shrink_factor atp_proof conjecture_shape thm_names params frees = let val lines = @@ -683,7 +683,7 @@ |> decode_lines ctxt full_types |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names) |> rpair [] |-> fold_rev add_nontrivial_line - |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor + |> rpair (0, []) |-> fold_rev (add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees) |> snd in @@ -981,7 +981,7 @@ do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" in do_proof end -fun isar_proof_text (pool, debug, full_types, shrink_factor, ctxt, +fun isar_proof_text (pool, debug, full_types, isar_shrink_factor, ctxt, conjecture_shape) (minimize_command, atp_proof, thm_names, goal, i) = let @@ -992,8 +992,9 @@ val (one_line_proof, lemma_names) = metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) fun isar_proof_for () = - case proof_from_atp_proof pool ctxt full_types shrink_factor atp_proof - conjecture_shape thm_names params frees + case proof_from_atp_proof pool ctxt full_types isar_shrink_factor + atp_proof conjecture_shape thm_names params + frees |> redirect_proof thy conjecture_shape hyp_ts concl_t |> kill_duplicate_assumptions_in_proof |> then_chain_proof