author | blanchet |
Mon, 06 Dec 2010 14:47:58 +0100 | |
changeset 41038 | 9592334001d5 |
parent 40931 | 061b8257ab9f |
child 41999 | 3c029ef9e0f2 |
permissions | -rw-r--r-- |
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 | 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 | 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 | 17 |
val auto = Unsynchronized.ref false |
18 |
||
39333 | 19 |
val _ = |
20 |
ProofGeneralPgip.add_preference Preferences.category_tracing |
|
40222
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
21 |
(Preferences.bool_pref auto "auto-try" "Try standard proof methods.") |
39333 | 22 |
|
40301 | 23 |
val default_timeout = seconds 5.0 |
38944 | 24 |
|
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
case (case timeout_opt of |
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
28 |
SOME timeout => TimeLimit.timeLimit timeout |
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
29 |
| 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
|
30 |
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
|
31 |
| NONE => false |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
32 |
end |
40113
1f61f0826e8a
handle timeouts (to prevent failure from other threads);
blanchet
parents:
39719
diff
changeset
|
33 |
handle TimeLimit.TimeOut => false |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
34 |
|
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
35 |
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
|
36 |
let val timer = Timer.startRealTimer () in |
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
37 |
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
|
38 |
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
|
39 |
else |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
40 |
NONE |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
41 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
42 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
43 |
fun named_method thy name = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
44 |
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
|
45 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
46 |
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
|
47 |
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
|
48 |
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
|
49 |
end |
40222
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
50 |
handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *) |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
51 |
|
40222
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
52 |
fun do_named_method (name, (all_goals, run_if_auto)) auto timeout_opt st = |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
53 |
if not auto orelse run_if_auto then |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
54 |
do_generic timeout_opt |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
55 |
(name ^ (if all_goals andalso |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
56 |
nprems_of (#goal (Proof.goal st)) > 1 then |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
57 |
"[1]" |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
58 |
else |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
59 |
"")) I (#goal o Proof.goal) |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
60 |
(apply_named_method_on_first_goal name (Proof.context_of st)) st |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
61 |
else |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
62 |
NONE |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
63 |
|
40222
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
64 |
(* name * (all_goals, run_if_auto) *) |
39547 | 65 |
val named_methods = |
40222
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
66 |
[("simp", (false, true)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
67 |
("auto", (true, true)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
68 |
("fast", (false, false)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
69 |
("fastsimp", (false, false)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
70 |
("force", (false, false)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
71 |
("blast", (false, true)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
72 |
("metis", (false, true)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
73 |
("linarith", (false, true)), |
cd6d2b0a4096
reintroduced Auto Try, but this time really off by default -- and leave some classical+simp reasoners out for Auto Try (but keep them for Try)
blanchet
parents:
40132
diff
changeset
|
74 |
("presburger", (false, true))] |
39547 | 75 |
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
|
76 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
77 |
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
|
78 |
|
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
79 |
fun do_try auto timeout_opt st = |
41038 | 80 |
let |
81 |
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false) |
|
82 |
in |
|
83 |
case do_methods |> Par_List.map (fn f => f auto timeout_opt st) |
|
84 |
|> map_filter I |> sort (int_ord o pairself snd) of |
|
85 |
[] => (if auto then () else writeln "No proof found."; (false, st)) |
|
86 |
| xs as (s, _) :: _ => |
|
87 |
let |
|
88 |
val xs = xs |> map swap |> AList.coalesce (op =) |
|
89 |
|> map (swap o apsnd commas) |
|
90 |
val message = |
|
91 |
(if auto then "Auto Try found a proof" else "Try this command") ^ |
|
92 |
": " ^ |
|
93 |
Markup.markup Markup.sendback |
|
94 |
((if nprems_of (#goal (Proof.goal st)) = 1 then "by" |
|
95 |
else "apply") ^ " " ^ s) ^ |
|
96 |
"\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" |
|
97 |
in |
|
98 |
(true, st |> (if auto then |
|
99 |
Proof.goal_message |
|
100 |
(fn () => Pretty.chunks [Pretty.str "", |
|
101 |
Pretty.markup Markup.hilite |
|
102 |
[Pretty.str message]]) |
|
103 |
else |
|
104 |
tap (fn _ => Output.urgent_message message))) |
|
105 |
end |
|
106 |
end |
|
39331 | 107 |
|
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
108 |
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
|
109 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
110 |
val tryN = "try" |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
111 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
112 |
val _ = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
113 |
Outer_Syntax.improper_command tryN |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
114 |
"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
|
115 |
(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
|
116 |
o Toplevel.proof_of))) |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
117 |
|
40931 | 118 |
val auto_try = do_try true NONE |
39331 | 119 |
|
40931 | 120 |
val setup = Auto_Tools.register_tool (auto, auto_try) |
39331 | 121 |
|
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
122 |
end; |