# HG changeset patch # User blanchet # Date 1303403962 -7200 # Node ID 8e5438dc70bb9add054687bfbbdbab1230337437 # Parent 724e612ba2481d24a263eafb56b0ffcff4fc3619 cleanup: get rid of "may_slice" arguments without changing semantics diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Apr 21 18:39:22 2011 +0200 @@ -317,13 +317,13 @@ fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ()) -fun get_prover ctxt slicing args = +fun get_prover ctxt args = let fun default_prover_name () = hd (#provers (Sledgehammer_Isar.default_params ctxt [])) handle Empty => error "No ATP available." fun get_prover name = - (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name) + (name, Sledgehammer_Run.get_minimizing_prover ctxt false name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name @@ -429,7 +429,7 @@ val triv_str = if trivial then "[T] " else "" val _ = change_data id inc_sh_calls val _ = if trivial then () else change_data id inc_sh_nontriv_calls - val (prover_name, prover) = get_prover (Proof.context_of st) true args + val (prover_name, prover) = get_prover (Proof.context_of st) args val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart" val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" val dir = AList.lookup (op =) args keepK @@ -473,7 +473,7 @@ let val ctxt = Proof.context_of st val n0 = length (these (!named_thms)) - val (prover_name, _) = get_prover ctxt false args + val (prover_name, _) = get_prover ctxt args val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart" val timeout = AList.lookup (op =) args minimize_timeoutK diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:39:22 2011 +0200 @@ -254,7 +254,7 @@ val explicit_apply = 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 = lookup_bool "slicing" + val slicing = not auto andalso lookup_bool "slicing" val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout val expect = lookup_string "expect" in @@ -303,7 +303,7 @@ in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params false ctxt override_params) false true i + run_sledgehammer (get_params false ctxt override_params) false i relevance_override (minimize_command override_params i) state |> K () @@ -376,7 +376,7 @@ fun auto_sledgehammer state = let val ctxt = Proof.context_of state in - run_sledgehammer (get_params true ctxt []) true false 1 + run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override (minimize_command [] 1) state end diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Apr 21 18:39:22 2011 +0200 @@ -147,7 +147,7 @@ silent i n state facts = let val ctxt = Proof.context_of state - val prover = get_prover ctxt false false prover_name + val prover = get_prover ctxt false prover_name val msecs = Time.toMilliseconds timeout val _ = print silent (fn () => "Sledgehammer minimize: " ^ quote prover_name ^ ".") diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:39:22 2011 +0200 @@ -93,7 +93,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val get_prover : Proof.context -> bool -> bool -> string -> prover + val get_prover : Proof.context -> bool -> string -> prover val setup : theory -> theory end; @@ -334,7 +334,7 @@ them each time. *) val atp_important_message_keep_factor = 0.1 -fun run_atp auto may_slice name +fun run_atp auto name ({exec, required_execs, arguments, slices, proof_delims, known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config) ({debug, verbose, overlord, max_relevant, monomorphize, @@ -345,7 +345,6 @@ val thy = Proof.theory_of state val ctxt = Proof.context_of state val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal - val slicing = may_slice andalso slicing fun monomorphize_facts facts = let val repair_context = @@ -566,13 +565,11 @@ val smt_slice_time_frac = Unsynchronized.ref 0.5 val smt_slice_min_secs = Unsynchronized.ref 5 -fun smt_filter_loop may_slice name - ({debug, verbose, overlord, monomorphize_limit, timeout, - slicing, ...} : params) +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit, + timeout, slicing, ...} : params) state i smt_filter = let val ctxt = Proof.context_of state - val slicing = may_slice andalso slicing val max_slices = if slicing then !smt_max_slices else 1 val repair_context = select_smt_solver name @@ -684,8 +681,7 @@ (Config.put Metis_Tactics.verbose debug #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i -fun run_smt_solver auto may_slice name (params as {debug, verbose, ...}) - minimize_command +fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command ({state, subgoal, subgoal_count, facts, smt_filter, ...} : prover_problem) = let @@ -695,7 +691,7 @@ val facts = facts ~~ (0 upto num_facts - 1) |> map (smt_weighted_fact thy num_facts) val {outcome, used_facts, run_time_in_msecs} = - smt_filter_loop may_slice name params state subgoal smt_filter facts + smt_filter_loop name params state subgoal smt_filter facts val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts) val outcome = outcome |> Option.map failure_from_smt_failure val message = @@ -727,12 +723,12 @@ run_time_in_msecs = run_time_in_msecs, message = message} end -fun get_prover ctxt auto may_slice name = +fun get_prover ctxt auto name = let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then - run_smt_solver auto may_slice name + run_smt_solver auto name else if member (op =) (supported_atps thy) name then - run_atp auto may_slice name (get_atp thy name) + run_atp auto name (get_atp thy name) else error ("No such prover: " ^ name ^ ".") end diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Apr 21 18:39:22 2011 +0200 @@ -14,10 +14,10 @@ type prover = Sledgehammer_Provers.prover val auto_minimize_min_facts : int Unsynchronized.ref - val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover + val get_minimizing_prover : Proof.context -> bool -> string -> prover val run_sledgehammer : - params -> bool -> bool -> int -> relevance_override - -> (string -> minimize_command) -> Proof.state -> bool * Proof.state + params -> bool -> int -> relevance_override -> (string -> minimize_command) + -> Proof.state -> bool * Proof.state end; structure Sledgehammer_Run : SLEDGEHAMMER_RUN = @@ -44,10 +44,10 @@ val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts) -fun get_minimizing_prover ctxt auto may_slice name +fun get_minimizing_prover ctxt auto name (params as {debug, verbose, explicit_apply, ...}) minimize_command (problem as {state, subgoal, subgoal_count, facts, ...}) = - get_prover ctxt auto may_slice name params minimize_command problem + get_prover ctxt auto name params minimize_command problem |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => if is_some outcome then result @@ -85,11 +85,10 @@ fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, expect, ...}) - auto may_slice minimize_command only + auto minimize_command only {state, goal, subgoal, subgoal_count, facts, smt_filter} name = let val ctxt = Proof.context_of state - val slicing = may_slice andalso slicing val birth_time = Time.now () val death_time = Time.+ (birth_time, timeout) val max_relevant = @@ -104,8 +103,7 @@ smt_filter = smt_filter} fun really_go () = problem - |> get_minimizing_prover ctxt auto may_slice name params - (minimize_command name) + |> get_minimizing_prover ctxt auto name params (minimize_command name) |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some" (* sic *), message)) fun go () = @@ -170,8 +168,7 @@ fun run_sledgehammer (params as {debug, blocking, provers, monomorphize, type_sys, relevance_thresholds, max_relevant, slicing, timeout, ...}) - auto may_slice i (relevance_override as {only, ...}) - minimize_command state = + auto i (relevance_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." else case subgoal_count state of @@ -184,7 +181,6 @@ state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state val thy = Proof_Context.theory_of ctxt - val slicing = may_slice andalso slicing val {facts = chained_ths, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i val no_dangerous_types = types_dangerous_types type_sys @@ -205,7 +201,7 @@ facts = facts, smt_filter = maybe_smt_filter (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - val launch = launch_prover params auto may_slice minimize_command only + val launch = launch_prover params auto minimize_command only in if auto then fold (fn prover => fn (true, state) => (true, state) diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Thu Apr 21 18:39:22 2011 +0200 @@ -23,7 +23,7 @@ @ [("timeout", string_of_int (Time.toSeconds timeout))]) (* @ [("overlord", "true")] *) |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer_Provers.get_prover ctxt false true name + val prover = Sledgehammer_Provers.get_prover ctxt false name val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name val is_built_in_const =