src/HOL/Tools/try.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 41038 9592334001d5
child 41999 3c029ef9e0f2
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
blanchet@38942
     1
(*  Title:      HOL/Tools/try.ML
blanchet@38942
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@38942
     3
blanchet@38942
     4
Try a combination of proof methods.
blanchet@38942
     5
*)
blanchet@38942
     6
blanchet@38942
     7
signature TRY =
blanchet@38942
     8
sig
blanchet@39331
     9
  val auto : bool Unsynchronized.ref
blanchet@39336
    10
  val invoke_try : Time.time option -> Proof.state -> bool
blanchet@39331
    11
  val setup : theory -> theory
blanchet@38942
    12
end;
blanchet@38942
    13
blanchet@38942
    14
structure Try : TRY =
blanchet@38942
    15
struct
blanchet@38942
    16
blanchet@39331
    17
val auto = Unsynchronized.ref false
blanchet@39331
    18
blanchet@39333
    19
val _ =
blanchet@39333
    20
  ProofGeneralPgip.add_preference Preferences.category_tracing
blanchet@40222
    21
      (Preferences.bool_pref auto "auto-try" "Try standard proof methods.")
blanchet@39333
    22
wenzelm@40301
    23
val default_timeout = seconds 5.0
blanchet@38944
    24
blanchet@39336
    25
fun can_apply timeout_opt pre post tac st =
blanchet@38942
    26
  let val {goal, ...} = Proof.goal st in
blanchet@39336
    27
    case (case timeout_opt of
blanchet@39336
    28
            SOME timeout => TimeLimit.timeLimit timeout
blanchet@39336
    29
          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
blanchet@38942
    30
      SOME (x, _) => nprems_of (post x) < nprems_of goal
blanchet@38942
    31
    | NONE => false
blanchet@38942
    32
  end
blanchet@40113
    33
  handle TimeLimit.TimeOut => false
blanchet@38942
    34
blanchet@39336
    35
fun do_generic timeout_opt command pre post apply st =
blanchet@38942
    36
  let val timer = Timer.startRealTimer () in
blanchet@39336
    37
    if can_apply timeout_opt pre post apply st then
blanchet@38942
    38
      SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
blanchet@38942
    39
    else
blanchet@38942
    40
      NONE
blanchet@38942
    41
  end
blanchet@38942
    42
blanchet@38942
    43
fun named_method thy name =
blanchet@38942
    44
  Method.method thy (Args.src ((name, []), Position.none))
blanchet@38942
    45
blanchet@38942
    46
fun apply_named_method_on_first_goal name ctxt =
blanchet@38942
    47
  let val thy = ProofContext.theory_of ctxt in
blanchet@38942
    48
    Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name)))
blanchet@38942
    49
  end
blanchet@40222
    50
  handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
blanchet@38942
    51
blanchet@40222
    52
fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st =
blanchet@40222
    53
  if not auto orelse run_if_auto then
blanchet@40222
    54
    do_generic timeout_opt
blanchet@40222
    55
               (name ^ (if all_goals andalso
blanchet@40222
    56
                           nprems_of (#goal (Proof.goal st)) > 1 then
blanchet@40222
    57
                          "[1]"
blanchet@40222
    58
                        else
blanchet@40222
    59
                          "")) I (#goal o Proof.goal)
blanchet@40222
    60
               (apply_named_method_on_first_goal name (Proof.context_of st)) st
blanchet@40222
    61
  else
blanchet@40222
    62
    NONE
blanchet@38942
    63
blanchet@40222
    64
(* name * (all_goals, run_if_auto) *)
blanchet@39547
    65
val named_methods =
blanchet@40222
    66
  [("simp", (false, true)),
blanchet@40222
    67
   ("auto", (true, true)),
blanchet@40222
    68
   ("fast", (false, false)),
blanchet@40222
    69
   ("fastsimp", (false, false)),
blanchet@40222
    70
   ("force", (false, false)),
blanchet@40222
    71
   ("blast", (false, true)),
blanchet@40222
    72
   ("metis", (false, true)),
blanchet@40222
    73
   ("linarith", (false, true)),
blanchet@40222
    74
   ("presburger", (false, true))]
blanchet@39547
    75
val do_methods = map do_named_method named_methods
blanchet@38942
    76
blanchet@38942
    77
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
blanchet@38942
    78
blanchet@39336
    79
fun do_try auto timeout_opt st =
blanchet@41038
    80
  let
blanchet@41038
    81
    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
blanchet@41038
    82
  in
blanchet@41038
    83
    case do_methods |> Par_List.map (fn f => f auto timeout_opt st)
blanchet@41038
    84
                    |> map_filter I |> sort (int_ord o pairself snd) of
blanchet@41038
    85
      [] => (if auto then () else writeln "No proof found."; (false, st))
blanchet@41038
    86
    | xs as (s, _) :: _ =>
blanchet@41038
    87
      let
blanchet@41038
    88
        val xs = xs |> map swap |> AList.coalesce (op =)
blanchet@41038
    89
                    |> map (swap o apsnd commas)
blanchet@41038
    90
        val message =
blanchet@41038
    91
          (if auto then "Auto Try found a proof" else "Try this command") ^
blanchet@41038
    92
          ": " ^
blanchet@41038
    93
          Markup.markup Markup.sendback
blanchet@41038
    94
              ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
blanchet@41038
    95
                else "apply") ^ " " ^ s) ^
blanchet@41038
    96
          "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
blanchet@41038
    97
      in
blanchet@41038
    98
        (true, st |> (if auto then
blanchet@41038
    99
                        Proof.goal_message
blanchet@41038
   100
                            (fn () => Pretty.chunks [Pretty.str "",
blanchet@41038
   101
                                      Pretty.markup Markup.hilite
blanchet@41038
   102
                                                    [Pretty.str message]])
blanchet@41038
   103
                      else
blanchet@41038
   104
                        tap (fn _ => Output.urgent_message message)))
blanchet@41038
   105
      end
blanchet@41038
   106
  end
blanchet@39331
   107
blanchet@39336
   108
val invoke_try = fst oo do_try false
blanchet@38942
   109
blanchet@38942
   110
val tryN = "try"
blanchet@38942
   111
blanchet@38942
   112
val _ =
blanchet@38942
   113
  Outer_Syntax.improper_command tryN
blanchet@38942
   114
      "try a combination of proof methods" Keyword.diag
blanchet@39336
   115
      (Scan.succeed (Toplevel.keep (K () o do_try false (SOME default_timeout)
blanchet@39336
   116
                                    o Toplevel.proof_of)))
blanchet@38942
   117
blanchet@40931
   118
val auto_try = do_try true NONE
blanchet@39331
   119
blanchet@40931
   120
val setup = Auto_Tools.register_tool (auto, auto_try)
blanchet@39331
   121
blanchet@38942
   122
end;