src/HOL/Tools/try.ML
author blanchet
Mon, 13 Sep 2010 14:28:25 +0200
changeset 39336 1899349a5026
parent 39334 c0bb925ae912
child 39547 5df45da44bfb
permissions -rw-r--r--
change signature of "Try.invoke_try" to make it more flexible
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
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    61
fun do_named_method_on_first_goal name timeout_opt st =
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    62
  do_generic timeout_opt
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    63
             (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    64
                      else "")) I (#goal o Proof.goal)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    65
             (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
    66
39222
decf607a5a67 remove "safe" (as suggested by Tobias) and added "arith" to "try"
blanchet
parents: 38946
diff changeset
    67
val all_goals_named_methods = ["auto"]
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    68
val first_goal_named_methods =
39222
decf607a5a67 remove "safe" (as suggested by Tobias) and added "arith" to "try"
blanchet
parents: 38946
diff changeset
    69
  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    70
val do_methods =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    71
  map do_named_method_on_first_goal all_goals_named_methods @
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    72
  map do_named_method first_goal_named_methods
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    73
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    74
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
    75
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    76
fun do_try auto timeout_opt st =
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
    77
  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
    78
                  |> 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
    79
    [] => (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
    80
  | xs as (s, _) :: _ =>
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    81
    let
39332
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    82
      val xs = xs |> map swap |> AList.coalesce (op =)
538b94dc62de make Try's output more concise
blanchet
parents: 39331
diff changeset
    83
                  |> map (swap o apsnd commas)
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    84
      val message =
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    85
        (if auto then "Auto Try found a proof" else "Try this command") ^ ": " ^
38946
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    86
        Markup.markup Markup.sendback
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    87
            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    88
             " " ^ s) ^
39331
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    89
        ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n"
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    90
    in
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    91
      (true, st |> (if auto then
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    92
                      Proof.goal_message
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    93
                          (fn () => Pretty.chunks [Pretty.str "",
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    94
                                    Pretty.markup Markup.hilite
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    95
                                                  [Pretty.str message]])
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    96
                    else
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    97
                      tap (fn _ => priority message)))
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    98
    end
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
    99
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   100
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
   101
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   102
val tryN = "try"
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 _ =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   105
  Outer_Syntax.improper_command tryN
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   106
      "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
   107
      (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
   108
                                    o Toplevel.proof_of)))
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   109
39336
1899349a5026 change signature of "Try.invoke_try" to make it more flexible
blanchet
parents: 39334
diff changeset
   110
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
   111
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   112
val setup = Auto_Tools.register_tool (tryN, auto_try)
8b1969d603c0 added Auto Try to the mix of automatic tools
blanchet
parents: 39222
diff changeset
   113
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
   114
end;