# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID 5910dd009d0e4ddfa521a82f7cca8b55b4ebb19d # Parent abb5d1f907e488a6759094296e5f21c720e548fb handle non-auto try case of Sledgehammer better diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200 @@ -327,7 +327,8 @@ 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 name) + (name, Sledgehammer_Run.get_minimizing_prover ctxt + Sledgehammer_Provers.Normal name) in (case AList.lookup (op =) args proverK of SOME name => get_prover name diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200 @@ -232,7 +232,7 @@ val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) -fun extract_params auto default_params override_params = +fun extract_params mode default_params override_params = let val override_params = map unalias_raw_param override_params val raw_params = rev override_params @ rev default_params @@ -266,19 +266,19 @@ case lookup name of SOME "smart" => NONE | _ => SOME (lookup_int name) - val debug = not auto andalso lookup_bool "debug" - val verbose = debug orelse (not auto andalso lookup_bool "verbose") + val debug = mode <> Auto_Try andalso lookup_bool "debug" + val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") val overlord = lookup_bool "overlord" val blocking = - Isabelle_Process.is_active () orelse auto orelse debug orelse + Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" val provers = lookup_string "provers" |> space_explode " " - |> auto ? single o hd + |> mode = Auto_Try ? single o hd val type_sys = - if auto then + if mode = Auto_Try then Smart_Type_Sys true else case lookup_string "type_sys" of - "smart" => Smart_Type_Sys (lookup_bool "full_types") + "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types") | s => Dumb_Type_Sys (type_sys_from_string s) val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_int_option "max_relevant" @@ -287,10 +287,11 @@ 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 = not auto andalso lookup_bool "slicing" - val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout + val slicing = mode <> Auto_Try andalso lookup_bool "slicing" + val timeout = + (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout val preplay_timeout = - if auto then Time.zeroTime + if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout" |> the_timeout val expect = lookup_string "expect" in @@ -303,8 +304,8 @@ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} end -fun get_params auto ctxt = extract_params auto (default_raw_params ctxt) -fun default_params thy = get_params false thy o map (apsnd single) +fun get_params mode ctxt = extract_params mode (default_raw_params ctxt) +fun default_params thy = get_params Normal thy o map (apsnd single) (* Sledgehammer the given subgoal *) @@ -328,14 +329,14 @@ in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params false ctxt override_params) false i + run_sledgehammer (get_params Normal ctxt override_params) Normal i relevance_override (minimize_command override_params i) state |> K () end else if subcommand = minN then - run_minimize (get_params false ctxt override_params) (the_default 1 opt_i) - (#add relevance_override) state + run_minimize (get_params Minimize ctxt override_params) + (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = supported_proversN then @@ -406,9 +407,10 @@ fun try_sledgehammer auto state = let val ctxt = Proof.context_of state + val mode = if auto then Auto_Try else Try val i = 1 in - run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override + run_sledgehammer (get_params mode ctxt []) mode i no_relevance_override (minimize_command [] i) state end diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri May 27 10:30:08 2011 +0200 @@ -152,7 +152,7 @@ silent i n state facts = let val ctxt = Proof.context_of state - val prover = get_prover ctxt false prover_name + val prover = get_prover ctxt Minimize prover_name val msecs = Time.toMilliseconds timeout val _ = print silent (fn () => "Sledgehammer minimize: " ^ quote prover_name ^ ".") diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:08 2011 +0200 @@ -15,6 +15,8 @@ type type_system = Sledgehammer_ATP_Translate.type_system type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + datatype mode = Auto_Try | Try | Normal | Minimize + datatype rich_type_system = Dumb_Type_Sys of type_system | Smart_Type_Sys of bool @@ -97,7 +99,7 @@ val kill_provers : unit -> unit val running_provers : unit -> unit val messages : int option -> unit - val get_prover : Proof.context -> bool -> string -> prover + val get_prover : Proof.context -> mode -> string -> prover end; structure Sledgehammer_Provers : SLEDGEHAMMER_PROVERS = @@ -114,6 +116,8 @@ (** The Sledgehammer **) +datatype mode = Auto_Try | Try | Normal | Minimize + (* Identifier to distinguish Sledgehammer from other tools using "Async_Manager". *) val das_tool = "Sledgehammer" @@ -320,10 +324,13 @@ |> Exn.release |> tap (after path) -fun proof_banner auto blocking name = - if auto then "Auto Sledgehammer (" ^ quote name ^ ") found a proof" - else if blocking then quote name ^ " found a proof" - else "Try this command" +fun proof_banner mode blocking name = + case mode of + Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof" + | Try => "Sledgehammer (" ^ quote name ^ ") found a proof" + | Normal => if blocking then quote name ^ " found a proof" + else "Try this command" + | Minimize => "Try this command" val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) @@ -473,7 +480,7 @@ #> Config.put SMT_Config.monomorph_limit max_mono_iters #> Config.put SMT_Config.monomorph_instances max_mono_instances -fun run_atp auto name +fun run_atp mode name ({exec, required_execs, arguments, proof_delims, known_failures, conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config) ({debug, verbose, overlord, blocking, type_sys, max_relevant, @@ -696,7 +703,7 @@ (output, msecs, type_sys, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = - if not auto andalso + if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else @@ -715,7 +722,7 @@ val isar_params = (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab) val metis_params = - (proof_banner auto blocking name, minimize_command, type_sys, atp_proof, + (proof_banner mode blocking name, minimize_command, type_sys, atp_proof, facts_offset, fact_names, typed_helpers, goal, subgoal) val (outcome, (message, used_facts)) = case outcome of @@ -894,7 +901,7 @@ | NONE => Preplay_Timed_Out end -fun run_smt_solver auto name +fun run_smt_solver mode name (params as {debug, verbose, blocking, preplay_timeout, ...}) minimize_command ({state, subgoal, subgoal_count, facts, smt_filter, ...} @@ -920,7 +927,7 @@ else "smt_solver = " ^ maybe_quote name, "smt", NONE) in - try_command_line (proof_banner auto blocking name) + try_command_line (proof_banner mode blocking name) (apply_on_subgoal settings subgoal subgoal_count ^ command_call method (map fst other_lemmas)) ^ minimize_line minimize_command @@ -938,12 +945,12 @@ run_time_in_msecs = run_time_in_msecs, message = message} end -fun get_prover ctxt auto name = +fun get_prover ctxt mode name = let val thy = Proof_Context.theory_of ctxt in if is_smt_prover ctxt name then - run_smt_solver auto name + run_smt_solver mode name else if member (op =) (supported_atps thy) name then - run_atp auto name (get_atp thy name) + run_atp mode name (get_atp thy name) else error ("No such prover: " ^ name ^ ".") end diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri May 27 10:30:08 2011 +0200 @@ -10,6 +10,7 @@ sig type relevance_override = Sledgehammer_Filter.relevance_override type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command + type mode = Sledgehammer_Provers.mode type params = Sledgehammer_Provers.params type prover = Sledgehammer_Provers.prover @@ -18,9 +19,9 @@ val timeoutN : string val unknownN : string val auto_minimize_min_facts : int Config.T - val get_minimizing_prover : Proof.context -> bool -> string -> prover + val get_minimizing_prover : Proof.context -> mode -> string -> prover val run_sledgehammer : - params -> bool -> int -> relevance_override -> (string -> minimize_command) + params -> mode -> int -> relevance_override -> (string -> minimize_command) -> Proof.state -> bool * (string * Proof.state) end; @@ -66,10 +67,10 @@ Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts} (fn generic => Config.get_generic generic binary_min_facts) -fun get_minimizing_prover ctxt auto name +fun get_minimizing_prover ctxt mode name (params as {debug, verbose, explicit_apply, ...}) minimize_command (problem as {state, subgoal, subgoal_count, facts, ...}) = - get_prover ctxt auto name params minimize_command problem + get_prover ctxt mode name params minimize_command problem |> (fn result as {outcome, used_facts, run_time_in_msecs, message} => if is_some outcome then result @@ -108,7 +109,7 @@ fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, expect, ...}) - auto minimize_command only + mode minimize_command only {state, goal, subgoal, subgoal_count, facts, smt_filter} name = let val ctxt = Proof.context_of state @@ -127,7 +128,7 @@ smt_filter = smt_filter} fun really_go () = problem - |> get_minimizing_prover ctxt auto name params (minimize_command name) + |> get_minimizing_prover ctxt mode name params (minimize_command name) |> (fn {outcome, message, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN @@ -159,7 +160,7 @@ warning ("Unexpected outcome: " ^ quote outcome_code ^ "."); in (outcome_code, message) end in - if auto then + if mode = Auto_Try then let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in (outcome_code, state @@ -196,12 +197,12 @@ fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact" -val auto_max_relevant_divisor = 2 (* FUDGE *) +val auto_try_max_relevant_divisor = 2 (* FUDGE *) fun run_sledgehammer (params as {debug, verbose, blocking, provers, relevance_thresholds, max_relevant, slicing, timeout, ...}) - auto i (relevance_override as {only, ...}) minimize_command state = + mode i (relevance_override as {only, ...}) minimize_command state = if null provers then error "No prover is set." else case subgoal_count state of @@ -209,7 +210,7 @@ | n => let val _ = Proof.assert_backward state - val print = if auto then K () else Output.urgent_message + val print = if mode = Normal then Output.urgent_message else K () val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug) val ctxt = Proof.context_of state @@ -234,11 +235,11 @@ facts = facts, smt_filter = maybe_smt_filter (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - val launch = launch_prover params auto minimize_command only + val launch = launch_prover params mode minimize_command only in - if auto then + if mode = Auto_Try orelse mode = Try then (unknownN, state) - |> fold (fn prover => fn accum as (outcome_code, state) => + |> fold (fn prover => fn accum as (outcome_code, _) => if outcome_code = someN then accum else launch problem prover) provers @@ -257,7 +258,8 @@ 0 |> fold (Integer.max o default_max_relevant_for_prover ctxt slicing) provers - |> auto ? (fn n => n div auto_max_relevant_divisor) + |> mode = Auto_Try + ? (fn n => n div auto_try_max_relevant_divisor) val is_built_in_const = is_built_in_const_for_prover ctxt (hd provers) in @@ -315,12 +317,15 @@ launch_atps "Unit equational provers" is_unit_equality ueq_atps fun launch_atps_and_smt_solvers () = [launch_full_atps, launch_ueq_atps, launch_smts] - |> smart_par_list_map (fn f => f (unknownN, state) |> K ()) + |> smart_par_list_map (fn f => ignore (f (unknownN, state))) handle ERROR msg => (print ("Error: " ^ msg); error msg) + fun maybe f (accum as (outcome_code, _)) = + accum |> (mode = Normal orelse outcome_code <> someN) ? f in (unknownN, state) |> (if blocking then - launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts) + launch_full_atps + #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts) else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) handle TimeLimit.TimeOut => diff -r abb5d1f907e4 -r 5910dd009d0e src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Fri May 27 10:30:08 2011 +0200 @@ -23,7 +23,8 @@ @ [("timeout", string_of_int (Time.toSeconds timeout))]) (* @ [("overlord", "true")] *) |> Sledgehammer_Isar.default_params ctxt - val prover = Sledgehammer_Provers.get_prover ctxt false name + val prover = + Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing name val is_built_in_const = diff -r abb5d1f907e4 -r 5910dd009d0e src/Tools/try.ML --- a/src/Tools/try.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/Tools/try.ML Fri May 27 10:30:08 2011 +0200 @@ -57,6 +57,7 @@ fun try_tools state = get_tools (Proof.theory_of state) + |> tap (fn _ => Output.urgent_message "Trying...") |> Par_List.get_some (fn (name, (_, tool)) => case try (tool false) state of