author | blanchet |
Tue, 31 Aug 2010 20:24:28 +0200 | |
changeset 38942 | e10c11971fa7 |
child 38944 | 827c98e8ba8b |
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 |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
9 |
val timeout : int Unsynchronized.ref |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
10 |
val invoke_try : Proof.state -> unit |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
11 |
end; |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
12 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
13 |
structure Try : TRY = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
14 |
struct |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
15 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
16 |
fun can_apply time pre post tac st = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
17 |
let val {goal, ...} = Proof.goal st in |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
18 |
case TimeLimit.timeLimit time (Seq.pull o tac) (pre st) of |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
19 |
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
|
20 |
| NONE => false |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
21 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
22 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
23 |
fun do_generic command timeout pre post apply st = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
24 |
let val timer = Timer.startRealTimer () in |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
25 |
if can_apply timeout pre post apply st then |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
26 |
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
|
27 |
else |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
28 |
NONE |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
29 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
30 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
31 |
fun named_method thy name = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
32 |
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
|
33 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
34 |
fun apply_named_method name ctxt = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
35 |
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
|
36 |
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
|
37 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
38 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
39 |
fun do_named_method name timeout st = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
40 |
do_generic name timeout (#goal o Proof.goal) snd |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
41 |
(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
|
42 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
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
|
46 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
47 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
48 |
fun do_named_method_on_first_goal name timeout st = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
49 |
do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]" |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
50 |
else "")) timeout I (#goal o Proof.goal) |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
51 |
(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
|
52 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
53 |
val all_goals_named_methods = ["auto", "safe"] |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
54 |
val first_goal_named_methods = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
55 |
["simp", "fast", "fastsimp", "force", "best", "blast"] |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
56 |
val do_methods = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
60 |
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
|
61 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
62 |
val timeout = Unsynchronized.ref 5 |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
63 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
64 |
fun invoke_try st = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
65 |
case do_methods |> Par_List.map (fn f => f (Time.fromSeconds (!timeout)) st) |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
66 |
|> map_filter I |> sort (int_ord o pairself snd) of |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
67 |
[] => writeln "Tried." |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
68 |
| xs as (s, _) :: _ => |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
69 |
priority ("Try this command: " ^ |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
70 |
Markup.markup Markup.sendback ("apply " ^ s) ^ ".\n" ^ |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
71 |
"(" ^ space_implode "; " (map time_string xs) ^ ")\n") |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
72 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
73 |
val tryN = "try" |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
74 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
75 |
val _ = |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
76 |
Outer_Syntax.improper_command tryN |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
77 |
"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
|
78 |
(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
|
79 |
|
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
80 |
end; |