handle non-auto try case of Sledgehammer better
authorblanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 430215910dd009d0e
parent 43020 abb5d1f907e4
child 43022 7d3ce43d9464
handle non-auto try case of Sledgehammer better
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
src/Tools/try.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -327,7 +327,8 @@
     1.4        hd (#provers (Sledgehammer_Isar.default_params ctxt []))
     1.5        handle Empty => error "No ATP available."
     1.6      fun get_prover name =
     1.7 -      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
     1.8 +      (name, Sledgehammer_Run.get_minimizing_prover ctxt
     1.9 +                Sledgehammer_Provers.Normal name)
    1.10    in
    1.11      (case AList.lookup (op =) args proverK of
    1.12        SOME name => get_prover name
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -232,7 +232,7 @@
     2.4  val infinity_time_in_secs = 60 * 60 * 24 * 365
     2.5  val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
     2.6  
     2.7 -fun extract_params auto default_params override_params =
     2.8 +fun extract_params mode default_params override_params =
     2.9    let
    2.10      val override_params = map unalias_raw_param override_params
    2.11      val raw_params = rev override_params @ rev default_params
    2.12 @@ -266,19 +266,19 @@
    2.13        case lookup name of
    2.14          SOME "smart" => NONE
    2.15        | _ => SOME (lookup_int name)
    2.16 -    val debug = not auto andalso lookup_bool "debug"
    2.17 -    val verbose = debug orelse (not auto andalso lookup_bool "verbose")
    2.18 +    val debug = mode <> Auto_Try andalso lookup_bool "debug"
    2.19 +    val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose")
    2.20      val overlord = lookup_bool "overlord"
    2.21      val blocking =
    2.22 -      Isabelle_Process.is_active () orelse auto orelse debug orelse
    2.23 +      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
    2.24        lookup_bool "blocking"
    2.25      val provers = lookup_string "provers" |> space_explode " "
    2.26 -                  |> auto ? single o hd
    2.27 +                  |> mode = Auto_Try ? single o hd
    2.28      val type_sys =
    2.29 -      if auto then
    2.30 +      if mode = Auto_Try then
    2.31          Smart_Type_Sys true
    2.32        else case lookup_string "type_sys" of
    2.33 -        "smart" => Smart_Type_Sys (lookup_bool "full_types")
    2.34 +        "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
    2.35        | s => Dumb_Type_Sys (type_sys_from_string s)
    2.36      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    2.37      val max_relevant = lookup_int_option "max_relevant"
    2.38 @@ -287,10 +287,11 @@
    2.39      val explicit_apply = lookup_bool "explicit_apply"
    2.40      val isar_proof = lookup_bool "isar_proof"
    2.41      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    2.42 -    val slicing = not auto andalso lookup_bool "slicing"
    2.43 -    val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout
    2.44 +    val slicing = mode <> Auto_Try andalso lookup_bool "slicing"
    2.45 +    val timeout =
    2.46 +      (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
    2.47      val preplay_timeout =
    2.48 -      if auto then Time.zeroTime
    2.49 +      if mode = Auto_Try then Time.zeroTime
    2.50        else lookup_time "preplay_timeout" |> the_timeout
    2.51      val expect = lookup_string "expect"
    2.52    in
    2.53 @@ -303,8 +304,8 @@
    2.54       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    2.55    end
    2.56  
    2.57 -fun get_params auto ctxt = extract_params auto (default_raw_params ctxt)
    2.58 -fun default_params thy = get_params false thy o map (apsnd single)
    2.59 +fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
    2.60 +fun default_params thy = get_params Normal thy o map (apsnd single)
    2.61  
    2.62  (* Sledgehammer the given subgoal *)
    2.63  
    2.64 @@ -328,14 +329,14 @@
    2.65    in
    2.66      if subcommand = runN then
    2.67        let val i = the_default 1 opt_i in
    2.68 -        run_sledgehammer (get_params false ctxt override_params) false i
    2.69 +        run_sledgehammer (get_params Normal ctxt override_params) Normal i
    2.70                           relevance_override (minimize_command override_params i)
    2.71                           state
    2.72          |> K ()
    2.73        end
    2.74      else if subcommand = minN then
    2.75 -      run_minimize (get_params false ctxt override_params) (the_default 1 opt_i)
    2.76 -                   (#add relevance_override) state
    2.77 +      run_minimize (get_params Minimize ctxt override_params)
    2.78 +                   (the_default 1 opt_i) (#add relevance_override) state
    2.79      else if subcommand = messagesN then
    2.80        messages opt_i
    2.81      else if subcommand = supported_proversN then
    2.82 @@ -406,9 +407,10 @@
    2.83  fun try_sledgehammer auto state =
    2.84    let
    2.85      val ctxt = Proof.context_of state
    2.86 +    val mode = if auto then Auto_Try else Try
    2.87      val i = 1
    2.88    in
    2.89 -    run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override
    2.90 +    run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override
    2.91                       (minimize_command [] i) state
    2.92    end
    2.93  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -152,7 +152,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 prover_name
     3.8 +    val prover = get_prover ctxt Minimize 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	Fri May 27 10:30:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     4.3 @@ -15,6 +15,8 @@
     4.4    type type_system = Sledgehammer_ATP_Translate.type_system
     4.5    type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
     4.6  
     4.7 +  datatype mode = Auto_Try | Try | Normal | Minimize
     4.8 +
     4.9    datatype rich_type_system =
    4.10      Dumb_Type_Sys of type_system |
    4.11      Smart_Type_Sys of bool
    4.12 @@ -97,7 +99,7 @@
    4.13    val kill_provers : unit -> unit
    4.14    val running_provers : unit -> unit
    4.15    val messages : int option -> unit
    4.16 -  val get_prover : Proof.context -> bool -> string -> prover
    4.17 +  val get_prover : Proof.context -> mode -> string -> prover
    4.18  end;
    4.19  
    4.20  structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS =
    4.21 @@ -114,6 +116,8 @@
    4.22  
    4.23  (** The Sledgehammer **)
    4.24  
    4.25 +datatype mode = Auto_Try | Try | Normal | Minimize
    4.26 +
    4.27  (* Identifier to distinguish Sledgehammer from other tools using
    4.28     "Async_Manager". *)
    4.29  val das_tool = "Sledgehammer"
    4.30 @@ -320,10 +324,13 @@
    4.31    |> Exn.release
    4.32    |> tap (after path)
    4.33  
    4.34 -fun proof_banner auto blocking name =
    4.35 -  if auto then "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
    4.36 -  else if blocking then quote name ^ " found a proof"
    4.37 -  else "Try this command"
    4.38 +fun proof_banner mode blocking name =
    4.39 +  case mode of
    4.40 +    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
    4.41 +  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    4.42 +  | Normal => if blocking then quote name ^ " found a proof"
    4.43 +              else "Try this command"
    4.44 +  | Minimize => "Try this command"
    4.45  
    4.46  val smt_triggers =
    4.47    Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    4.48 @@ -473,7 +480,7 @@
    4.49    #> Config.put SMT_Config.monomorph_limit max_mono_iters
    4.50    #> Config.put SMT_Config.monomorph_instances max_mono_instances
    4.51  
    4.52 -fun run_atp auto name
    4.53 +fun run_atp mode name
    4.54          ({exec, required_execs, arguments, proof_delims, known_failures,
    4.55            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    4.56          ({debug, verbose, overlord, blocking, type_sys, max_relevant,
    4.57 @@ -696,7 +703,7 @@
    4.58           (output, msecs, type_sys, atp_proof, outcome)) =
    4.59        with_path cleanup export run_on problem_path_name
    4.60      val important_message =
    4.61 -      if not auto andalso
    4.62 +      if mode = Normal andalso
    4.63           random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
    4.64          extract_important_message output
    4.65        else
    4.66 @@ -715,7 +722,7 @@
    4.67      val isar_params =
    4.68        (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
    4.69      val metis_params =
    4.70 -      (proof_banner auto blocking name, minimize_command, type_sys, atp_proof,
    4.71 +      (proof_banner mode blocking name, minimize_command, type_sys, atp_proof,
    4.72         facts_offset, fact_names, typed_helpers, goal, subgoal)
    4.73      val (outcome, (message, used_facts)) =
    4.74        case outcome of
    4.75 @@ -894,7 +901,7 @@
    4.76      | NONE => Preplay_Timed_Out
    4.77    end
    4.78  
    4.79 -fun run_smt_solver auto name
    4.80 +fun run_smt_solver mode name
    4.81          (params as {debug, verbose, blocking, preplay_timeout, ...})
    4.82          minimize_command
    4.83          ({state, subgoal, subgoal_count, facts, smt_filter, ...}
    4.84 @@ -920,7 +927,7 @@
    4.85                      else "smt_solver = " ^ maybe_quote name,
    4.86                      "smt", NONE)
    4.87          in
    4.88 -          try_command_line (proof_banner auto blocking name)
    4.89 +          try_command_line (proof_banner mode blocking name)
    4.90                (apply_on_subgoal settings subgoal subgoal_count ^
    4.91                 command_call method (map fst other_lemmas)) ^
    4.92            minimize_line minimize_command
    4.93 @@ -938,12 +945,12 @@
    4.94       run_time_in_msecs = run_time_in_msecs, message = message}
    4.95    end
    4.96  
    4.97 -fun get_prover ctxt auto name =
    4.98 +fun get_prover ctxt mode name =
    4.99    let val thy = Proof_Context.theory_of ctxt in
   4.100      if is_smt_prover ctxt name then
   4.101 -      run_smt_solver auto name
   4.102 +      run_smt_solver mode name
   4.103      else if member (op =) (supported_atps thy) name then
   4.104 -      run_atp auto name (get_atp thy name)
   4.105 +      run_atp mode name (get_atp thy name)
   4.106      else
   4.107        error ("No such prover: " ^ name ^ ".")
   4.108    end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4  sig
     5.5    type relevance_override = Sledgehammer_Filter.relevance_override
     5.6    type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
     5.7 +  type mode = Sledgehammer_Provers.mode
     5.8    type params = Sledgehammer_Provers.params
     5.9    type prover = Sledgehammer_Provers.prover
    5.10  
    5.11 @@ -18,9 +19,9 @@
    5.12    val timeoutN : string
    5.13    val unknownN : string
    5.14    val auto_minimize_min_facts : int Config.T
    5.15 -  val get_minimizing_prover : Proof.context -> bool -> string -> prover
    5.16 +  val get_minimizing_prover : Proof.context -> mode -> string -> prover
    5.17    val run_sledgehammer :
    5.18 -    params -> bool -> int -> relevance_override -> (string -> minimize_command)
    5.19 +    params -> mode -> int -> relevance_override -> (string -> minimize_command)
    5.20      -> Proof.state -> bool * (string * Proof.state)
    5.21  end;
    5.22  
    5.23 @@ -66,10 +67,10 @@
    5.24    Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
    5.25        (fn generic => Config.get_generic generic binary_min_facts)
    5.26  
    5.27 -fun get_minimizing_prover ctxt auto name
    5.28 +fun get_minimizing_prover ctxt mode name
    5.29          (params as {debug, verbose, explicit_apply, ...}) minimize_command
    5.30          (problem as {state, subgoal, subgoal_count, facts, ...}) =
    5.31 -  get_prover ctxt auto name params minimize_command problem
    5.32 +  get_prover ctxt mode name params minimize_command problem
    5.33    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    5.34           if is_some outcome then
    5.35             result
    5.36 @@ -108,7 +109,7 @@
    5.37  
    5.38  fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    5.39                                expect, ...})
    5.40 -        auto minimize_command only
    5.41 +        mode minimize_command only
    5.42          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    5.43    let
    5.44      val ctxt = Proof.context_of state
    5.45 @@ -127,7 +128,7 @@
    5.46         smt_filter = smt_filter}
    5.47      fun really_go () =
    5.48        problem
    5.49 -      |> get_minimizing_prover ctxt auto name params (minimize_command name)
    5.50 +      |> get_minimizing_prover ctxt mode name params (minimize_command name)
    5.51        |> (fn {outcome, message, ...} =>
    5.52               (if outcome = SOME ATP_Proof.TimedOut then timeoutN
    5.53                else if is_some outcome then noneN
    5.54 @@ -159,7 +160,7 @@
    5.55              warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
    5.56        in (outcome_code, message) end
    5.57    in
    5.58 -    if auto then
    5.59 +    if mode = Auto_Try then
    5.60        let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
    5.61          (outcome_code,
    5.62           state
    5.63 @@ -196,12 +197,12 @@
    5.64  fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
    5.65    | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
    5.66  
    5.67 -val auto_max_relevant_divisor = 2 (* FUDGE *)
    5.68 +val auto_try_max_relevant_divisor = 2 (* FUDGE *)
    5.69  
    5.70  fun run_sledgehammer (params as {debug, verbose, blocking, provers,
    5.71                                   relevance_thresholds, max_relevant, slicing,
    5.72                                   timeout, ...})
    5.73 -        auto i (relevance_override as {only, ...}) minimize_command state =
    5.74 +        mode i (relevance_override as {only, ...}) minimize_command state =
    5.75    if null provers then
    5.76      error "No prover is set."
    5.77    else case subgoal_count state of
    5.78 @@ -209,7 +210,7 @@
    5.79    | n =>
    5.80      let
    5.81        val _ = Proof.assert_backward state
    5.82 -      val print = if auto then K () else Output.urgent_message
    5.83 +      val print = if mode = Normal then Output.urgent_message else K ()
    5.84        val state =
    5.85          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    5.86        val ctxt = Proof.context_of state
    5.87 @@ -234,11 +235,11 @@
    5.88               facts = facts,
    5.89               smt_filter = maybe_smt_filter
    5.90                    (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    5.91 -          val launch = launch_prover params auto minimize_command only
    5.92 +          val launch = launch_prover params mode minimize_command only
    5.93          in
    5.94 -          if auto then
    5.95 +          if mode = Auto_Try orelse mode = Try then
    5.96              (unknownN, state)
    5.97 -            |> fold (fn prover => fn accum as (outcome_code, state) =>
    5.98 +            |> fold (fn prover => fn accum as (outcome_code, _) =>
    5.99                          if outcome_code = someN then accum
   5.100                          else launch problem prover)
   5.101                      provers
   5.102 @@ -257,7 +258,8 @@
   5.103                0 |> fold (Integer.max
   5.104                           o default_max_relevant_for_prover ctxt slicing)
   5.105                          provers
   5.106 -                |> auto ? (fn n => n div auto_max_relevant_divisor)
   5.107 +                |> mode = Auto_Try
   5.108 +                   ? (fn n => n div auto_try_max_relevant_divisor)
   5.109            val is_built_in_const =
   5.110              is_built_in_const_for_prover ctxt (hd provers)
   5.111          in
   5.112 @@ -315,12 +317,15 @@
   5.113          launch_atps "Unit equational provers" is_unit_equality ueq_atps
   5.114        fun launch_atps_and_smt_solvers () =
   5.115          [launch_full_atps, launch_ueq_atps, launch_smts]
   5.116 -        |> smart_par_list_map (fn f => f (unknownN, state) |> K ())
   5.117 +        |> smart_par_list_map (fn f => ignore (f (unknownN, state)))
   5.118          handle ERROR msg => (print ("Error: " ^ msg); error msg)
   5.119 +      fun maybe f (accum as (outcome_code, _)) =
   5.120 +        accum |> (mode = Normal orelse outcome_code <> someN) ? f
   5.121      in
   5.122        (unknownN, state)
   5.123        |> (if blocking then
   5.124 -            launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
   5.125 +            launch_full_atps
   5.126 +            #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
   5.127            else
   5.128              (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
   5.129        handle TimeLimit.TimeOut =>
     6.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:08 2011 +0200
     6.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Fri May 27 10:30:08 2011 +0200
     6.3 @@ -23,7 +23,8 @@
     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 name
     6.8 +    val prover =
     6.9 +      Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name
    6.10      val default_max_relevant =
    6.11        Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name
    6.12      val is_built_in_const =
     7.1 --- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     7.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
     7.3 @@ -57,6 +57,7 @@
     7.4  
     7.5  fun try_tools state =
     7.6    get_tools (Proof.theory_of state)
     7.7 +  |> tap (fn _ => Output.urgent_message "Trying...")
     7.8    |> Par_List.get_some
     7.9           (fn (name, (_, tool)) =>
    7.10               case try (tool false) state of