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