blanchet@43857
|
1 |
(* Title: HOL/Tools/try_methods.ML
|
blanchet@39168
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
blanchet@39168
|
3 |
|
blanchet@39168
|
4 |
Try a combination of proof methods.
|
blanchet@39168
|
5 |
*)
|
blanchet@39168
|
6 |
|
blanchet@43857
|
7 |
signature TRY_METHODS =
|
blanchet@39168
|
8 |
sig
|
blanchet@43861
|
9 |
val try_methodsN : string
|
blanchet@43861
|
10 |
val noneN : string
|
blanchet@39577
|
11 |
val auto : bool Unsynchronized.ref
|
blanchet@43857
|
12 |
val try_methods :
|
blanchet@43050
|
13 |
Time.time option -> string list * string list * string list * string list
|
blanchet@43050
|
14 |
-> Proof.state -> bool
|
blanchet@39577
|
15 |
val setup : theory -> theory
|
blanchet@39168
|
16 |
end;
|
blanchet@39168
|
17 |
|
blanchet@43857
|
18 |
structure Try_Methods : TRY_METHODS =
|
blanchet@39168
|
19 |
struct
|
blanchet@39168
|
20 |
|
blanchet@43861
|
21 |
val try_methodsN = "try_methods"
|
blanchet@43861
|
22 |
|
blanchet@43861
|
23 |
val noneN = "none"
|
blanchet@43861
|
24 |
|
blanchet@39577
|
25 |
val auto = Unsynchronized.ref false
|
blanchet@39577
|
26 |
|
blanchet@39579
|
27 |
val _ =
|
blanchet@39579
|
28 |
ProofGeneralPgip.add_preference Preferences.category_tracing
|
blanchet@43857
|
29 |
(Preferences.bool_pref auto "auto-try-methods"
|
blanchet@43857
|
30 |
"Try standard proof methods.")
|
blanchet@39579
|
31 |
|
wenzelm@40553
|
32 |
val default_timeout = seconds 5.0
|
blanchet@39170
|
33 |
|
blanchet@39582
|
34 |
fun can_apply timeout_opt pre post tac st =
|
blanchet@39168
|
35 |
let val {goal, ...} = Proof.goal st in
|
blanchet@39582
|
36 |
case (case timeout_opt of
|
blanchet@39582
|
37 |
SOME timeout => TimeLimit.timeLimit timeout
|
blanchet@39582
|
38 |
| NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
|
blanchet@39168
|
39 |
SOME (x, _) => nprems_of (post x) < nprems_of goal
|
blanchet@39168
|
40 |
| NONE => false
|
blanchet@39168
|
41 |
end
|
blanchet@40357
|
42 |
handle TimeLimit.TimeOut => false
|
blanchet@39168
|
43 |
|
blanchet@39582
|
44 |
fun do_generic timeout_opt command pre post apply st =
|
blanchet@39168
|
45 |
let val timer = Timer.startRealTimer () in
|
blanchet@39582
|
46 |
if can_apply timeout_opt pre post apply st then
|
blanchet@39168
|
47 |
SOME (command, Time.toMilliseconds (Timer.checkRealTimer timer))
|
blanchet@39168
|
48 |
else
|
blanchet@39168
|
49 |
NONE
|
blanchet@39168
|
50 |
end
|
blanchet@39168
|
51 |
|
blanchet@42870
|
52 |
val parse_method =
|
blanchet@42870
|
53 |
enclose "(" ")"
|
blanchet@42870
|
54 |
#> Outer_Syntax.scan Position.start
|
blanchet@42870
|
55 |
#> filter Token.is_proper
|
blanchet@42870
|
56 |
#> Scan.read Token.stopper Method.parse
|
blanchet@42870
|
57 |
#> (fn SOME (Method.Source src) => src | _ => raise Fail "expected Source")
|
blanchet@39168
|
58 |
|
blanchet@42870
|
59 |
fun apply_named_method_on_first_goal method thy =
|
blanchet@42870
|
60 |
method |> parse_method
|
blanchet@42870
|
61 |
|> Method.method thy
|
blanchet@42870
|
62 |
|> Method.Basic
|
blanchet@42870
|
63 |
|> curry Method.SelectGoals 1
|
blanchet@42870
|
64 |
|> Proof.refine
|
blanchet@40463
|
65 |
handle ERROR _ => K Seq.empty (* e.g., the method isn't available yet *)
|
blanchet@39168
|
66 |
|
blanchet@42870
|
67 |
fun add_attr_text (NONE, _) s = s
|
blanchet@42870
|
68 |
| add_attr_text (_, []) s = s
|
blanchet@42870
|
69 |
| add_attr_text (SOME x, fs) s =
|
blanchet@42870
|
70 |
s ^ " " ^ (if x = "" then "" else x ^ ": ") ^ space_implode " " fs
|
blanchet@43050
|
71 |
fun attrs_text (sx, ix, ex, dx) (ss, is, es, ds) =
|
blanchet@43050
|
72 |
"" |> fold add_attr_text [(sx, ss), (ix, is), (ex, es), (dx, ds)]
|
blanchet@42870
|
73 |
|
blanchet@42870
|
74 |
fun do_named_method (name, ((all_goals, run_if_auto), attrs)) auto timeout_opt
|
blanchet@43050
|
75 |
quad st =
|
blanchet@40463
|
76 |
if not auto orelse run_if_auto then
|
blanchet@43050
|
77 |
let val attrs = attrs_text attrs quad in
|
blanchet@42870
|
78 |
do_generic timeout_opt
|
blanchet@42870
|
79 |
(name ^ (if all_goals andalso
|
blanchet@42870
|
80 |
nprems_of (#goal (Proof.goal st)) > 1 then
|
blanchet@42870
|
81 |
"[1]"
|
blanchet@42870
|
82 |
else
|
blanchet@42870
|
83 |
"") ^
|
blanchet@42870
|
84 |
attrs) I (#goal o Proof.goal)
|
blanchet@42870
|
85 |
(apply_named_method_on_first_goal (name ^ attrs)
|
blanchet@42870
|
86 |
(Proof.theory_of st)) st
|
blanchet@42870
|
87 |
end
|
blanchet@40463
|
88 |
else
|
blanchet@40463
|
89 |
NONE
|
blanchet@39168
|
90 |
|
blanchet@43050
|
91 |
val full_attrs = (SOME "simp", SOME "intro", SOME "elim", SOME "dest")
|
blanchet@43050
|
92 |
val clas_attrs = (NONE, SOME "intro", SOME "elim", SOME "dest")
|
blanchet@43050
|
93 |
val simp_attrs = (SOME "add", NONE, NONE, NONE)
|
blanchet@43050
|
94 |
val metis_attrs = (SOME "", SOME "", SOME "", SOME "")
|
blanchet@43050
|
95 |
val no_attrs = (NONE, NONE, NONE, NONE)
|
blanchet@42870
|
96 |
|
blanchet@43050
|
97 |
(* name * ((all_goals, run_if_auto), (simp, intro, elim, dest) *)
|
blanchet@39769
|
98 |
val named_methods =
|
blanchet@42870
|
99 |
[("simp", ((false, true), simp_attrs)),
|
blanchet@42870
|
100 |
("auto", ((true, true), full_attrs)),
|
blanchet@42870
|
101 |
("fast", ((false, false), clas_attrs)),
|
blanchet@42870
|
102 |
("fastsimp", ((false, false), full_attrs)),
|
blanchet@42870
|
103 |
("force", ((false, false), full_attrs)),
|
blanchet@42870
|
104 |
("blast", ((false, true), clas_attrs)),
|
blanchet@42870
|
105 |
("metis", ((false, true), metis_attrs)),
|
blanchet@42870
|
106 |
("linarith", ((false, true), no_attrs)),
|
blanchet@42870
|
107 |
("presburger", ((false, true), no_attrs))]
|
blanchet@39769
|
108 |
val do_methods = map do_named_method named_methods
|
blanchet@39168
|
109 |
|
blanchet@39168
|
110 |
fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
|
blanchet@39168
|
111 |
|
blanchet@43857
|
112 |
fun do_try_methods auto timeout_opt quad st =
|
blanchet@41286
|
113 |
let
|
blanchet@41286
|
114 |
val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
|
blanchet@41286
|
115 |
in
|
blanchet@43050
|
116 |
case do_methods |> Par_List.map (fn f => f auto timeout_opt quad st)
|
blanchet@41286
|
117 |
|> map_filter I |> sort (int_ord o pairself snd) of
|
blanchet@43861
|
118 |
[] => (if auto then () else writeln "No proof found.";
|
blanchet@43861
|
119 |
(false, (noneN, st)))
|
blanchet@41286
|
120 |
| xs as (s, _) :: _ =>
|
blanchet@41286
|
121 |
let
|
blanchet@42870
|
122 |
val xs = xs |> map (fn (s, n) => (n, hd (space_explode " " s)))
|
blanchet@42870
|
123 |
|> AList.coalesce (op =)
|
blanchet@41286
|
124 |
|> map (swap o apsnd commas)
|
blanchet@42870
|
125 |
val need_parens = exists_string (curry (op =) " ") s
|
blanchet@41286
|
126 |
val message =
|
blanchet@43857
|
127 |
(if auto then "Auto Try Methods found a proof"
|
blanchet@43857
|
128 |
else "Try this command") ^ ": " ^
|
blanchet@41286
|
129 |
Markup.markup Markup.sendback
|
blanchet@41286
|
130 |
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
|
blanchet@42870
|
131 |
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
|
blanchet@41286
|
132 |
"\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
|
blanchet@41286
|
133 |
in
|
blanchet@43861
|
134 |
(true, (s, st |> (if auto then
|
blanchet@43861
|
135 |
Proof.goal_message
|
blanchet@43861
|
136 |
(fn () => Pretty.chunks [Pretty.str "",
|
blanchet@43861
|
137 |
Pretty.markup Markup.hilite
|
blanchet@43861
|
138 |
[Pretty.str message]])
|
blanchet@43861
|
139 |
else
|
blanchet@43861
|
140 |
tap (fn _ => Output.urgent_message message))))
|
blanchet@41286
|
141 |
end
|
blanchet@41286
|
142 |
end
|
blanchet@39577
|
143 |
|
blanchet@43857
|
144 |
fun try_methods timeout_opt = fst oo do_try_methods false timeout_opt
|
blanchet@39168
|
145 |
|
blanchet@43857
|
146 |
fun try_methods_trans quad =
|
blanchet@43857
|
147 |
Toplevel.keep (K () o do_try_methods false (SOME default_timeout) quad
|
blanchet@42870
|
148 |
o Toplevel.proof_of)
|
blanchet@42870
|
149 |
|
blanchet@43050
|
150 |
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) =
|
blanchet@43050
|
151 |
(s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2)
|
blanchet@42870
|
152 |
|
blanchet@42870
|
153 |
fun string_of_xthm (xref, args) =
|
blanchet@42870
|
154 |
Facts.string_of_ref xref ^
|
blanchet@42870
|
155 |
implode (map (enclose "[" "]" o Pretty.str_of
|
blanchet@42870
|
156 |
o Args.pretty_src @{context}) args)
|
blanchet@42870
|
157 |
|
blanchet@42870
|
158 |
val parse_fact_refs =
|
blanchet@42870
|
159 |
Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
|
blanchet@42870
|
160 |
(Parse_Spec.xthm >> string_of_xthm))
|
blanchet@42870
|
161 |
val parse_attr =
|
blanchet@42870
|
162 |
Args.$$$ "simp" |-- Args.colon |-- parse_fact_refs
|
blanchet@43050
|
163 |
>> (fn ss => (ss, [], [], []))
|
blanchet@42870
|
164 |
|| Args.$$$ "intro" |-- Args.colon |-- parse_fact_refs
|
blanchet@43050
|
165 |
>> (fn is => ([], is, [], []))
|
blanchet@42870
|
166 |
|| Args.$$$ "elim" |-- Args.colon |-- parse_fact_refs
|
blanchet@43050
|
167 |
>> (fn es => ([], [], es, []))
|
blanchet@43050
|
168 |
|| Args.$$$ "dest" |-- Args.colon |-- parse_fact_refs
|
blanchet@43050
|
169 |
>> (fn ds => ([], [], [], ds))
|
blanchet@42870
|
170 |
fun parse_attrs x =
|
blanchet@42870
|
171 |
(Args.parens parse_attrs
|
blanchet@42870
|
172 |
|| Scan.repeat parse_attr
|
blanchet@43050
|
173 |
>> (fn quad => fold merge_attrs quad ([], [], [], []))) x
|
blanchet@42870
|
174 |
|
blanchet@43857
|
175 |
val parse_try_methods_command =
|
blanchet@43857
|
176 |
Scan.optional parse_attrs ([], [], [], []) #>> try_methods_trans
|
blanchet@42870
|
177 |
|
blanchet@39168
|
178 |
val _ =
|
blanchet@43857
|
179 |
Outer_Syntax.improper_command try_methodsN
|
blanchet@43857
|
180 |
"try a combination of proof methods" Keyword.diag
|
blanchet@43857
|
181 |
parse_try_methods_command
|
blanchet@39168
|
182 |
|
blanchet@43861
|
183 |
fun try_try_methods auto = do_try_methods auto NONE ([], [], [], [])
|
blanchet@39577
|
184 |
|
blanchet@43865
|
185 |
val setup = Try.register_tool (try_methodsN, (20, auto, try_try_methods))
|
blanchet@39577
|
186 |
|
blanchet@39168
|
187 |
end;
|