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