src/HOL/Tools/try_methods.ML
author huffman
Mon, 08 Aug 2011 09:52:09 -0700
changeset 44064 5bce8ff0d9ae
parent 43607 119767e1ccb4
child 44651 5d6a11e166cf
permissions -rw-r--r--
moved division ring stuff from Rings.thy to Fields.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
     1
(*  Title:      HOL/Tools/try_methods.ML
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     3
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     4
Try a combination of proof methods.
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     5
*)
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     6
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
     7
signature TRY_METHODS =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     8
sig
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
     9
  val try_methodsN : string
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    10
  val noneN : string
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    11
  val auto : bool Unsynchronized.ref
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
    12
  val try_methods :
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    13
    Time.time option -> string list * string list * string list * string list
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    14
    -> Proof.state -> bool
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    15
  val setup : theory -> theory
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    16
end;
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    17
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
    18
structure Try_Methods : TRY_METHODS =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    19
struct
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    20
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    21
datatype mode = Auto_Try | Try | Normal
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    22
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    23
val try_methodsN = "try_methods"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    24
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    25
val noneN = "none"
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
    26
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    27
val auto = Unsynchronized.ref false
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    28
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    29
val _ =
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    30
  ProofGeneralPgip.add_preference Preferences.category_tracing
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
    31
      (Preferences.bool_pref auto "auto-try-methods"
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
    32
                             "Try standard proof methods.")
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    33
40301
bf39a257b3d3 simplified some time constants;
wenzelm
parents: 40222
diff changeset
    34
