# HG changeset patch # User blanchet # Date 1306485008 -7200 # Node ID abb5d1f907e488a6759094296e5f21c720e548fb # Parent 619f16bf2150611f0d0f5540567255587ad048fb added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods diff -r 619f16bf2150 -r abb5d1f907e4 etc/isar-keywords.el --- a/etc/isar-keywords.el Fri May 27 10:30:08 2011 +0200 +++ b/etc/isar-keywords.el Fri May 27 10:30:08 2011 +0200 @@ -253,6 +253,7 @@ "thy_deps" "translations" "try" + "try_methods" "txt" "txt_raw" "typ" @@ -411,6 +412,7 @@ "thm_deps" "thy_deps" "try" + "try_methods" "typ" "unused_thms" "value" diff -r 619f16bf2150 -r abb5d1f907e4 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 @@ -582,7 +582,8 @@ Unsynchronized.ref (NONE : ((string * locality) * thm list) list option) val minimize = AList.defined (op =) args minimizeK val metis_ft = AList.defined (op =) args metis_ftK - val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre + val trivial = + Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre handle TimeLimit.TimeOut => false fun apply_reconstructor m1 m2 = if metis_ft diff -r 619f16bf2150 -r abb5d1f907e4 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri May 27 10:30:08 2011 +0200 @@ -55,6 +55,11 @@ batch_size: int, expect: string} + val genuineN : string + val quasi_genuineN : string + val potentialN : string + val noneN : string + val unknownN : string val register_frac_type : string -> (string * string) list -> theory -> theory val unregister_frac_type : string -> theory -> theory val register_codatatype : typ -> string -> styp list -> theory -> theory @@ -131,6 +136,12 @@ batch_size: int, expect: string} +val genuineN = "genuine" +val quasi_genuineN = "quasi_genuine" +val potentialN = "potential" +val noneN = "none" +val unknownN = "unknown" + (* TODO: eliminate these historical aliases *) val register_frac_type = Nitpick_HOL.register_frac_type_global val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global @@ -973,7 +984,7 @@ fun run_batches _ _ [] (found_really_genuine, max_potential, max_genuine, donno) = if donno > 0 andalso max_genuine > 0 then - (print_m (fn () => excipit "checked"); "unknown") + (print_m (fn () => excipit "checked"); unknownN) else if max_genuine = original_max_genuine then if max_potential = original_max_potential then (print_m (fn () => @@ -982,7 +993,7 @@ " This suggests that the induction hypothesis might be \ \general enough to prove this subgoal." else - "")); if skipped > 0 then "unknown" else "none") + "")); if skipped > 0 then unknownN else noneN) else (print_m (fn () => excipit ("could not find a" ^ @@ -991,11 +1002,11 @@ else "ny better " ^ das_wort_model ^ "s.") ^ " It checked")); - "potential") + potentialN) else if found_really_genuine then - "genuine" + genuineN else - "quasi_genuine" + quasi_genuineN | run_batches j n (batch :: batches) z = let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in run_batches (j + 1) n (if max_genuine > 0 then batches else []) z @@ -1007,7 +1018,7 @@ (false, max_potential, max_genuine, 0) handle TimeLimit.TimeOut => (print_m (fn () => excipit "ran out of time after checking"); - if !met_potential > 0 then "potential" else "unknown") + if !met_potential > 0 then potentialN else unknownN) val _ = print_v (fn () => "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^ ".") @@ -1026,7 +1037,7 @@ ("no_kodkodi", state)) else let - val unknown_outcome = ("unknown", state) + val unknown_outcome = (unknownN, state) val deadline = Option.map (curry Time.+ (Time.now ())) timeout val outcome as (outcome_code, _) = time_limit (if debug orelse is_none timeout then NONE @@ -1065,7 +1076,7 @@ val t = state |> Proof.raw_goal |> #goal |> prop_of in case Logic.count_prems t of - 0 => (Output.urgent_message "No subgoal!"; ("none", state)) + 0 => (Output.urgent_message "No subgoal!"; (noneN, state)) | n => let val t = Logic.goal_params t i |> fst diff -r 619f16bf2150 -r abb5d1f907e4 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri May 27 10:30:08 2011 +0200 @@ -10,6 +10,8 @@ sig type params = Nitpick.params + val nitpickN : string + val nitpick_paramsN : string val auto : bool Unsynchronized.ref val default_params : theory -> (string * string) list -> params val setup : theory -> theory @@ -24,6 +26,9 @@ open Nitpick_Nut open Nitpick +val nitpickN = "nitpick" +val nitpick_paramsN = "nitpick_params" + val auto = Unsynchronized.ref false (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share @@ -356,18 +361,18 @@ val params as {blocking, debug, ...} = extract_params ctxt auto (default_raw_params thy) override_params fun go () = - (false, state) + (unknownN, state) |> (if auto then perhaps o try else if debug then fn f => fn x => f x else handle_exceptions ctxt) - (fn (_, state) => pick_nits_in_subgoal state params auto i step - |>> curry (op =) "genuine") - in if blocking then go () else Future.fork (tap go) |> K (false, state) end + (fn (_, state) => pick_nits_in_subgoal state params auto i step) + in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end + |> `(fn (outcome_code, _) => outcome_code = genuineN) fun nitpick_trans (params, i) = - Toplevel.keep (fn st => - (pick_nits params false i (Toplevel.proof_position_of st) - (Toplevel.proof_of st); ())) + Toplevel.keep (fn state => + pick_nits params false i (Toplevel.proof_position_of state) + (Toplevel.proof_of state) |> K ()) fun string_for_raw_param (name, value) = name ^ " = " ^ stringify_raw_param_value value @@ -388,15 +393,15 @@ (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans val parse_nitpick_params_command = parse_params #>> nitpick_params_trans -val _ = Outer_Syntax.improper_command "nitpick" +val _ = Outer_Syntax.improper_command nitpickN "try to find a counterexample for a given subgoal using Nitpick" Keyword.diag parse_nitpick_command -val _ = Outer_Syntax.command "nitpick_params" +val _ = Outer_Syntax.command nitpick_paramsN "set and display the default parameters for Nitpick" Keyword.thy_decl parse_nitpick_params_command -val auto_nitpick = pick_nits [] true 1 0 +fun try_nitpick auto = pick_nits [] auto 1 0 -val setup = Try.register_tool (auto, auto_nitpick) +val setup = Try.register_tool (nitpickN, (auto, try_nitpick)) end; diff -r 619f16bf2150 -r abb5d1f907e4 src/HOL/Tools/Nitpick/nitrox.ML --- a/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Fri May 27 10:30:08 2011 +0200 @@ -124,7 +124,7 @@ ("format", "1000"), ("max_potential", "0"), (* ("timeout", "240 s"), *) - ("expect", "genuine")] + ("expect", Nitpick.genuineN)] |> Nitpick_Isar.default_params @{theory} val auto = false val i = 1 diff -r 619f16bf2150 -r abb5d1f907e4 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 @@ -8,6 +8,7 @@ sig type params = Sledgehammer_Provers.params + val sledgehammerN : string val auto : bool Unsynchronized.ref val provers : string Unsynchronized.ref val timeout : int Unsynchronized.ref @@ -26,6 +27,17 @@ open Sledgehammer_Minimize open Sledgehammer_Run +val sledgehammerN = "sledgehammer" +val sledgehammer_paramsN = "sledgehammer_params" + +val runN = "run" +val minN = "min" +val messagesN = "messages" +val supported_proversN = "supported_provers" +val running_proversN = "running_provers" +val kill_proversN = "kill_provers" +val refresh_tptpN = "refresh_tptp" + val auto = Unsynchronized.ref false val _ = @@ -296,17 +308,6 @@ (* Sledgehammer the given subgoal *) -val sledgehammerN = "sledgehammer" -val sledgehammer_paramsN = "sledgehammer_params" - -val runN = "run" -val minN = "min" -val messagesN = "messages" -val supported_proversN = "supported_provers" -val running_proversN = "running_provers" -val kill_proversN = "kill_provers" -val refresh_tptpN = "refresh_tptp" - val is_raw_param_relevant_for_minimize = member (op =) params_for_minimize o fst o unalias_raw_param fun string_for_raw_param (key, values) = @@ -402,12 +403,15 @@ "set and display the default parameters for Sledgehammer" Keyword.thy_decl parse_sledgehammer_params_command -fun auto_sledgehammer state = - let val ctxt = Proof.context_of state in - run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override - (minimize_command [] 1) state +fun try_sledgehammer auto state = + let + val ctxt = Proof.context_of state + val i = 1 + in + run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override + (minimize_command [] i) state end -val setup = Try.register_tool (auto, auto_sledgehammer) +val setup = Try.register_tool (sledgehammerN, (auto, try_sledgehammer)) end; diff -r 619f16bf2150 -r abb5d1f907e4 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 @@ -13,11 +13,15 @@ type params = Sledgehammer_Provers.params type prover = Sledgehammer_Provers.prover + val someN : string + val noneN : string + val timeoutN : string + val unknownN : string val auto_minimize_min_facts : int Config.T val get_minimizing_prover : Proof.context -> bool -> string -> prover val run_sledgehammer : params -> bool -> int -> relevance_override -> (string -> minimize_command) - -> Proof.state -> bool * Proof.state + -> Proof.state -> bool * (string * Proof.state) end; structure Sledgehammer_Run : SLEDGEHAMMER_RUN = @@ -29,6 +33,22 @@ open Sledgehammer_Provers open Sledgehammer_Minimize +val someN = "some" +val noneN = "none" +val timeoutN = "timeout" +val unknownN = "unknown" + +val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN] + +fun max_outcome_code codes = + NONE + |> fold (fn candidate => + fn accum as SOME _ => accum + | NONE => if member (op =) codes candidate then SOME candidate + else NONE) + ordered_outcome_codes + |> the_default unknownN + fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal = (name, @@ -86,11 +106,6 @@ | NONE => result end) -val someN = "some" -val noneN = "none" -val timeoutN = "timeout" -val unknownN = "unknown" - fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout, expect, ...}) auto minimize_command only @@ -190,7 +205,7 @@ if null provers then error "No prover is set." else case subgoal_count state of - 0 => (Output.urgent_message "No subgoal!"; (false, state)) + 0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state))) | n => let val _ = Proof.assert_backward state @@ -219,18 +234,19 @@ facts = facts, smt_filter = maybe_smt_filter (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i} - fun launch problem = - launch_prover params auto minimize_command only problem - #>> curry (op =) someN + val launch = launch_prover params auto minimize_command only in if auto then - fold (fn prover => fn (true, state) => (true, state) - | (false, _) => launch problem prover) - provers (false, state) + (unknownN, state) + |> fold (fn prover => fn accum as (outcome_code, state) => + if outcome_code = someN then accum + else launch problem prover) + provers else provers - |> (if blocking then smart_par_list_map else map) (launch problem) - |> exists fst |> rpair state + |> (if blocking then smart_par_list_map else map) + (launch problem #> fst) + |> max_outcome_code |> rpair state end fun get_facts label is_appropriate_prop relevance_fudge provers = let @@ -290,24 +306,26 @@ in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =) - |> map (launch_provers state (K facts) weight smt_filter o snd) - |> exists fst |> rpair state + |> map (snd #> launch_provers state (K facts) weight smt_filter + #> fst) + |> max_outcome_code |> rpair state end val launch_full_atps = launch_atps "ATP" (K true) full_atps val launch_ueq_atps = 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 (false, state) |> K ()) + |> smart_par_list_map (fn f => f (unknownN, state) |> K ()) handle ERROR msg => (print ("Error: " ^ msg); error msg) in - (false, state) + (unknownN, state) |> (if blocking then launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts) else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p)) handle TimeLimit.TimeOut => - (print "Sledgehammer ran out of time."; (false, state)) + (print "Sledgehammer ran out of time."; (unknownN, state)) end + |> `(fn (outcome_code, _) => outcome_code = someN) end; diff -r 619f16bf2150 -r abb5d1f907e4 src/HOL/Tools/try_methods.ML --- a/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/HOL/Tools/try_methods.ML Fri May 27 10:30:08 2011 +0200 @@ -6,6 +6,8 @@ signature TRY_METHODS = sig + val try_methodsN : string + val noneN : string val auto : bool Unsynchronized.ref val try_methods : Time.time option -> string list * string list * string list * string list @@ -16,6 +18,10 @@ structure Try_Methods : TRY_METHODS = struct +val try_methodsN = "try_methods" + +val noneN = "none" + val auto = Unsynchronized.ref false val _ = @@ -109,7 +115,8 @@ in case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st) |> map_filter I |> sort (int_ord o pairself snd) of - [] => (if auto then () else writeln "No proof found."; (false, st)) + [] => (if auto then () else writeln "No proof found."; + (false, (noneN, st))) | xs as (s, _) :: _ => let val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s))) @@ -124,20 +131,18 @@ else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" in - (true, st |> (if auto then - Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.hilite - [Pretty.str message]]) - else - tap (fn _ => Output.urgent_message message))) + (true, (s, st |> (if auto then + Proof.goal_message + (fn () => Pretty.chunks [Pretty.str "", + Pretty.markup Markup.hilite + [Pretty.str message]]) + else + tap (fn _ => Output.urgent_message message)))) end end fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt -val try_methodsN = "try_methods" - fun try_methods_trans quad = Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad o Toplevel.proof_of) @@ -175,8 +180,8 @@ "try a combination of proof methods" Keyword.diag parse_try_methods_command -val auto_try_methods = do_try_methods true NONE ([], [], [], []) +fun try_try_methods auto = do_try_methods auto NONE ([], [], [], []) -val setup = Try.register_tool (auto, auto_try_methods) +val setup = Try.register_tool (try_methodsN, (auto, try_try_methods)) end; diff -r 619f16bf2150 -r abb5d1f907e4 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/Tools/quickcheck.ML Fri May 27 10:30:08 2011 +0200 @@ -6,6 +6,10 @@ signature QUICKCHECK = sig + val quickcheckN: string + val genuineN: string + val noneN: string + val unknownN: string val setup: theory -> theory (* configuration *) val auto: bool Unsynchronized.ref @@ -61,6 +65,13 @@ structure Quickcheck : QUICKCHECK = struct +val quickcheckN = "quickcheck" +val quickcheck_paramsN = "quickcheck_params" + +val genuineN = "genuine" +val noneN = "none" +val unknownN = "unknown" + (* preferences *) val auto = Unsynchronized.ref false; @@ -472,10 +483,11 @@ Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") :: map (fn (s, t) => Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex)) - @ (Pretty.str ("Evaluated terms:\n") :: - map (fn (t, u) => - Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) - (rev eval_terms))); + @ (if null eval_terms then [] + else (Pretty.str ("Evaluated terms:\n") :: + map (fn (t, u) => + Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u]) + (rev eval_terms)))); fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors, satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = @@ -511,27 +523,6 @@ (* map (pretty_reports ctxt) (reports_of result) :: *) (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) []) -(* automatic testing *) - -fun auto_quickcheck state = - let - val ctxt = Proof.context_of state; - val res = - state - |> Proof.map_context (Config.put report false #> Config.put quiet true) - |> try (test_goal (false, false) ([], []) 1); - in - case res of - NONE => (false, state) - | SOME (result :: _) => if found_counterexample result then - (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "", - Pretty.mark Markup.hilite (pretty_counterex ctxt true (response_of result))])) state) - else - (false, state) - end - -val setup = Try.register_tool (auto, auto_quickcheck) - (* Isar commands *) fun read_nat s = case (Library.read_int o Symbol.explode) s @@ -610,7 +601,8 @@ fun quickcheck_cmd args i state = gen_quickcheck args i (Toplevel.proof_of state) - |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false; + |> Output.urgent_message o Pretty.string_of + o pretty_counterex_and_reports (Toplevel.context_of state) false; val parse_arg = Parse.name -- @@ -622,15 +614,47 @@ Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed []; val _ = - Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl + Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args))); val _ = - Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag + Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i))); +(* automatic testing *) + +fun try_quickcheck auto state = + let + val ctxt = Proof.context_of state; + val i = 1; + val res = + state + |> Proof.map_context (Config.put report false #> Config.put quiet true) + |> try (test_goal (false, false) ([], []) i); + in + case res of + NONE => (unknownN, state) + | SOME results => + let + val msg = pretty_counterex_and_reports ctxt auto results + |> not auto ? tap (Output.urgent_message o Pretty.string_of) + in + if exists found_counterexample results then + (genuineN, + state |> (if auto then + Proof.goal_message (K (Pretty.chunks [Pretty.str "", + Pretty.mark Markup.hilite msg])) + else + I)) + else + (noneN, state) + end + end + |> `(fn (outcome_code, _) => outcome_code = genuineN) + +val setup = Try.register_tool (quickcheckN, (auto, try_quickcheck)) + end; - val auto_quickcheck = Quickcheck.auto; diff -r 619f16bf2150 -r abb5d1f907e4 src/Tools/solve_direct.ML --- a/src/Tools/solve_direct.ML Fri May 27 10:30:08 2011 +0200 +++ b/src/Tools/solve_direct.ML Fri May 27 10:30:08 2011 +0200 @@ -10,9 +10,13 @@ signature SOLVE_DIRECT = sig + val solve_directN: string + val someN: string + val noneN: string + val unknownN: string val auto: bool Unsynchronized.ref val max_solutions: int Unsynchronized.ref - val solve_direct: bool -> Proof.state -> bool * Proof.state + val solve_direct: bool -> Proof.state -> bool * (string * Proof.state) val setup: theory -> theory end; @@ -21,6 +25,9 @@ val solve_directN = "solve_direct"; +val someN = "some"; +val noneN = "none"; +val unknownN = "none"; (* preferences *) @@ -74,7 +81,7 @@ in (case try seek_against_goal () of SOME (SOME results) => - (true, + (someN, state |> (if auto then Proof.goal_message @@ -85,8 +92,10 @@ else tap (fn _ => Output.urgent_message (Pretty.string_of (Pretty.chunks (message results)))))) - | _ => (false, state)) - end; + | SOME NONE => (noneN, state) + | NONE => (unknownN, state)) + end + |> `(fn (outcome_code, _) => outcome_code = someN); val _ = Outer_Syntax.improper_command solve_directN @@ -97,8 +106,6 @@ (* hook *) -val auto_solve_direct = solve_direct true; - -val setup = Try.register_tool (auto, auto_solve_direct); +val setup = Try.register_tool (solve_directN, (auto, solve_direct)); end; diff -r 619f16bf2150 -r abb5d1f907e4 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 @@ -6,16 +6,28 @@ signature TRY = sig + type tool = + string * (bool Unsynchronized.ref + * (bool -> Proof.state -> bool * (string * Proof.state))) + + val tryN : string val auto_time_limit: real Unsynchronized.ref - val register_tool : - bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory - -> theory + val register_tool : tool -> theory -> theory + val get_tools : theory -> tool list + val try_tools : Proof.state -> (string * string) option end; structure Try : TRY = struct +type tool = + string * (bool Unsynchronized.ref + * (bool -> Proof.state -> bool * (string * Proof.state))) + +val tryN = "try" + + (* preferences *) val auto_time_limit = Unsynchronized.ref 4.0 @@ -31,24 +43,42 @@ structure Data = Theory_Data ( - type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list + type T = tool list val empty = [] val extend = I fun merge data : T = AList.merge (op =) (K true) data ) +val get_tools = Data.get + val register_tool = Data.map o AList.update (op =) +(* try command *) + +fun try_tools state = + get_tools (Proof.theory_of state) + |> Par_List.get_some + (fn (name, (_, tool)) => + case try (tool false) state of + SOME (true, (outcome_code, _)) => SOME (name, outcome_code) + | _ => NONE) + +val _ = + Outer_Syntax.improper_command tryN + "try a combination of automatic proving and disproving tools" Keyword.diag + (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of))) + -(* automatic testing *) +(* automatic try *) -fun run_tools tools state = - tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE) - |> Par_List.get_some (fn tool => - case try tool state of - SOME (true, state) => SOME state - | _ => NONE) - |> the_default state +fun auto_try state = + get_tools (Proof.theory_of state) + |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE) + |> Par_List.get_some (fn tool => + case try (tool true) state of + SOME (true, (_, state)) => SOME state + | _ => NONE) + |> the_default state (* Too large values are understood as milliseconds, ensuring compatibility with old setting files. No users can possibly in their right mind want the user @@ -62,8 +92,7 @@ val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state => if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then - TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) - (run_tools (Data.get (Proof.theory_of state))) state + TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state handle TimeLimit.TimeOut => state else state))