src/HOL/Tools/try.ML
author blanchet
Fri, 17 Sep 2010 17:02:34 +0200
changeset 39547 5df45da44bfb
parent 39336 1899349a5026
child 39616 8052101883c3
permissions -rw-r--r--
reorder proof methods and take out "best"; suggestions from Tobias
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.
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
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     7
signature TRY =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     8
sig
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
     9
  val auto : bool Unsynchronized.ref
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    10
  val invoke_try : Time.time option -> Proof.state -> bool
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    11
  val setup : theory -> theory
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    12
end;
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    13
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    14
structure Try : TRY =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    15
struct
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    16
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    17
val auto = Unsynchronized.ref false
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    18
39333
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    19
val _ =
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    20
  ProofGeneralPgip.add_preference Preferences.category_tracing
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    21
  (setmp_noncritical auto true (fn () =>
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    22
    Preferences.bool_pref auto
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    23
      "auto-try" "Try standard proof methods.") ());
c277c79fb9db add Proof General option
blanchet
parents: 39332
diff changeset
    24
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    25
val default_timeout = Time.fromSeconds 5
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    26
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    27
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
    28
  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
    29
    case (case timeout_opt of
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    30
            SOME timeout => TimeLimit.timeLimit timeout
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    31
          | 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
    32
      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
    33
    | NONE => false
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    34
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    35
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    36
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
    37
  let val timer = Timer.startRealTimer () in
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    38
    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
    39
      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
    40
    else
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    41
      NONE
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    42
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    43
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    44
fun named_method thy name =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    45
  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
    46
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    47
fun apply_named_method name ctxt =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    48
  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
    49
    Method.apply (named_method thy name) ctxt []
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    50
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    51
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    52
fun do_named_method name timeout_opt st =
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    53
  do_generic timeout_opt name (#goal o Proof.goal) snd
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    54
             (apply_named_method name (Proof.context_of st)) st
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),
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    72
   ("force", false), ("blast", false), ("arith", false)]
5df45da44bfb reorder proof methods and take out "best";
blanchet
parents: 39336
diff changeset
    73
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
    74
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    75
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
    76
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    77
fun do_try auto timeout_opt st =
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    78
  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
    79
                  |> 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
    80
    [] => (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
    81
  | xs as (s, _) :: _ =>
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    82
    let
39332
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    83
      val xs = xs |> map swap |> AList.coalesce (op =)
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    84
                  |> map (swap o apsnd commas)
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    85
      val message =
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    86
        (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
38946
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    87
        Markup.markup Markup.sendback
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    88
            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    89
             " " ^ s) ^
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    90
        ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n"
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    91
    in
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    92
      (true, st |> (if auto then
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    93
                      Proof.goal_message
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    94
                          (fn () => Pretty.chunks [Pretty.str "",
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    95
                                    Pretty.markup Markup.hilite
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    96
                                                  [Pretty.str message]])
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    97
                    else
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    98
                      tap (fn _ => priority message)))
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    99
    end
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   100
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   101
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
   102
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   103
val tryN = "try"
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   104
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   105
val _ =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   106
  Outer_Syntax.improper_command tryN
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   107
      "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
   108
      (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
   109
                                    o Toplevel.proof_of)))
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   110
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   111
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
   112
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   113
val setup = Auto_Tools.register_tool (tryN, auto_try)
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   114
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   115
end;