|
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 timeout : int Unsynchronized.ref |
|
10 val invoke_try : Proof.state -> unit |
|
11 end; |
|
12 |
|
13 structure Try : TRY = |
|
14 struct |
|
15 |
|
16 fun can_apply time pre post tac st = |
|
17 let val {goal, ...} = Proof.goal st in |
|
18 case TimeLimit.timeLimit time (Seq.pull o tac) (pre st) of |
|
19 SOME (x, _) => nprems_of (post x) < nprems_of goal |
|
20 | NONE => false |
|
21 end |
|
22 |
|
23 fun do_generic command timeout pre post apply st = |
|
24 let val timer = Timer.startRealTimer () in |
|
25 if can_apply timeout pre post apply st then |
|
26 SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer)) |
|
27 else |
|
28 NONE |
|
29 end |
|
30 |
|
31 fun named_method thy name = |
|
32 Method.method thy (Args.src ((name, []), Position.none)) |
|
33 |
|
34 fun apply_named_method name ctxt = |
|
35 let val thy = ProofContext.theory_of ctxt in |
|
36 Method.apply (named_method thy name) ctxt [] |
|
37 end |
|
38 |
|
39 fun do_named_method name timeout st = |
|
40 do_generic name timeout (#goal o Proof.goal) snd |
|
41 (apply_named_method name (Proof.context_of st)) st |
|
42 |
|
43 fun apply_named_method_on_first_goal name ctxt = |
|
44 let val thy = ProofContext.theory_of ctxt in |
|
45 Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name))) |
|
46 end |
|
47 |
|
48 fun do_named_method_on_first_goal name timeout st = |
|
49 do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]" |
|
50 else "")) timeout I (#goal o Proof.goal) |
|
51 (apply_named_method_on_first_goal name (Proof.context_of st)) st |
|
52 |
|
53 val all_goals_named_methods = ["auto", "safe"] |
|
54 val first_goal_named_methods = |
|
55 ["simp", "fast", "fastsimp", "force", "best", "blast"] |
|
56 val do_methods = |
|
57 map do_named_method_on_first_goal all_goals_named_methods @ |
|
58 map do_named_method first_goal_named_methods |
|
59 |
|
60 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" |
|
61 |
|
62 val timeout = Unsynchronized.ref 5 |
|
63 |
|
64 fun invoke_try st = |
|
65 case do_methods |> Par_List.map (fn f => f (Time.fromSeconds (!timeout)) st) |
|
66 |> map_filter I |> sort (int_ord o pairself snd) of |
|
67 [] => writeln "Tried." |
|
68 | xs as (s, _) :: _ => |
|
69 priority ("Try this command: " ^ |
|
70 Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^ |
|
71 "(" ^ space_implode "; " (map time_string xs) ^ ")\n") |
|
72 |
|
73 val tryN = "try" |
|
74 |
|
75 val _ = |
|
76 Outer_Syntax.improper_command tryN |
|
77 "try a combination of proof methods" Keyword.diag |
|
78 (Scan.succeed (Toplevel.keep (invoke_try o Toplevel.proof_of))) |
|
79 |
|
80 end; |