author | blanchet |
Thu, 30 Jan 2014 13:38:28 +0100 | |
changeset 55177 | b7ca9f98faca |
parent 54431 | e98996c2a32c |
child 55178 | 318cd8ac1817 |
permissions | -rw-r--r-- |
46641 | 1 |
(* Title: HOL/Tools/try0.ML |
38942
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 |
|
46641 | 7 |
signature TRY0 = |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
8 |
sig |
46641 | 9 |
val try0N : string |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
10 |
val noneN : string |
55177 | 11 |
|
12 |
val silence_methods : bool -> Proof.context -> Proof.context |
|
46641 | 13 |
val try0 : |
42179 | 14 |
Time.time option -> string list * string list * string list * string list |
15 |
-> Proof.state -> bool |
|
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
16 |
end; |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
17 |
|
46641 | 18 |
structure Try0 : TRY0 = |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
19 |
struct |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
20 |
|
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
21 |
datatype mode = Auto_Try | Try | Normal |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
22 |
|
46641 | 23 |
val try0N = "try0" |
43020
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
24 |
|
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
25 |
val noneN = "none" |
abb5d1f907e4
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
blanchet
parents:
43018
diff
changeset
|
26 |
|
39333 | 27 |
val _ = |
52639 | 28 |
ProofGeneral.preference_option ProofGeneral.category_tracing |
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset
|
29 |
NONE |
52717
da7bf8b3d24a
clarified option name, with improved sort order wrt. "time" options;
wenzelm
parents:
52697
diff
changeset
|
30 |
@{option auto_methods} |
52017
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset
|
31 |
"auto-try0" |
bc0238c1f73a
clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
wenzelm
parents:
52007
diff
changeset
|
32 |
"Try standard proof methods" |
39333 | 33 |
|
40301 | 34 |
val default_timeout = seconds 5.0 |
38944 | 35 |
|
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
36 |
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
|
37 |
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
|
38 |
case (case timeout_opt of |
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
39 |
SOME timeout => TimeLimit.timeLimit timeout |
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
40 |
| 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
|
41 |
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
|
42 |
| NONE => false |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
43 |
end |
40113
1f61f0826e8a
handle timeouts (to prevent failure from other threads);
blanchet
parents:
39719
diff
changeset
|
44 |
handle TimeLimit.TimeOut => false |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
45 |
|
54291 | 46 |
fun do_generic timeout_opt name command pre post apply st = |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
47 |
let val timer = Timer.startRealTimer () in |
39336
1899349a5026
change signature of "Try.invoke_try" to make it more flexible
blanchet
parents:
39334
diff
changeset
|
48 |
if can_apply timeout_opt pre post apply st then |
54291 | 49 |
SOME (name, command, Time.toMilliseconds (Timer.checkRealTimer timer)) |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
50 |
else |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
51 |
NONE |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
52 |
end |
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
53 |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
54 |
val parse_method = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
55 |
enclose "(" ")" |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
56 |
#> Outer_Syntax.scan Position.start |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
57 |
#> filter Token.is_proper |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
58 |
#> Scan.read Token.stopper Method.parse |
49866 | 59 |
#> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source") |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
60 |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
61 |
fun apply_named_method_on_first_goal method thy = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
62 |
method |> parse_method |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
63 |
|> Method.method thy |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
64 |
|> Method.Basic |
51383 | 65 |
|> curry Method.Select_Goals 1 |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
66 |
|> Proof.refine |
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
|
67 |
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
|
68 |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
69 |
fun add_attr_text (NONE, _) s = s |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
70 |
| add_attr_text (_, []) s = s |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
71 |
| add_attr_text (SOME x, fs) s = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
72 |
s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs |
42179 | 73 |
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) = |
74 |
"" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)] |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
75 |
|
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
76 |
fun do_named_method (name, ((all_goals, run_if_auto_try), attrs)) mode |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
77 |
timeout_opt quad st = |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
78 |
if mode <> Auto_Try orelse run_if_auto_try then |
42179 | 79 |
let val attrs = attrs_text attrs quad in |
54291 | 80 |
do_generic timeout_opt name |
81 |
((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^ |
|
82 |
(if all_goals andalso nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else "")) |
|
83 |
I (#goal o Proof.goal) |
|
84 |
(apply_named_method_on_first_goal (name ^ attrs) (Proof.theory_of st)) st |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
85 |
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
|
86 |
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
|
87 |
NONE |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
88 |
|
42179 | 89 |
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest") |
90 |
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest") |
|
91 |
val simp_attrs = (SOME "add", NONE, NONE, NONE) |
|
92 |
val metis_attrs = (SOME "", SOME "", SOME "", SOME "") |
|
93 |
val no_attrs = (NONE, NONE, NONE, NONE) |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
94 |
|
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
95 |
(* name * ((all_goals, run_if_auto_try), (simp, intro, elim, dest) *) |
39547 | 96 |
val named_methods = |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
97 |
[("simp", ((false, true), simp_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
98 |
("auto", ((true, true), full_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
99 |
("fast", ((false, false), clas_attrs)), |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44651
diff
changeset
|
100 |
("fastforce", ((false, false), full_attrs)), |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
101 |
("force", ((false, false), full_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
102 |
("blast", ((false, true), clas_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
103 |
("metis", ((false, true), metis_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
104 |
("linarith", ((false, true), no_attrs)), |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
105 |
("presburger", ((false, true), no_attrs))] |
39547 | 106 |
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
|
107 |
|
54248
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
108 |
fun time_string ms = string_of_int ms ^ " ms" |
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
109 |
fun tool_time_string (s, ms) = s ^ ": " ^ time_string ms |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
110 |
|
55177 | 111 |
(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification |
112 |
bound exceeded" warnings and the like. *) |
|
113 |
fun silence_methods debug = |
|
114 |
Config.put Metis_Tactic.verbose debug |
|
115 |
#> Config.put Lin_Arith.verbose debug |
|
116 |
#> (not debug ? |
|
117 |
(Context_Position.set_visible false |
|
118 |
#> Proof_Context.background_theory (fn thy => |
|
119 |
thy |
|
120 |
|> Context_Position.set_visible_global false |
|
121 |
|> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound)))) |
|
122 |
||
46641 | 123 |
fun do_try0 mode timeout_opt quad st = |
41038 | 124 |
let |
55177 | 125 |
val st = st |> Proof.map_context (silence_methods false) |
54431 | 126 |
fun trd (_, _, t) = t |
54248
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
127 |
fun par_map f = |
54431 | 128 |
if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd) |
54248
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
129 |
else Par_List.get_some f #> the_list |
41038 | 130 |
in |
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
131 |
if mode = Normal then |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
132 |
"Trying " ^ space_implode " " (Try.serial_commas "and" |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
133 |
(map (quote o fst) named_methods)) ^ "..." |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
134 |
|> Output.urgent_message |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
135 |
else |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
136 |
(); |
54291 | 137 |
(case par_map (fn f => f mode timeout_opt quad st) do_methods of |
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
138 |
[] => |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
139 |
(if mode = Normal then Output.urgent_message "No proof found." else (); |
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
140 |
(false, (noneN, st))) |
54291 | 141 |
| xs as (name, command, _) :: _ => |
41038 | 142 |
let |
54291 | 143 |
val xs = xs |> map (fn (name, _, n) => (n, name)) |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
144 |
|> AList.coalesce (op =) |
41038 | 145 |
|> map (swap o apsnd commas) |
146 |
val message = |
|
43026
0f15575a6465
handle non-auto try cases gracefully in Try Methods
blanchet
parents:
43024
diff
changeset
|
147 |
(case mode of |
52970 | 148 |
Auto_Try => "Auto Try0 found a proof" |
149 |
| Try => "Try0 found a proof" |
|
43031 | 150 |
| Normal => "Try this") ^ ": " ^ |
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
52970
diff
changeset
|
151 |
Active.sendback_markup [Markup.padding_command] |
41038 | 152 |
((if nprems_of (#goal (Proof.goal st)) = 1 then "by" |
54291 | 153 |
else "apply") ^ " " ^ command) ^ |
54248
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
154 |
(case xs of |
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
155 |
[(_, ms)] => " (" ^ time_string ms ^ ")." |
c7af3d651658
make 'try0' return faster when invoked as part of 'try'
blanchet
parents:
53052
diff
changeset
|
156 |
| xs => "\n(" ^ space_implode "; " (map tool_time_string xs) ^ ").") |
41038 | 157 |
in |
54291 | 158 |
(true, (name, |
159 |
st |> (if mode = Auto_Try then |
|
160 |
Proof.goal_message |
|
161 |
(fn () => Pretty.markup Markup.information [Pretty.str message]) |
|
162 |
else |
|
163 |
tap (fn _ => Output.urgent_message message)))) |
|
164 |
end) |
|
41038 | 165 |
end |
39331 | 166 |
|
46641 | 167 |
fun try0 timeout_opt = fst oo do_try0 Normal timeout_opt |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
168 |
|
46641 | 169 |
fun try0_trans quad = |
51557
4e4b56b7a3a5
more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
wenzelm
parents:
51383
diff
changeset
|
170 |
Toplevel.unknown_proof o |
46641 | 171 |
Toplevel.keep (K () o do_try0 Normal (SOME default_timeout) quad |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
172 |
o Toplevel.proof_of) |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
173 |
|
42179 | 174 |
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = |
175 |
(s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2) |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
176 |
|
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
177 |
fun string_of_xthm (xref, args) = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
178 |
Facts.string_of_ref xref ^ |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
179 |
implode (map (enclose "[" "]" o Pretty.str_of |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
180 |
o Args.pretty_src @{context}) args) |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
181 |
|
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
182 |
val parse_fact_refs = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
183 |
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
184 |
(Parse_Spec.xthm >> string_of_xthm)) |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
185 |
val parse_attr = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
186 |
Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs |
42179 | 187 |
>> (fn ss => (ss, [], [], [])) |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
188 |
|| Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs |
42179 | 189 |
>> (fn is => ([], is, [], [])) |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
190 |
|| Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs |
42179 | 191 |
>> (fn es => ([], [], es, [])) |
192 |
|| Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs |
|
193 |
>> (fn ds => ([], [], [], ds)) |
|
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
194 |
fun parse_attrs x = |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
195 |
(Args.parens parse_attrs |
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
196 |
|| Scan.repeat parse_attr |
42179 | 197 |
>> (fn quad => fold merge_attrs quad ([], [], [], []))) x |
41999
3c029ef9e0f2
added "simp:", "intro:", and "elim:" to "try" command
blanchet
parents:
41038
diff
changeset
|
198 |
|
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
199 |
val _ = |
46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46641
diff
changeset
|
200 |
Outer_Syntax.improper_command @{command_spec "try0"} |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46641
diff
changeset
|
201 |
"try a combination of proof methods" |
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46641
diff
changeset
|
202 |
(Scan.optional parse_attrs ([], [], [], []) #>> try0_trans) |
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
203 |
|
46641 | 204 |
fun try_try0 auto = |
205 |
do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []) |
|
39331 | 206 |
|
52717
da7bf8b3d24a
clarified option name, with improved sort order wrt. "time" options;
wenzelm
parents:
52697
diff
changeset
|
207 |
val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0)) |
39331 | 208 |
|
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
diff
changeset
|
209 |
end; |