cleanup: get rid of "may_slice" arguments without changing semantics
authorblanchet
Thu Apr 21 18:39:22 2011 +0200 (2011-04-21)
changeset 424448e5438dc70bb
parent 42443 724e612ba248
child 42445 c6ea64ebb8c5
cleanup: get rid of "may_slice" arguments without changing semantics
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/ex/sledgehammer_tactics.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 18:39:22 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Apr 21 18:39:22 2011 +0200
     1.3 @@ -317,13 +317,13 @@
     1.4  fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())
     1.5  
     1.6  
     1.7 -fun get_prover ctxt slicing args =
     1.8 +fun get_prover ctxt args =
     1.9    let
    1.10      fun default_prover_name () =
    1.11        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
    1.12        handle Empty => error "No ATP available."
    1.13      fun get_prover name =
    1.14 -      (name, Sledgehammer_Run.get_minimizing_prover ctxt false slicing name)
    1.15 +      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
    1.16    in
    1.17      (case AList.lookup (op =) args proverK of
    1.18        SOME name => get_prover name
    1.19 @@ -429,7 +429,7 @@
    1.20      val triv_str = if trivial then "[T] " else ""
    1.21      val _ = change_data id inc_sh_calls
    1.22      val _ = if trivial then () else change_data id inc_sh_nontriv_calls
    1.23 -    val (prover_name, prover) = get_prover (Proof.context_of st) true args
    1.24 +    val (prover_name, prover) = get_prover (Proof.context_of st) args
    1.25      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
    1.26      val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
    1.27      val dir = AList.lookup (op =) args keepK
    1.28 @@ -473,7 +473,7 @@
    1.29    let
    1.30      val ctxt = Proof.context_of st
    1.31      val n0 = length (these (!named_thms))
    1.32 -    val (prover_name, _) = get_prover ctxt false args
    1.33 +    val (prover_name, _) = get_prover ctxt args
    1.34      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
    1.35      val timeout =
    1.36        AList.lookup (op =) args minimize_timeoutK
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:39:22 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:39:22 2011 +0200
     2.3 @@ -254,7 +254,7 @@
     2.4      val explicit_apply = lookup_bool "explicit_apply"
     2.5      val isar_proof = lookup_bool "isar_proof"
     2.6      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     2.7 -    val slicing = lookup_bool "slicing"
     2.8 +    val slicing = not auto andalso lookup_bool "slicing"
     2.9      val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    2.10      val expect = lookup_string "expect"
    2.11    in
    2.12 @@ -303,7 +303,7 @@
    2.13    in
    2.14      if subcommand = runN then
    2.15        let val i = the_default 1 opt_i in
    2.16 -        run_sledgehammer (get_params false ctxt override_params) false true i
    2.17 +        run_sledgehammer (get_params false ctxt override_params) false i
    2.18                           relevance_override (minimize_command override_params i)
    2.19                           state
    2.20          |> K ()
    2.21 @@ -376,7 +376,7 @@
    2.22  
    2.23  fun auto_sledgehammer state =
    2.24    let val ctxt = Proof.context_of state in
    2.25 -    run_sledgehammer (get_params true ctxt []) true false 1
    2.26 +    run_sledgehammer (get_params true ctxt []) true 1
    2.27                       no_relevance_override (minimize_command [] 1) state
    2.28    end
    2.29  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Apr 21 18:39:22 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Apr 21 18:39:22 2011 +0200
     3.3 @@ -147,7 +147,7 @@
     3.4                     silent i n state facts =
     3.5    let
     3.6      val ctxt = Proof.context_of state
     3.7 -    val prover = get_prover ctxt false false prover_name
     3.8 +    val prover = get_prover ctxt false prover_name
     3.9      val msecs = Time.toMilliseconds timeout
    3.10      val _ = print silent (fn () => "Sledgehammer minimize: " ^
    3.11                                     quote prover_name ^ ".")
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:39:22 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:39:22 2011 +0200
     4.3 @@ -93,7 +93,7 @@
     4.4    val kill_provers : unit -> unit
     4.5    val running_provers : unit -> unit
     4.6    val messages : int option -> unit
     4.7 -  val get_prover : Proof.context -> bool -> bool -> string -> prover
     4.8 +  val get_prover : Proof.context -> bool -> string -> prover
     4.9    val setup : theory -> theory
    4.10  end;
    4.11  
    4.12 @@ -334,7 +334,7 @@
    4.13     them each time. *)
    4.14  val atp_important_message_keep_factor = 0.1
    4.15  
    4.16 -fun run_atp auto may_slice name
    4.17 +fun run_atp auto name
    4.18          ({exec, required_execs, arguments, slices, proof_delims, known_failures,
    4.19            explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
    4.20          ({debug, verbose, overlord, max_relevant, monomorphize,
    4.21 @@ -345,7 +345,6 @@
    4.22      val thy = Proof.theory_of state
    4.23      val ctxt = Proof.context_of state
    4.24      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    4.25 -    val slicing = may_slice andalso slicing
    4.26      fun monomorphize_facts facts =
    4.27        let
    4.28          val repair_context =
    4.29 @@ -566,13 +565,11 @@
    4.30  val smt_slice_time_frac = Unsynchronized.ref 0.5
    4.31  val smt_slice_min_secs = Unsynchronized.ref 5
    4.32  
    4.33 -fun smt_filter_loop may_slice name
    4.34 -                    ({debug, verbose, overlord, monomorphize_limit, timeout,
    4.35 -                      slicing, ...} : params)
    4.36 +fun smt_filter_loop name ({debug, verbose, overlord, monomorphize_limit,
    4.37 +                           timeout, slicing, ...} : params)
    4.38                      state i smt_filter =
    4.39    let
    4.40      val ctxt = Proof.context_of state
    4.41 -    val slicing = may_slice andalso slicing
    4.42      val max_slices = if slicing then !smt_max_slices else 1
    4.43      val repair_context =
    4.44        select_smt_solver name
    4.45 @@ -684,8 +681,7 @@
    4.46              (Config.put Metis_Tactics.verbose debug
    4.47               #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
    4.48  
    4.49 -fun run_smt_solver auto may_slice name (params as {debug, verbose, ...})
    4.50 -                   minimize_command
    4.51 +fun run_smt_solver auto name (params as {debug, verbose, ...}) minimize_command
    4.52                     ({state, subgoal, subgoal_count, facts, smt_filter, ...}
    4.53                      : prover_problem) =
    4.54    let
    4.55 @@ -695,7 +691,7 @@
    4.56      val facts = facts ~~ (0 upto num_facts - 1)
    4.57                  |> map (smt_weighted_fact thy num_facts)
    4.58      val {outcome, used_facts, run_time_in_msecs} =
    4.59 -      smt_filter_loop may_slice name params state subgoal smt_filter facts
    4.60 +      smt_filter_loop name params state subgoal smt_filter facts
    4.61      val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
    4.62      val outcome = outcome |> Option.map failure_from_smt_failure
    4.63      val message =
    4.64 @@ -727,12 +723,12 @@
    4.65       run_time_in_msecs = run_time_in_msecs, message = message}
    4.66    end
    4.67  
    4.68 -fun get_prover ctxt auto may_slice name =
    4.69 +fun get_prover ctxt auto name =
    4.70    let val thy = Proof_Context.theory_of ctxt in
    4.71      if is_smt_prover ctxt name then
    4.72 -      run_smt_solver auto may_slice name
    4.73 +      run_smt_solver auto name
    4.74      else if member (op =) (supported_atps thy) name then
    4.75 -      run_atp auto may_slice name (get_atp thy name)
    4.76 +      run_atp auto name (get_atp thy name)
    4.77      else
    4.78        error ("No such prover: " ^ name ^ ".")
    4.79    end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     5.3 @@ -14,10 +14,10 @@
     5.4    type prover = Sledgehammer_Provers.prover
     5.5  
     5.6    val auto_minimize_min_facts : int Unsynchronized.ref
     5.7 -  val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover
     5.8 +  val get_minimizing_prover : Proof.context -> bool -> string -> prover
     5.9    val run_sledgehammer :
    5.10 -    params -> bool -> bool -> int -> relevance_override
    5.11 -    -> (string -> minimize_command) -> Proof.state -> bool * Proof.state
    5.12 +    params -> bool -> int -> relevance_override -> (string -> minimize_command)
    5.13 +    -> Proof.state -> bool * Proof.state
    5.14  end;
    5.15  
    5.16  structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
    5.17 @@ -44,10 +44,10 @@
    5.18  
    5.19  val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
    5.20  
    5.21 -fun get_minimizing_prover ctxt auto may_slice name
    5.22 +fun get_minimizing_prover ctxt auto name
    5.23          (params as {debug, verbose, explicit_apply, ...}) minimize_command
    5.24          (problem as {state, subgoal, subgoal_count, facts, ...}) =
    5.25 -  get_prover ctxt auto may_slice name params minimize_command problem
    5.26 +  get_prover ctxt auto name params minimize_command problem
    5.27    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    5.28           if is_some outcome then
    5.29             result
    5.30 @@ -85,11 +85,10 @@
    5.31  
    5.32  fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    5.33                                expect, ...})
    5.34 -        auto may_slice minimize_command only
    5.35 +        auto minimize_command only
    5.36          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    5.37    let
    5.38      val ctxt = Proof.context_of state
    5.39 -    val slicing = may_slice andalso slicing
    5.40      val birth_time = Time.now ()
    5.41      val death_time = Time.+ (birth_time, timeout)
    5.42      val max_relevant =
    5.43 @@ -104,8 +103,7 @@
    5.44         smt_filter = smt_filter}
    5.45      fun really_go () =
    5.46        problem
    5.47 -      |> get_minimizing_prover ctxt auto may_slice name params
    5.48 -                               (minimize_command name)
    5.49 +      |> get_minimizing_prover ctxt auto name params (minimize_command name)
    5.50        |> (fn {outcome, message, ...} =>
    5.51               (if is_some outcome then "none" else "some" (* sic *), message))
    5.52      fun go () =
    5.53 @@ -170,8 +168,7 @@
    5.54  fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
    5.55                                   type_sys, relevance_thresholds, max_relevant,
    5.56                                   slicing, timeout, ...})
    5.57 -                     auto may_slice i (relevance_override as {only, ...})
    5.58 -                     minimize_command state =
    5.59 +        auto i (relevance_override as {only, ...}) minimize_command state =
    5.60    if null provers then
    5.61      error "No prover is set."
    5.62    else case subgoal_count state of
    5.63 @@ -184,7 +181,6 @@
    5.64          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    5.65        val ctxt = Proof.context_of state
    5.66        val thy = Proof_Context.theory_of ctxt
    5.67 -      val slicing = may_slice andalso slicing
    5.68        val {facts = chained_ths, goal, ...} = Proof.goal state
    5.69        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    5.70        val no_dangerous_types = types_dangerous_types type_sys
    5.71 @@ -205,7 +201,7 @@
    5.72               facts = facts,
    5.73               smt_filter = maybe_smt_filter
    5.74                    (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    5.75 -          val launch = launch_prover params auto may_slice minimize_command only
    5.76 +          val launch = launch_prover params auto minimize_command only
    5.77          in
    5.78            if auto then
    5.79              fold (fn prover => fn (true, state) => (true, state)
     6.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     6.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Thu Apr 21 18:39:22 2011 +0200
     6.3 @@ -23,7 +23,7 @@
     6.4         @ [("timeout", string_of_int (Time.toSeconds timeout))])
     6.5         (* @ [("overlord", "true")] *)
     6.6        |> Sledgehammer_Isar.default_params ctxt
     6.7 -    val prover = Sledgehammer_Provers.get_prover ctxt false true name
     6.8 +    val prover = Sledgehammer_Provers.get_prover ctxt false name
     6.9      val default_max_relevant =
    6.10        Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    6.11      val is_built_in_const =