src/HOL/Tools/try.ML
author wenzelm
Mon, 25 Oct 2010 21:06:56 +0200
changeset 40132 7ee65dbffa31
parent 40113 1f61f0826e8a
child 40222 cd6d2b0a4096
permissions -rw-r--r--
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/try.ML
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.
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
     5
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
     6
FIXME: reintroduce or remove commented code (see also HOL.thy)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     7
*)
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     8
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     9
signature TRY =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    10
sig
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    11
(*
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    12
  val auto : bool Unsynchronized.ref
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    13
*)
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    14
  val invoke_try : Time.time option -> Proof.state -> bool
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    15
(*
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    16
  val setup : theory -> theory
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    17
*)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    18
end;
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    19
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    20
structure Try : TRY =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    21
struct
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    22
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    23
(*
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    24
val auto = Unsynchronized.ref false
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    25
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    26
val _ =
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    27
  ProofGeneralPgip.add_preference Preferences.category_tracing
39616
8052101883c3 renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents: 39547
diff changeset
    28
  (Unsynchronized.setmp auto true (fn () =>
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    29
    Preferences.bool_pref auto
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    30
      "auto-try" "Try standard proof methods.") ());
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
    31
*)
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    32
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    33
val default_timeout = Time.fromSeconds 5
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    34
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    35
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
    36
  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
    37
    case (case timeout_opt of
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    38
            SOME timeout => TimeLimit.timeLimit timeout
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    39
          | 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
    40
      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
    41
    | NONE => false
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    42
  end
40113
1f61f0826e8a handle timeouts (to prevent failure from other threads);
blanchet
parents: 39719
diff changeset
    43
  handle TimeLimit.TimeOut => false
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    44
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    45
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
    46
  let val timer = Timer.startRealTimer () in
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    47
    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
    48
      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
    49
    else
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    50
      NONE
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    51
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    52
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    53
fun named_method thy name =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    54
  Method.method thy (Args.src ((name, []), Position.none))
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    55
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    56
fun apply_named_method_on_first_goal name ctxt =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    57
  let val thy = ProofContext.theory_of ctxt in
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    58
    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    59
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    60
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    61
fun do_named_method (name, all_goals) timeout_opt st =
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    62
  do_generic timeout_opt
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    63
             (name ^ (if all_goals andalso
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    64
                         nprems_of (#goal (Proof.goal st)) > 1 then
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    65
                        "[1]"
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    66
                      else
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    67
                        "")) I (#goal o Proof.goal)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    68
             (apply_named_method_on_first_goal name (Proof.context_of st)) st
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    69
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    70
val named_methods =
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    71
  [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false),
40113
1f61f0826e8a handle timeouts (to prevent failure from other threads);
blanchet
parents: 39719
diff changeset
    72
   ("force", false), ("blast", false), ("metis", false), ("linarith", false),
1f61f0826e8a handle timeouts (to prevent failure from other threads);
blanchet
parents: 39719
diff changeset
    73
   ("presburger", false)]
39547
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    74
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
    75
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    76
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
    77
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    78
fun do_try auto timeout_opt st =
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    79
  case do_methods |> Par_List.map (fn f => f timeout_opt st)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    80
                  |> map_filter I |> sort (int_ord o pairself snd) of
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    81
    [] => (if auto then () else writeln "No proof found."; (false, st))
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    82
  | xs as (s, _) :: _ =>
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    83
    let
39332
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    84
      val xs = xs |> map swap |> AList.coalesce (op =)
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    85
                  |> map (swap o apsnd commas)
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    86
      val message =
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    87
        (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
38946
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    88
        Markup.markup Markup.sendback
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    89
            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    90
             " " ^ s) ^
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    91
        ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n"
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    92
    in
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    93
      (true, st |> (if auto then
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    94
                      Proof.goal_message
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    95
                          (fn () => Pretty.chunks [Pretty.str "",
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    96
                                    Pretty.markup Markup.hilite
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    97
                                                  [Pretty.str message]])
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    98
                    else
40132
7ee65dbffa31 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents: 40113
diff changeset
    99
                      tap (fn _ => Output.urgent_message message)))
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   100
    end
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   101
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   102
val invoke_try = fst oo do_try false
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   103
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   104
val tryN = "try"
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   105
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   106
val _ =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   107
  Outer_Syntax.improper_command tryN
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   108
      "try a combination of proof methods" Keyword.diag
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   109
      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   110
                                    o Toplevel.proof_of)))
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   111
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
   112
(*
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   113
fun auto_try st = if not (!auto) then (false, st) else do_try true NONE st
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   114
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   115
val setup = Auto_Tools.register_tool (tryN, auto_try)
39719
b876d7525e72 comment out Auto Try until issues are resolved (automatically on by default even though the code says off; thread that continues in the background)
blanchet
parents: 39616
diff changeset
   116
*)
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   117
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   118
end;