src/HOL/Tools/try.ML
author blanchet
Wed, 08 Sep 2010 15:57:50 +0200
changeset 39222 decf607a5a67
parent 38946 da5e4f182f69
child 39331 8b1969d603c0
permissions -rw-r--r--
remove "safe" (as suggested by Tobias) and added "arith" to "try"
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
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
     9
  val invoke_try : Proof.state -> unit
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    10
end;
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    11
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    12
structure Try : TRY =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    13
struct
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    14
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    15
val timeout = Time.fromSeconds 5
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    16
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    17
fun can_apply pre post tac st =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    18
  let val {goal, ...} = Proof.goal st in
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    19
    case TimeLimit.timeLimit timeout (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
    20
      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
    21
    | NONE => false
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    22
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    23
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    24
fun do_generic command pre post apply st =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    25
  let val timer = Timer.startRealTimer () in
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    26
    if can_apply pre post apply st then
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    27
      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
    28
    else
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    29
      NONE
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    30
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    31
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    32
fun named_method thy name =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    33
  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
    34
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    35
fun apply_named_method name ctxt =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    36
  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
    37
    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
    38
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    39
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    40
fun do_named_method name st =
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    41
  do_generic 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
    42
             (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
    43
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    44
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
    45
  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
    46
    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
    47
  end
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    48
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    49
fun do_named_method_on_first_goal name st =
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    50
  do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    51
                      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
    52
             (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
    53
39222
decf607a5a67 remove "safe" (as suggested by Tobias) and added "arith" to "try"
blanchet
parents: 38946
diff changeset
    54
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
    55
val first_goal_named_methods =
39222
decf607a5a67 remove "safe" (as suggested by Tobias) and added "arith" to "try"
blanchet
parents: 38946
diff changeset
    56
  ["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
    57
val do_methods =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    58
  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
    59
  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
    60
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    61
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
    62
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    63
fun invoke_try st =
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    64
  case do_methods |> Par_List.map (fn f => f st)
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    65
                  |> map_filter I |> sort (int_ord o pairself snd) of
38944
827c98e8ba8b fiddling with "try"
blanchet
parents: 38942
diff changeset
    66
    [] => writeln "No proof found."
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    67
  | xs as (s, _) :: _ =>
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    68
    priority ("Try this command: " ^
38946
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    69
        Markup.markup Markup.sendback
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    70
            ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    71
             " " ^ s) ^
da5e4f182f69 distinguish between "by" and "apply"
blanchet
parents: 38944
diff changeset
    72
        ".\n(" ^ space_implode "; " (map time_string xs) ^ ")\n")
38942
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
val tryN = "try"
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
val _ =
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    77
  Outer_Syntax.improper_command tryN
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    78
      "try a combination of proof methods" Keyword.diag
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    79
      (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of)))
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    80
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff changeset
    81
end;