val default_timeout = seconds 5.0
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    35
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    36
fun can_apply timeout_opt pre post tac st =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    37
  let val {goal, ...} = Proof.goal st in
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    38
    case (case timeout_opt of
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    39
            SOME timeout => TimeLimit.timeLimit timeout
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    40
          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    41
      SOME (x, _) => nprems_of (post x) < nprems_of goal
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    42
    | NONE => false
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    43
  end
40113
1f61f0826e8a handle timeouts (to prevent failure from other threads);
blanchet
parents: 39719
diff changeset
    44
  handle TimeLimit.TimeOut => false
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    45
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    46
fun do_generic timeout_opt command pre post apply st =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    47
  let val timer = Timer.startRealTimer () in
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    48
    if can_apply timeout_opt pre post apply st then
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    49
      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    50
    else
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    51
      NONE
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    52
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    53
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    54
val parse_method =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    55
  enclose "(" ")"
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    56
  #> Outer_Syntax.scan Position.start
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    57
  #> filter Token.is_proper
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    58
  #> Scan.read Token.stopper Method.parse
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    59
  #> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    60
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    61
fun apply_named_method_on_first_goal method thy =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    62
  method |> parse_method
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    63
         |> Method.method thy
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    64
         |> Method.Basic
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    65
         |> curry Method.SelectGoals 1
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    66
         |> Proof.refine
40222
cd6d2b0a4096 reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents: 40132
diff changeset
    67
  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    68
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    69
fun add_attr_text (NONE, _) s = s
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    70
  | add_attr_text (_, []) s = s
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    71
  | add_attr_text (SOME x, fs) s =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    72
    s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    73
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    74
  "" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    75
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    76
fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    77
                    timeout_opt quad st =
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    78
  if mode <> Auto_Try orelse run_if_auto_try then
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    79
    let val attrs = attrs_text attrs quad in
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    80
      do_generic timeout_opt
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    81
                 (name ^ (if all_goals andalso
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    82
                             nprems_of (#goal (Proof.goal st)) > 1 then
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    83
                            "[1]"
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    84
                          else
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    85
                            "") ^
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    86
                  attrs) I (#goal o Proof.goal)
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    87
                 (apply_named_method_on_first_goal (name ^ attrs)
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    88
                                                   (Proof.theory_of st)) st
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    89
    end
40222
cd6d2b0a4096 reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents: 40132
diff changeset
    90
  else
cd6d2b0a4096 reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents: 40132
diff changeset
    91
    NONE
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    92
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    93
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    94
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    95
val simp_attrs = (SOME "add", NONE, NONE, NONE)
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    96
val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
    97
val no_attrs = (NONE, NONE, NONE, NONE)
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
    98
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
    99
(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *)
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
   100
val named_methods =
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   101
  [("simp", ((false, true), simp_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   102
   ("auto", ((true, true), full_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   103
   ("fast", ((false, false), clas_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   104
   ("fastsimp", ((false, false), full_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   105
   ("force", ((false, false), full_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   106
   ("blast", ((false, true), clas_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   107
   ("metis", ((false, true), metis_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   108
   ("linarith", ((false, true), no_attrs)),
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   109
   ("presburger", ((false, true), no_attrs))]
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
   110
val do_methods = map do_named_method named_methods
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   111
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   112
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   113
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   114
fun do_try_methods mode timeout_opt quad st =
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   115
  let
43607
119767e1ccb4 linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents: 43031
diff changeset
   116
    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #>
119767e1ccb4 linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
boehmes
parents: 43031
diff changeset
   117
      Config.put Lin_Arith.verbose false)
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   118
  in
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   119
    if mode = Normal then
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   120
      "Trying " ^ space_implode " " (Try.serial_commas "and"
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   121
                                      (map (quote o fst) named_methods)) ^ "..."
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   122
      |> Output.urgent_message
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   123
    else
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   124
      ();
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   125
    case do_methods |> Par_List.map (fn f => f mode timeout_opt quad st)
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   126
                    |> map_filter I |> sort (int_ord o pairself snd) of
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   127
      [] =>
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   128
      (if mode = Normal then Output.urgent_message "No proof found." else ();
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   129
       (false, (noneN, st)))
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   130
    | xs as (s, _) :: _ =>
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   131
      let
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   132
        val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   133
                    |> AList.coalesce (op =)
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   134
                    |> map (swap o apsnd commas)
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   135
        val need_parens = exists_string (curry (op =) " ") s
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   136
        val message =
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   137
          (case mode of
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   138
             Auto_Try => "Auto Try Methods found a proof"
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   139
           | Try => "Try Methods found a proof"
43031
e437d47f419f more concise output
blanchet
parents: 43026
diff changeset
   140
           | Normal => "Try this") ^ ": " ^
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   141
          Markup.markup Markup.sendback
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   142
              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   143
                else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   144
          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   145
      in
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   146
        (true, (s, st |> (if mode = Auto_Try then
43020
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   147
                            Proof.goal_message
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   148
                                (fn () => Pretty.chunks [Pretty.str "",
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   149
                                          Pretty.markup Markup.hilite
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   150
                                                        [Pretty.str message]])
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   151
                          else
abb5d1f907e4 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents: 43018
diff changeset
   152
                            tap (fn _ => Output.urgent_message message))))
41038
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   153
      end
9592334001d5 quiet Metis in "try"
blanchet
parents: 40931
diff changeset
   154
  end
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   155
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   156
fun try_methods timeout_opt = fst oo do_try_methods Normal timeout_opt
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   157
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   158
fun try_methods_trans quad =
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   159
  Toplevel.keep (K () o do_try_methods Normal (SOME default_timeout) quad
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   160
                 o Toplevel.proof_of)
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   161
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   162
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   163
  (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   164
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   165
fun string_of_xthm (xref, args) =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   166
  Facts.string_of_ref xref ^
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   167
  implode (map (enclose "[" "]" o Pretty.str_of
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   168
                o Args.pretty_src @{context}) args)
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   169
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   170
val parse_fact_refs =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   171
  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   172
                            (Parse_Spec.xthm >> string_of_xthm))
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   173
val parse_attr =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   174
     Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   175
     >> (fn ss => (ss, [], [], []))
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   176
  || Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   177
     >> (fn is => ([], is, [], []))
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   178
  || Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   179
     >> (fn es => ([], [], es, []))
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   180
  || Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   181
     >> (fn ds => ([], [], [], ds))
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   182
fun parse_attrs x =
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   183
    (Args.parens parse_attrs
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   184
  || Scan.repeat parse_attr
42179
24662b614fd4 added support for "dest:" to "try"
blanchet
parents: 41999
diff changeset
   185
     >> (fn quad => fold merge_attrs quad ([], [], [], []))) x
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   186
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   187
val parse_try_methods_command =
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   188
  Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans
41999
3c029ef9e0f2 added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents: 41038
diff changeset
   189
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   190
val _ =
43016
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   191
  Outer_Syntax.improper_command try_methodsN
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   192
      "try a combination of proof methods" Keyword.diag
42330f25142c renamed "try" "try_methods"
blanchet
parents: 42179
diff changeset
   193
      parse_try_methods_command
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   194
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   195
fun try_try_methods auto =
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   196
  do_try_methods (if auto then Auto_Try else Try) NONE ([], [], [], [])
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   197
43026
0f15575a6465 handle non-auto try cases gracefully in Try Methods
blanchet
parents: 43024
diff changeset
   198
val setup = Try.register_tool (try_methodsN, (30, auto, try_try_methods))
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   199
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   200
end;