added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
authorblanchet
Fri May 27 10:30:08 2011 +0200 (2011-05-27)
changeset 43020abb5d1f907e4
parent 43019 619f16bf2150
child 43021 5910dd009d0e
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
etc/isar-keywords.el
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Nitpick/nitrox.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
src/HOL/Tools/try_methods.ML
src/Tools/quickcheck.ML
src/Tools/solve_direct.ML
src/Tools/try.ML
     1.1 --- a/etc/isar-keywords.el	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/etc/isar-keywords.el	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -253,6 +253,7 @@
     1.4      "thy_deps"
     1.5      "translations"
     1.6      "try"
     1.7 +    "try_methods"
     1.8      "txt"
     1.9      "txt_raw"
    1.10      "typ"
    1.11 @@ -411,6 +412,7 @@
    1.12      "thm_deps"
    1.13      "thy_deps"
    1.14      "try"
    1.15 +    "try_methods"
    1.16      "typ"
    1.17      "unused_thms"
    1.18      "value"
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -582,7 +582,8 @@
     2.4          Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
     2.5        val minimize = AList.defined (op =) args minimizeK
     2.6        val metis_ft = AList.defined (op =) args metis_ftK
     2.7 -      val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
     2.8 +      val trivial =
     2.9 +        Try_Methods.try_methods (SOME try_timeout) ([], [], [], []) pre
    2.10          handle TimeLimit.TimeOut => false
    2.11        fun apply_reconstructor m1 m2 =
    2.12          if metis_ft
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -55,6 +55,11 @@
     3.4       batch_size: int,
     3.5       expect: string}
     3.6  
     3.7 +  val genuineN : string
     3.8 +  val quasi_genuineN : string
     3.9 +  val potentialN : string
    3.10 +  val noneN : string
    3.11 +  val unknownN : string
    3.12    val register_frac_type : string -> (string * string) list -> theory -> theory
    3.13    val unregister_frac_type : string -> theory -> theory
    3.14    val register_codatatype : typ -> string -> styp list -> theory -> theory
    3.15 @@ -131,6 +136,12 @@
    3.16     batch_size: int,
    3.17     expect: string}
    3.18  
    3.19 +val genuineN = "genuine"
    3.20 +val quasi_genuineN = "quasi_genuine"
    3.21 +val potentialN = "potential"
    3.22 +val noneN = "none"
    3.23 +val unknownN = "unknown"
    3.24 +
    3.25  (* TODO: eliminate these historical aliases *)
    3.26  val register_frac_type = Nitpick_HOL.register_frac_type_global
    3.27  val unregister_frac_type = Nitpick_HOL.unregister_frac_type_global
    3.28 @@ -973,7 +984,7 @@
    3.29      fun run_batches _ _ []
    3.30                      (found_really_genuine, max_potential, max_genuine, donno) =
    3.31          if donno > 0 andalso max_genuine > 0 then
    3.32 -          (print_m (fn () => excipit "checked"); "unknown")
    3.33 +          (print_m (fn () => excipit "checked"); unknownN)
    3.34          else if max_genuine = original_max_genuine then
    3.35            if max_potential = original_max_potential then
    3.36              (print_m (fn () =>
    3.37 @@ -982,7 +993,7 @@
    3.38                      " This suggests that the induction hypothesis might be \
    3.39                      \general enough to prove this subgoal."
    3.40                    else
    3.41 -                    "")); if skipped > 0 then "unknown" else "none")
    3.42 +                    "")); if skipped > 0 then unknownN else noneN)
    3.43            else
    3.44              (print_m (fn () =>
    3.45                   excipit ("could not find a" ^
    3.46 @@ -991,11 +1002,11 @@
    3.47                             else
    3.48                               "ny better " ^ das_wort_model ^ "s.") ^
    3.49                            " It checked"));
    3.50 -             "potential")
    3.51 +             potentialN)
    3.52          else if found_really_genuine then
    3.53 -          "genuine"
    3.54 +          genuineN
    3.55          else
    3.56 -          "quasi_genuine"
    3.57 +          quasi_genuineN
    3.58        | run_batches j n (batch :: batches) z =
    3.59          let val (z as (_, _, max_genuine, _)) = run_batch j n batch z in
    3.60            run_batches (j + 1) n (if max_genuine > 0 then batches else []) z
    3.61 @@ -1007,7 +1018,7 @@
    3.62                    (false, max_potential, max_genuine, 0)
    3.63        handle TimeLimit.TimeOut =>
    3.64               (print_m (fn () => excipit "ran out of time after checking");
    3.65 -              if !met_potential > 0 then "potential" else "unknown")
    3.66 +              if !met_potential > 0 then potentialN else unknownN)
    3.67      val _ = print_v (fn () =>
    3.68                  "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
    3.69                  ".")
    3.70 @@ -1026,7 +1037,7 @@
    3.71         ("no_kodkodi", state))
    3.72      else
    3.73        let
    3.74 -        val unknown_outcome = ("unknown", state)
    3.75 +        val unknown_outcome = (unknownN, state)
    3.76          val deadline = Option.map (curry Time.+ (Time.now ())) timeout
    3.77          val outcome as (outcome_code, _) =
    3.78            time_limit (if debug orelse is_none timeout then NONE
    3.79 @@ -1065,7 +1076,7 @@
    3.80      val t = state |> Proof.raw_goal |> #goal |> prop_of
    3.81    in
    3.82      case Logic.count_prems t of
    3.83 -      0 => (Output.urgent_message "No subgoal!"; ("none", state))
    3.84 +      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
    3.85      | n =>
    3.86        let
    3.87          val t = Logic.goal_params t i |> fst
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri May 27 10:30:08 2011 +0200
     4.3 @@ -10,6 +10,8 @@
     4.4  sig
     4.5    type params = Nitpick.params
     4.6  
     4.7 +  val nitpickN : string
     4.8 +  val nitpick_paramsN : string
     4.9    val auto : bool Unsynchronized.ref
    4.10    val default_params : theory -> (string * string) list -> params
    4.11    val setup : theory -> theory
    4.12 @@ -24,6 +26,9 @@
    4.13  open Nitpick_Nut
    4.14  open Nitpick
    4.15  
    4.16 +val nitpickN = "nitpick"
    4.17 +val nitpick_paramsN = "nitpick_params"
    4.18 +
    4.19  val auto = Unsynchronized.ref false
    4.20  
    4.21  (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
    4.22 @@ -356,18 +361,18 @@
    4.23      val params as {blocking, debug, ...} =
    4.24        extract_params ctxt auto (default_raw_params thy) override_params
    4.25      fun go () =
    4.26 -      (false, state)
    4.27 +      (unknownN, state)
    4.28        |> (if auto then perhaps o try
    4.29            else if debug then fn f => fn x => f x
    4.30            else handle_exceptions ctxt)
    4.31 -         (fn (_, state) => pick_nits_in_subgoal state params auto i step
    4.32 -                           |>> curry (op =) "genuine")
    4.33 -  in if blocking then go () else Future.fork (tap go) |> K (false, state) end
    4.34 +         (fn (_, state) => pick_nits_in_subgoal state params auto i step)
    4.35 +  in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end
    4.36 +  |> `(fn (outcome_code, _) => outcome_code = genuineN)
    4.37  
    4.38  fun nitpick_trans (params, i) =
    4.39 -  Toplevel.keep (fn st =>
    4.40 -      (pick_nits params false i (Toplevel.proof_position_of st)
    4.41 -                 (Toplevel.proof_of st); ()))
    4.42 +  Toplevel.keep (fn state =>
    4.43 +      pick_nits params false i (Toplevel.proof_position_of state)
    4.44 +                (Toplevel.proof_of state) |> K ())
    4.45  
    4.46  fun string_for_raw_param (name, value) =
    4.47    name ^ " = " ^ stringify_raw_param_value value
    4.48 @@ -388,15 +393,15 @@
    4.49    (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
    4.50  val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
    4.51  
    4.52 -val _ = Outer_Syntax.improper_command "nitpick"
    4.53 +val _ = Outer_Syntax.improper_command nitpickN
    4.54              "try to find a counterexample for a given subgoal using Nitpick"
    4.55              Keyword.diag parse_nitpick_command
    4.56 -val _ = Outer_Syntax.command "nitpick_params"
    4.57 +val _ = Outer_Syntax.command nitpick_paramsN
    4.58              "set and display the default parameters for Nitpick"
    4.59              Keyword.thy_decl parse_nitpick_params_command
    4.60  
    4.61 -val auto_nitpick = pick_nits [] true 1 0
    4.62 +fun try_nitpick auto = pick_nits [] auto 1 0
    4.63  
    4.64 -val setup = Try.register_tool (auto, auto_nitpick)
    4.65 +val setup = Try.register_tool (nitpickN, (auto, try_nitpick))
    4.66  
    4.67  end;
     5.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Fri May 27 10:30:08 2011 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitrox.ML	Fri May 27 10:30:08 2011 +0200
     5.3 @@ -124,7 +124,7 @@
     5.4           ("format", "1000"),
     5.5           ("max_potential", "0"),
     5.6           (* ("timeout", "240 s"), *)
     5.7 -         ("expect", "genuine")]
     5.8 +         ("expect", Nitpick.genuineN)]
     5.9          |> Nitpick_Isar.default_params @{theory}
    5.10        val auto = false
    5.11        val i = 1
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 27 10:30:08 2011 +0200
     6.3 @@ -8,6 +8,7 @@
     6.4  sig
     6.5    type params = Sledgehammer_Provers.params
     6.6  
     6.7 +  val sledgehammerN : string
     6.8    val auto : bool Unsynchronized.ref
     6.9    val provers : string Unsynchronized.ref
    6.10    val timeout : int Unsynchronized.ref
    6.11 @@ -26,6 +27,17 @@
    6.12  open Sledgehammer_Minimize
    6.13  open Sledgehammer_Run
    6.14  
    6.15 +val sledgehammerN = "sledgehammer"
    6.16 +val sledgehammer_paramsN = "sledgehammer_params"
    6.17 +
    6.18 +val runN = "run"
    6.19 +val minN = "min"
    6.20 +val messagesN = "messages"
    6.21 +val supported_proversN = "supported_provers"
    6.22 +val running_proversN = "running_provers"
    6.23 +val kill_proversN = "kill_provers"
    6.24 +val refresh_tptpN = "refresh_tptp"
    6.25 +
    6.26  val auto = Unsynchronized.ref false
    6.27  
    6.28  val _ =
    6.29 @@ -296,17 +308,6 @@
    6.30  
    6.31  (* Sledgehammer the given subgoal *)
    6.32  
    6.33 -val sledgehammerN = "sledgehammer"
    6.34 -val sledgehammer_paramsN = "sledgehammer_params"
    6.35 -
    6.36 -val runN = "run"
    6.37 -val minN = "min"
    6.38 -val messagesN = "messages"
    6.39 -val supported_proversN = "supported_provers"
    6.40 -val running_proversN = "running_provers"
    6.41 -val kill_proversN = "kill_provers"
    6.42 -val refresh_tptpN = "refresh_tptp"
    6.43 -
    6.44  val is_raw_param_relevant_for_minimize =
    6.45    member (op =) params_for_minimize o fst o unalias_raw_param
    6.46  fun string_for_raw_param (key, values) =
    6.47 @@ -402,12 +403,15 @@
    6.48        "set and display the default parameters for Sledgehammer" Keyword.thy_decl
    6.49        parse_sledgehammer_params_command
    6.50  
    6.51 -fun auto_sledgehammer state =
    6.52 -  let val ctxt = Proof.context_of state in
    6.53 -    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
    6.54 -                     (minimize_command [] 1) state
    6.55 +fun try_sledgehammer auto state =
    6.56 +  let
    6.57 +    val ctxt = Proof.context_of state
    6.58 +    val i = 1
    6.59 +  in
    6.60 +    run_sledgehammer (get_params auto ctxt []) auto i no_relevance_override
    6.61 +                     (minimize_command [] i) state
    6.62    end
    6.63  
    6.64 -val setup = Try.register_tool (auto, auto_sledgehammer)
    6.65 +val setup = Try.register_tool (sledgehammerN, (auto, try_sledgehammer))
    6.66  
    6.67  end;
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri May 27 10:30:08 2011 +0200
     7.3 @@ -13,11 +13,15 @@
     7.4    type params = Sledgehammer_Provers.params
     7.5    type prover = Sledgehammer_Provers.prover
     7.6  
     7.7 +  val someN : string
     7.8 +  val noneN : string
     7.9 +  val timeoutN : string
    7.10 +  val unknownN : string
    7.11    val auto_minimize_min_facts : int Config.T
    7.12    val get_minimizing_prover : Proof.context -> bool -> string -> prover
    7.13    val run_sledgehammer :
    7.14      params -> bool -> int -> relevance_override -> (string -> minimize_command)
    7.15 -    -> Proof.state -> bool * Proof.state
    7.16 +    -> Proof.state -> bool * (string * Proof.state)
    7.17  end;
    7.18  
    7.19  structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
    7.20 @@ -29,6 +33,22 @@
    7.21  open Sledgehammer_Provers
    7.22  open Sledgehammer_Minimize
    7.23  
    7.24 +val someN = "some"
    7.25 +val noneN = "none"
    7.26 +val timeoutN = "timeout"
    7.27 +val unknownN = "unknown"
    7.28 +
    7.29 +val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
    7.30 +
    7.31 +fun max_outcome_code codes =
    7.32 +  NONE
    7.33 +  |> fold (fn candidate =>
    7.34 +              fn accum as SOME _ => accum
    7.35 +               | NONE => if member (op =) codes candidate then SOME candidate
    7.36 +                         else NONE)
    7.37 +          ordered_outcome_codes
    7.38 +  |> the_default unknownN
    7.39 +
    7.40  fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
    7.41                         n goal =
    7.42    (name,
    7.43 @@ -86,11 +106,6 @@
    7.44               | NONE => result
    7.45             end)
    7.46  
    7.47 -val someN = "some"
    7.48 -val noneN = "none"
    7.49 -val timeoutN = "timeout"
    7.50 -val unknownN = "unknown"
    7.51 -
    7.52  fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    7.53                                expect, ...})
    7.54          auto minimize_command only
    7.55 @@ -190,7 +205,7 @@
    7.56    if null provers then
    7.57      error "No prover is set."
    7.58    else case subgoal_count state of
    7.59 -    0 => (Output.urgent_message "No subgoal!"; (false, state))
    7.60 +    0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))
    7.61    | n =>
    7.62      let
    7.63        val _ = Proof.assert_backward state
    7.64 @@ -219,18 +234,19 @@
    7.65               facts = facts,
    7.66               smt_filter = maybe_smt_filter
    7.67                    (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    7.68 -          fun launch problem =
    7.69 -            launch_prover params auto minimize_command only problem
    7.70 -            #>> curry (op =) someN
    7.71 +          val launch = launch_prover params auto minimize_command only
    7.72          in
    7.73            if auto then
    7.74 -            fold (fn prover => fn (true, state) => (true, state)
    7.75 -                                | (false, _) => launch problem prover)
    7.76 -                 provers (false, state)
    7.77 +            (unknownN, state)
    7.78 +            |> fold (fn prover => fn accum as (outcome_code, state) =>
    7.79 +                        if outcome_code = someN then accum
    7.80 +                        else launch problem prover)
    7.81 +                    provers
    7.82            else
    7.83              provers
    7.84 -            |> (if blocking then smart_par_list_map else map) (launch problem)
    7.85 -            |> exists fst |> rpair state
    7.86 +            |> (if blocking then smart_par_list_map else map)
    7.87 +                   (launch problem #> fst)
    7.88 +            |> max_outcome_code |> rpair state
    7.89          end
    7.90        fun get_facts label is_appropriate_prop relevance_fudge provers =
    7.91          let
    7.92 @@ -290,24 +306,26 @@
    7.93            in
    7.94              smts |> map (`(class_of_smt_solver ctxt))
    7.95                   |> AList.group (op =)
    7.96 -                 |> map (launch_provers state (K facts) weight smt_filter o snd)
    7.97 -                 |> exists fst |> rpair state
    7.98 +                 |> map (snd #> launch_provers state (K facts) weight smt_filter
    7.99 +                             #> fst)
   7.100 +                 |> max_outcome_code |> rpair state
   7.101            end
   7.102        val launch_full_atps = launch_atps "ATP" (K true) full_atps
   7.103        val launch_ueq_atps =
   7.104          launch_atps "Unit equational provers" is_unit_equality ueq_atps
   7.105        fun launch_atps_and_smt_solvers () =
   7.106          [launch_full_atps, launch_ueq_atps, launch_smts]
   7.107 -        |> smart_par_list_map (fn f => f (false, state) |> K ())
   7.108 +        |> smart_par_list_map (fn f => f (unknownN, state) |> K ())
   7.109          handle ERROR msg => (print ("Error: " ^ msg); error msg)
   7.110      in
   7.111 -      (false, state)
   7.112 +      (unknownN, state)
   7.113        |> (if blocking then
   7.114              launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
   7.115            else
   7.116              (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
   7.117        handle TimeLimit.TimeOut =>
   7.118 -             (print "Sledgehammer ran out of time."; (false, state))
   7.119 +             (print "Sledgehammer ran out of time."; (unknownN, state))
   7.120      end
   7.121 +    |> `(fn (outcome_code, _) => outcome_code = someN)
   7.122  
   7.123  end;
     8.1 --- a/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     8.2 +++ b/src/HOL/Tools/try_methods.ML	Fri May 27 10:30:08 2011 +0200
     8.3 @@ -6,6 +6,8 @@
     8.4  
     8.5  signature TRY_METHODS =
     8.6  sig
     8.7 +  val try_methodsN : string
     8.8 +  val noneN : string
     8.9    val auto : bool Unsynchronized.ref
    8.10    val try_methods :
    8.11      Time.time option -> string list * string list * string list * string list
    8.12 @@ -16,6 +18,10 @@
    8.13  structure Try_Methods : TRY_METHODS =
    8.14  struct
    8.15  
    8.16 +val try_methodsN = "try_methods"
    8.17 +
    8.18 +val noneN = "none"
    8.19 +
    8.20  val auto = Unsynchronized.ref false
    8.21  
    8.22  val _ =
    8.23 @@ -109,7 +115,8 @@
    8.24    in
    8.25      case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
    8.26                      |> map_filter I |> sort (int_ord o pairself snd) of
    8.27 -      [] => (if auto then () else writeln "No proof found."; (false, st))
    8.28 +      [] => (if auto then () else writeln "No proof found.";
    8.29 +             (false, (noneN, st)))
    8.30      | xs as (s, _) :: _ =>
    8.31        let
    8.32          val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
    8.33 @@ -124,20 +131,18 @@
    8.34                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    8.35            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
    8.36        in
    8.37 -        (true, st |> (if auto then
    8.38 -                        Proof.goal_message
    8.39 -                            (fn () => Pretty.chunks [Pretty.str "",
    8.40 -                                      Pretty.markup Markup.hilite
    8.41 -                                                    [Pretty.str message]])
    8.42 -                      else
    8.43 -                        tap (fn _ => Output.urgent_message message)))
    8.44 +        (true, (s, st |> (if auto then
    8.45 +                            Proof.goal_message
    8.46 +                                (fn () => Pretty.chunks [Pretty.str "",
    8.47 +                                          Pretty.markup Markup.hilite
    8.48 +                                                        [Pretty.str message]])
    8.49 +                          else
    8.50 +                            tap (fn _ => Output.urgent_message message))))
    8.51        end
    8.52    end
    8.53  
    8.54  fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
    8.55  
    8.56 -val try_methodsN = "try_methods"
    8.57 -
    8.58  fun try_methods_trans quad =
    8.59    Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
    8.60                   o Toplevel.proof_of)
    8.61 @@ -175,8 +180,8 @@
    8.62        "try a combination of proof methods" Keyword.diag
    8.63        parse_try_methods_command
    8.64  
    8.65 -val auto_try_methods = do_try_methods true NONE ([], [], [], [])
    8.66 +fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
    8.67  
    8.68 -val setup = Try.register_tool (auto, auto_try_methods)
    8.69 +val setup = Try.register_tool (try_methodsN, (auto, try_try_methods))
    8.70  
    8.71  end;
     9.1 --- a/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     9.2 +++ b/src/Tools/quickcheck.ML	Fri May 27 10:30:08 2011 +0200
     9.3 @@ -6,6 +6,10 @@
     9.4  
     9.5  signature QUICKCHECK =
     9.6  sig
     9.7 +  val quickcheckN: string
     9.8 +  val genuineN: string
     9.9 +  val noneN: string
    9.10 +  val unknownN: string
    9.11    val setup: theory -> theory
    9.12    (* configuration *)
    9.13    val auto: bool Unsynchronized.ref
    9.14 @@ -61,6 +65,13 @@
    9.15  structure Quickcheck : QUICKCHECK =
    9.16  struct
    9.17  
    9.18 +val quickcheckN = "quickcheck"
    9.19 +val quickcheck_paramsN = "quickcheck_params"
    9.20 +
    9.21 +val genuineN = "genuine"
    9.22 +val noneN = "none"
    9.23 +val unknownN = "unknown"
    9.24 +
    9.25  (* preferences *)
    9.26  
    9.27  val auto = Unsynchronized.ref false;
    9.28 @@ -472,10 +483,11 @@
    9.29        Pretty.chunks ((Pretty.str (tool_name auto ^ " found a counterexample:\n") ::
    9.30          map (fn (s, t) =>
    9.31            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex))
    9.32 -        @ (Pretty.str ("Evaluated terms:\n") ::
    9.33 -        map (fn (t, u) =>
    9.34 -          Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
    9.35 -          (rev eval_terms)));
    9.36 +        @ (if null eval_terms then []
    9.37 +           else (Pretty.str ("Evaluated terms:\n") ::
    9.38 +             map (fn (t, u) =>
    9.39 +               Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, Syntax.pretty_term ctxt u])
    9.40 +               (rev eval_terms))));
    9.41  
    9.42  fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
    9.43      satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
    9.44 @@ -511,27 +523,6 @@
    9.45        (* map (pretty_reports ctxt) (reports_of result) :: *)
    9.46        (if Config.get ctxt timing then cons (pretty_timings (timings_of result)) else I) [])
    9.47  
    9.48 -(* automatic testing *)
    9.49 -
    9.50 -fun auto_quickcheck state =
    9.51 -  let
    9.52 -    val ctxt = Proof.context_of state;
    9.53 -    val res =
    9.54 -      state
    9.55 -      |> Proof.map_context (Config.put report false #> Config.put quiet true)
    9.56 -      |> try (test_goal (false, false) ([], []) 1);
    9.57 -  in
    9.58 -    case res of
    9.59 -      NONE => (false, state)
    9.60 -    | SOME (result :: _) => if found_counterexample result then
    9.61 -        (true, Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    9.62 -          Pretty.mark Markup.hilite (pretty_counterex ctxt true (response_of result))])) state)
    9.63 -      else
    9.64 -        (false, state)
    9.65 -  end
    9.66 -
    9.67 -val setup = Try.register_tool (auto, auto_quickcheck)
    9.68 -
    9.69  (* Isar commands *)
    9.70  
    9.71  fun read_nat s = case (Library.read_int o Symbol.explode) s
    9.72 @@ -610,7 +601,8 @@
    9.73  
    9.74  fun quickcheck_cmd args i state =
    9.75    gen_quickcheck args i (Toplevel.proof_of state)
    9.76 -  |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state) false;
    9.77 +  |> Output.urgent_message o Pretty.string_of
    9.78 +     o pretty_counterex_and_reports (Toplevel.context_of state) false;
    9.79  
    9.80  val parse_arg =
    9.81    Parse.name --
    9.82 @@ -622,15 +614,47 @@
    9.83    Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]" || Scan.succeed [];
    9.84  
    9.85  val _ =
    9.86 -  Outer_Syntax.command "quickcheck_params" "set parameters for random testing" Keyword.thy_decl
    9.87 +  Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
    9.88      (parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
    9.89  
    9.90  val _ =
    9.91 -  Outer_Syntax.improper_command "quickcheck" "try to find counterexample for subgoal" Keyword.diag
    9.92 +  Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
    9.93      (parse_args -- Scan.optional Parse.nat 1
    9.94        >> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
    9.95  
    9.96 +(* automatic testing *)
    9.97 +
    9.98 +fun try_quickcheck auto state =
    9.99 +  let
   9.100 +    val ctxt = Proof.context_of state;
   9.101 +    val i = 1;
   9.102 +    val res =
   9.103 +      state
   9.104 +      |> Proof.map_context (Config.put report false #> Config.put quiet true)
   9.105 +      |> try (test_goal (false, false) ([], []) i);
   9.106 +  in
   9.107 +    case res of
   9.108 +      NONE => (unknownN, state)
   9.109 +    | SOME results =>
   9.110 +        let
   9.111 +          val msg = pretty_counterex_and_reports ctxt auto results
   9.112 +                    |> not auto ? tap (Output.urgent_message o Pretty.string_of)
   9.113 +        in
   9.114 +          if exists found_counterexample results then
   9.115 +            (genuineN,
   9.116 +             state |> (if auto then
   9.117 +                         Proof.goal_message (K (Pretty.chunks [Pretty.str "",
   9.118 +                             Pretty.mark Markup.hilite msg]))
   9.119 +                       else
   9.120 +                         I))
   9.121 +          else
   9.122 +            (noneN, state)
   9.123 +        end
   9.124 +  end
   9.125 +  |> `(fn (outcome_code, _) => outcome_code = genuineN)
   9.126 +
   9.127 +val setup = Try.register_tool (quickcheckN, (auto, try_quickcheck))
   9.128 +
   9.129  end;
   9.130  
   9.131 -
   9.132  val auto_quickcheck = Quickcheck.auto;
    10.1 --- a/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
    10.2 +++ b/src/Tools/solve_direct.ML	Fri May 27 10:30:08 2011 +0200
    10.3 @@ -10,9 +10,13 @@
    10.4  
    10.5  signature SOLVE_DIRECT =
    10.6  sig
    10.7 +  val solve_directN: string
    10.8 +  val someN: string
    10.9 +  val noneN: string
   10.10 +  val unknownN: string
   10.11    val auto: bool Unsynchronized.ref
   10.12    val max_solutions: int Unsynchronized.ref
   10.13 -  val solve_direct: bool -> Proof.state -> bool * Proof.state
   10.14 +  val solve_direct: bool -> Proof.state -> bool * (string * Proof.state)
   10.15    val setup: theory -> theory
   10.16  end;
   10.17  
   10.18 @@ -21,6 +25,9 @@
   10.19  
   10.20  val solve_directN = "solve_direct";
   10.21  
   10.22 +val someN = "some";
   10.23 +val noneN = "none";
   10.24 +val unknownN = "none";
   10.25  
   10.26  (* preferences *)
   10.27  
   10.28 @@ -74,7 +81,7 @@
   10.29    in
   10.30      (case try seek_against_goal () of
   10.31        SOME (SOME results) =>
   10.32 -        (true,
   10.33 +        (someN,
   10.34            state |>
   10.35             (if auto then
   10.36               Proof.goal_message
   10.37 @@ -85,8 +92,10 @@
   10.38              else
   10.39                tap (fn _ =>
   10.40                  Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
   10.41 -    | _ => (false, state))
   10.42 -  end;
   10.43 +    | SOME NONE => (noneN, state)
   10.44 +    | NONE => (unknownN, state))
   10.45 +  end
   10.46 +  |> `(fn (outcome_code, _) => outcome_code = someN);
   10.47  
   10.48  val _ =
   10.49    Outer_Syntax.improper_command solve_directN
   10.50 @@ -97,8 +106,6 @@
   10.51  
   10.52  (* hook *)
   10.53  
   10.54 -val auto_solve_direct = solve_direct true;
   10.55 -
   10.56 -val setup = Try.register_tool (auto, auto_solve_direct);
   10.57 +val setup = Try.register_tool (solve_directN, (auto, solve_direct));
   10.58  
   10.59  end;
    11.1 --- a/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
    11.2 +++ b/src/Tools/try.ML	Fri May 27 10:30:08 2011 +0200
    11.3 @@ -6,16 +6,28 @@
    11.4  
    11.5  signature TRY =
    11.6  sig
    11.7 +  type tool =
    11.8 +    string * (bool Unsynchronized.ref
    11.9 +              * (bool -> Proof.state -> bool * (string * Proof.state)))
   11.10 +
   11.11 +  val tryN : string
   11.12    val auto_time_limit: real Unsynchronized.ref
   11.13  
   11.14 -  val register_tool :
   11.15 -    bool Unsynchronized.ref * (Proof.state -> bool * Proof.state) -> theory
   11.16 -    -> theory
   11.17 +  val register_tool : tool -> theory -> theory
   11.18 +  val get_tools : theory -> tool list
   11.19 +  val try_tools : Proof.state -> (string * string) option
   11.20  end;
   11.21  
   11.22  structure Try : TRY =
   11.23  struct
   11.24  
   11.25 +type tool =
   11.26 +  string * (bool Unsynchronized.ref
   11.27 +            * (bool -> Proof.state -> bool * (string * Proof.state)))
   11.28 +
   11.29 +val tryN = "try"
   11.30 +
   11.31 +
   11.32  (* preferences *)
   11.33  
   11.34  val auto_time_limit = Unsynchronized.ref 4.0
   11.35 @@ -31,24 +43,42 @@
   11.36  
   11.37  structure Data = Theory_Data
   11.38  (
   11.39 -  type T = (bool Unsynchronized.ref * (Proof.state -> bool * Proof.state)) list
   11.40 +  type T = tool list
   11.41    val empty = []
   11.42    val extend = I
   11.43    fun merge data : T = AList.merge (op =) (K true) data
   11.44  )
   11.45  
   11.46 +val get_tools = Data.get
   11.47 +
   11.48  val register_tool = Data.map o AList.update (op =)
   11.49  
   11.50 +(* try command *)
   11.51 +
   11.52 +fun try_tools state =
   11.53 +  get_tools (Proof.theory_of state)
   11.54 +  |> Par_List.get_some
   11.55 +         (fn (name, (_, tool)) =>
   11.56 +             case try (tool false) state of
   11.57 +               SOME (true, (outcome_code, _)) => SOME (name, outcome_code)
   11.58 +             | _ => NONE)
   11.59 +
   11.60 +val _ =
   11.61 +  Outer_Syntax.improper_command tryN
   11.62 +      "try a combination of automatic proving and disproving tools" Keyword.diag
   11.63 +      (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
   11.64 +
   11.65  
   11.66 -(* automatic testing *)
   11.67 +(* automatic try *)
   11.68  
   11.69 -fun run_tools tools state =
   11.70 -  tools |> map_filter (fn (auto, tool) => if !auto then SOME tool else NONE)
   11.71 -        |> Par_List.get_some (fn tool =>
   11.72 -                                 case try tool state of
   11.73 -                                   SOME (true, state) => SOME state
   11.74 -                                 | _ => NONE)
   11.75 -        |> the_default state
   11.76 +fun auto_try state =
   11.77 +  get_tools (Proof.theory_of state)
   11.78 +  |> map_filter (fn (_, (auto, tool)) => if !auto then SOME tool else NONE)
   11.79 +  |> Par_List.get_some (fn tool =>
   11.80 +                           case try (tool true) state of
   11.81 +                             SOME (true, (_, state)) => SOME state
   11.82 +                           | _ => NONE)
   11.83 +  |> the_default state
   11.84  
   11.85  (* Too large values are understood as milliseconds, ensuring compatibility with
   11.86     old setting files. No users can possibly in their right mind want the user
   11.87 @@ -62,8 +92,7 @@
   11.88  
   11.89  val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   11.90    if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
   11.91 -    TimeLimit.timeLimit (smart_seconds (!auto_time_limit))
   11.92 -        (run_tools (Data.get (Proof.theory_of state))) state
   11.93 +    TimeLimit.timeLimit (smart_seconds (!auto_time_limit)) auto_try state
   11.94      handle TimeLimit.TimeOut => state
   11.95    else
   11.96      state))