author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 64573 | e6aee01da22d |
child 73292 | f84a93f1de2f |
permissions | -rw-r--r-- |
47847 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle.ML |
32564 | 2 |
Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
32381 | 3 |
*) |
4 |
||
5 |
signature MIRABELLE = |
|
6 |
sig |
|
32564 | 7 |
(*configuration*) |
32396 | 8 |
val logfile : string Config.T |
32381 | 9 |
val timeout : int Config.T |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
10 |
val start_line : int Config.T |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset
|
11 |
val end_line : int Config.T |
32381 | 12 |
|
32564 | 13 |
(*core*) |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
14 |
type init_action = int -> theory -> theory |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
15 |
type done_args = {last: Toplevel.state, log: string -> unit} |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
16 |
type done_action = int -> done_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
17 |
type run_args = {pre: Proof.state, post: Toplevel.state option, |
32676 | 18 |
timeout: Time.time, log: string -> unit, pos: Position.T, name: string} |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
19 |
type run_action = int -> run_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
20 |
type action = init_action * run_action * done_action |
32521 | 21 |
val catch : (int -> string) -> run_action -> run_action |
34052 | 22 |
val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> |
23 |
int -> run_args -> 'a |
|
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
24 |
val register : action -> theory -> theory |
32495 | 25 |
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
26 |
unit |
|
27 |
||
32564 | 28 |
(*utility functions*) |
32469 | 29 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
30 |
Proof.state -> bool |
|
60361 | 31 |
val theorems_in_proof_term : theory -> thm -> thm list |
33243 | 32 |
val theorems_of_sucessful_proof : Toplevel.state option -> thm list |
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
33 |
val get_setting : (string * string) list -> string * string -> string |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
34 |
val get_int_setting : (string * string) list -> string * int -> int |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
35 |
val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
32381 | 36 |
end |
37 |
||
38 |
||
39 |
||
32497 | 40 |
structure Mirabelle : MIRABELLE = |
32495 | 41 |
struct |
42 |
||
43 |
(* Mirabelle configuration *) |
|
44 |
||
69597 | 45 |
val logfile = Attrib.setup_config_string \<^binding>\<open>mirabelle_logfile\<close> (K "") |
46 |
val timeout = Attrib.setup_config_int \<^binding>\<open>mirabelle_timeout\<close> (K 30) |
|
47 |
val start_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_start_line\<close> (K 0) |
|
48 |
val end_line = Attrib.setup_config_int \<^binding>\<open>mirabelle_end_line\<close> (K ~1) |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
49 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
50 |
|
32381 | 51 |
(* Mirabelle core *) |
52 |
||
32521 | 53 |
type init_action = int -> theory -> theory |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
54 |
type done_args = {last: Toplevel.state, log: string -> unit} |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
55 |
type done_action = int -> done_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
56 |
type run_args = {pre: Proof.state, post: Toplevel.state option, |
32676 | 57 |
timeout: Time.time, log: string -> unit, pos: Position.T, name: string} |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
58 |
type run_action = int -> run_args -> unit |
32521 | 59 |
type action = init_action * run_action * done_action |
32381 | 60 |
|
33522 | 61 |
structure Actions = Theory_Data |
32381 | 62 |
( |
32521 | 63 |
type T = (int * run_action * done_action) list |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
64 |
val empty = [] |
32381 | 65 |
val extend = I |
41481 | 66 |
fun merge data = Library.merge (K true) data (* FIXME potential data loss because of (K true) *) |
32381 | 67 |
) |
68 |
||
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
69 |
|
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
70 |
fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e) |
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
71 |
|
34052 | 72 |
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ()) |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
36787
diff
changeset
|
73 |
handle exn => |
62505 | 74 |
if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ()) |
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
75 |
|
34052 | 76 |
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
36787
diff
changeset
|
77 |
handle exn => |
62505 | 78 |
if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d) |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
79 |
|
32521 | 80 |
fun register (init, run, done) thy = |
81 |
let val id = length (Actions.get thy) + 1 |
|
82 |
in |
|
83 |
thy |
|
84 |
|> init id |
|
85 |
|> Actions.map (cons (id, run, done)) |
|
86 |
end |
|
32381 | 87 |
|
88 |
local |
|
89 |
||
90 |
fun log thy s = |
|
91 |
let fun append_to n = if n = "" then K () else File.append (Path.explode n) |
|
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
92 |
in append_to (Config.get_global thy logfile) (s ^ "\n") end |
32381 | 93 |
(* FIXME: with multithreading and parallel proofs enabled, we might need to |
94 |
encapsulate this inside a critical section *) |
|
95 |
||
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
96 |
fun log_sep thy = log thy "------------------" |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
97 |
|
32676 | 98 |
fun apply_actions thy pos name info (pre, post, time) actions = |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
99 |
let |
32676 | 100 |
fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} |
32521 | 101 |
fun run (id, run, _) = (apply (run id); log_sep thy) |
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
102 |
in (log thy info; log_sep thy; List.app run actions) end |
32381 | 103 |
|
104 |
fun in_range _ _ NONE = true |
|
105 |
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) |
|
106 |
||
107 |
fun only_within_range thy pos f x = |
|
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
108 |
let val l = Config.get_global thy start_line and r = Config.get_global thy end_line |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
109 |
in if in_range l r (Position.line_of pos) then f x else () end |
32381 | 110 |
|
111 |
in |
|
112 |
||
32521 | 113 |
fun run_actions tr pre post = |
32381 | 114 |
let |
115 |
val thy = Proof.theory_of pre |
|
116 |
val pos = Toplevel.pos_of tr |
|
117 |
val name = Toplevel.name_of tr |
|
36787
f60e4dd6d76f
renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
wenzelm
parents:
36001
diff
changeset
|
118 |
val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout)) |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
119 |
|
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
120 |
val str0 = string_of_int o the_default 0 |
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
42616
diff
changeset
|
121 |
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
122 |
val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" |
32381 | 123 |
in |
32676 | 124 |
only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) |
32381 | 125 |
end |
126 |
||
32521 | 127 |
fun done_actions st = |
128 |
let |
|
129 |
val thy = Toplevel.theory_of st |
|
130 |
val _ = log thy "\n\n"; |
|
131 |
in |
|
132 |
thy |
|
133 |
|> Actions.get |
|
134 |
|> List.app (fn (id, _, done) => done id {last=st, log=log thy}) |
|
135 |
end |
|
136 |
||
32381 | 137 |
end |
138 |
||
32504 | 139 |
val whitelist = ["apply", "by", "proof"] |
32468
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
140 |
|
32381 | 141 |
fun step_hook tr pre post = |
142 |
(* FIXME: might require wrapping into "interruptible" *) |
|
143 |
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso |
|
32504 | 144 |
member (op =) whitelist (Toplevel.name_of tr) |
32521 | 145 |
then run_actions tr (Toplevel.proof_of pre) (SOME post) |
146 |
else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post |
|
147 |
then done_actions pre |
|
32381 | 148 |
else () (* FIXME: add theory_hook here *) |
149 |
||
150 |
||
151 |
||
152 |
(* Mirabelle utility functions *) |
|
153 |
||
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
154 |
fun can_apply time tac st = |
32469 | 155 |
let |
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset
|
156 |
val {context = ctxt, facts, goal} = Proof.goal st |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
60361
diff
changeset
|
157 |
val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt) |
32381 | 158 |
in |
62519 | 159 |
(case try (Timeout.apply time (Seq.pull o full_tac)) goal of |
39451
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
160 |
SOME (SOME _) => true |
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
161 |
| _ => false) |
32381 | 162 |
end |
163 |
||
164 |
local |
|
165 |
||
166 |
fun fold_body_thms f = |
|
167 |
let |
|
64573 | 168 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) => |
32381 | 169 |
fn (x, seen) => |
170 |
if Inttab.defined seen i then (x, seen) |
|
171 |
else |
|
172 |
let |
|
64573 | 173 |
val name = Proofterm.thm_node_name thm_node |
174 |
val prop = Proofterm.thm_node_prop thm_node |
|
175 |
val body = Future.join (Proofterm.thm_node_body thm_node) |
|
176 |
val (x', seen') = app (n + (if name = "" then 0 else 1)) body |
|
32381 | 177 |
(x, Inttab.update (i, ()) seen) |
64573 | 178 |
in (x' |> n = 0 ? f (name, prop, body), seen') end) |
32381 | 179 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
180 |
||
181 |
in |
|
182 |
||
60361 | 183 |
fun theorems_in_proof_term thy thm = |
32381 | 184 |
let |
60361 | 185 |
val all_thms = Global_Theory.all_thms_of thy true |
32381 | 186 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
187 |
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
188 |
fun resolve_thms names = map_filter (member_of names) all_thms |
|
189 |
in |
|
190 |
resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
191 |
end |
|
192 |
||
193 |
end |
|
194 |
||
195 |
fun theorems_of_sucessful_proof state = |
|
196 |
(case state of |
|
197 |
NONE => [] |
|
198 |
| SOME st => |
|
199 |
if not (Toplevel.is_proof st) then [] |
|
60361 | 200 |
else |
201 |
theorems_in_proof_term (Toplevel.theory_of st) (#goal (Proof.goal (Toplevel.proof_of st)))) |
|
32381 | 202 |
|
203 |
fun get_setting settings (key, default) = |
|
204 |
the_default default (AList.lookup (op =) settings key) |
|
205 |
||
206 |
fun get_int_setting settings (key, default) = |
|
207 |
(case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
208 |
SOME (SOME i) => i |
|
209 |
| SOME NONE => error ("bad option: " ^ key) |
|
210 |
| NONE => default) |
|
211 |
||
42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
212 |
fun cpu_time f x = |
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
213 |
let val ({cpu, ...}, y) = Timing.timing f x |
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
214 |
in (y, Time.toMilliseconds cpu) end |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
215 |
|
32381 | 216 |
end |