author | boehmes |
Thu, 10 Dec 2009 18:10:59 +0100 | |
changeset 34052 | b2e6245fb3da |
parent 34035 | 08d34921b7dd |
child 35592 | 768d17f54125 |
permissions | -rw-r--r-- |
32564 | 1 |
(* Title: HOL/Mirabelle/Tools/mirabelle.ML |
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 |
32495 | 12 |
val setup : theory -> theory |
32381 | 13 |
|
32564 | 14 |
(*core*) |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
15 |
type init_action = int -> theory -> theory |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
16 |
type done_args = {last: Toplevel.state, log: string -> unit} |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
17 |
type done_action = int -> done_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
18 |
type run_args = {pre: Proof.state, post: Toplevel.state option, |
32676 | 19 |
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
|
20 |
type run_action = int -> run_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
21 |
type action = init_action * run_action * done_action |
32521 | 22 |
val catch : (int -> string) -> run_action -> run_action |
34052 | 23 |
val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> |
24 |
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
|
25 |
val register : action -> theory -> theory |
32495 | 26 |
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
27 |
unit |
|
28 |
||
32564 | 29 |
(*utility functions*) |
32381 | 30 |
val goal_thm_of : Proof.state -> thm |
32469 | 31 |
val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
32 |
Proof.state -> bool |
|
33243 | 33 |
val theorems_in_proof_term : thm -> thm list |
34 |
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
|
35 |
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
|
36 |
val get_int_setting : (string * string) list -> string * int -> int |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
37 |
val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
32381 | 38 |
end |
39 |
||
40 |
||
41 |
||
32497 | 42 |
structure Mirabelle : MIRABELLE = |
32495 | 43 |
struct |
44 |
||
45 |
(* Mirabelle configuration *) |
|
46 |
||
47 |
val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" |
|
48 |
val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 |
|
49 |
val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 |
|
50 |
val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 |
|
51 |
||
52 |
val setup = setup1 #> setup2 #> setup3 #> setup4 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
53 |
|
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
54 |
|
32381 | 55 |
(* Mirabelle core *) |
56 |
||
32521 | 57 |
type init_action = int -> theory -> theory |
32567
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
58 |
type done_args = {last: Toplevel.state, log: string -> unit} |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
59 |
type done_action = int -> done_args -> unit |
de411627a985
explicitly export type abbreviations (as usual in SML97);
wenzelm
parents:
32564
diff
changeset
|
60 |
type run_args = {pre: Proof.state, post: Toplevel.state option, |
32676 | 61 |
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
|
62 |
type run_action = int -> run_args -> unit |
32521 | 63 |
type action = init_action * run_action * done_action |
32381 | 64 |
|
33522 | 65 |
structure Actions = Theory_Data |
32381 | 66 |
( |
32521 | 67 |
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
|
68 |
val empty = [] |
32381 | 69 |
val extend = I |
33522 | 70 |
fun merge data = Library.merge (K true) data (* FIXME ?!? *) |
32381 | 71 |
) |
72 |
||
32515
e7c0d3c0494a
Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform),
boehmes
parents:
32504
diff
changeset
|
73 |
|
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
74 |
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
|
75 |
|
34052 | 76 |
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ()) |
77 |
handle (exn as Exn.Interrupt) => reraise exn |
|
78 |
| exn => (log_exn log tag id exn; ()) |
|
34035
08d34921b7dd
also consider the fully-typed version of metis for Mirabelle measurements
boehmes
parents:
33522
diff
changeset
|
79 |
|
34052 | 80 |
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st |
81 |
handle (exn as Exn.Interrupt) => reraise exn |
|
82 |
| exn => (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
|
83 |
|
32521 | 84 |
fun register (init, run, done) thy = |
85 |
let val id = length (Actions.get thy) + 1 |
|
86 |
in |
|
87 |
thy |
|
88 |
|> init id |
|
89 |
|> Actions.map (cons (id, run, done)) |
|
90 |
end |
|
32381 | 91 |
|
92 |
local |
|
93 |
||
94 |
fun log thy s = |
|
95 |
let fun append_to n = if n = "" then K () else File.append (Path.explode n) |
|
96 |
in append_to (Config.get_thy thy logfile) (s ^ "\n") end |
|
97 |
(* FIXME: with multithreading and parallel proofs enabled, we might need to |
|
98 |
encapsulate this inside a critical section *) |
|
99 |
||
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
100 |
fun log_sep thy = log thy "------------------" |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
101 |
|
32676 | 102 |
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
|
103 |
let |
32676 | 104 |
fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} |
32521 | 105 |
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
|
106 |
in (log thy info; log_sep thy; List.app run actions) end |
32381 | 107 |
|
108 |
fun in_range _ _ NONE = true |
|
109 |
| in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) |
|
110 |
||
111 |
fun only_within_range thy pos f x = |
|
112 |
let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line |
|
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
113 |
in if in_range l r (Position.line_of pos) then f x else () end |
32381 | 114 |
|
115 |
in |
|
116 |
||
32521 | 117 |
fun run_actions tr pre post = |
32381 | 118 |
let |
119 |
val thy = Proof.theory_of pre |
|
120 |
val pos = Toplevel.pos_of tr |
|
121 |
val name = Toplevel.name_of tr |
|
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
122 |
val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout)) |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
123 |
|
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
124 |
val str0 = string_of_int o the_default 0 |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
125 |
val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) |
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
126 |
val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" |
32381 | 127 |
in |
32676 | 128 |
only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) |
32381 | 129 |
end |
130 |
||
32521 | 131 |
fun done_actions st = |
132 |
let |
|
133 |
val thy = Toplevel.theory_of st |
|
134 |
val _ = log thy "\n\n"; |
|
135 |
in |
|
136 |
thy |
|
137 |
|> Actions.get |
|
138 |
|> List.app (fn (id, _, done) => done id {last=st, log=log thy}) |
|
139 |
end |
|
140 |
||
32381 | 141 |
end |
142 |
||
32504 | 143 |
val whitelist = ["apply", "by", "proof"] |
32468
3e6f5365971e
Mirabelle: explicit command blacklist, preliminary documentation
boehmes
parents:
32396
diff
changeset
|
144 |
|
32381 | 145 |
fun step_hook tr pre post = |
146 |
(* FIXME: might require wrapping into "interruptible" *) |
|
147 |
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso |
|
32504 | 148 |
member (op =) whitelist (Toplevel.name_of tr) |
32521 | 149 |
then run_actions tr (Toplevel.proof_of pre) (SOME post) |
150 |
else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post |
|
151 |
then done_actions pre |
|
32381 | 152 |
else () (* FIXME: add theory_hook here *) |
153 |
||
154 |
||
155 |
||
156 |
(* Mirabelle utility functions *) |
|
157 |
||
33292 | 158 |
val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *) |
32381 | 159 |
|
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
160 |
fun can_apply time tac st = |
32469 | 161 |
let |
33292 | 162 |
val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *) |
32469 | 163 |
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) |
32381 | 164 |
in |
32472
7b92a8b8daaf
Mirabelle: actions are responsible for their log messages, output is better readable
boehmes
parents:
32469
diff
changeset
|
165 |
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of |
32381 | 166 |
SOME (thm, _) => true |
167 |
| NONE => false) |
|
168 |
end |
|
169 |
||
170 |
local |
|
171 |
||
172 |
fun fold_body_thms f = |
|
173 |
let |
|
174 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => |
|
175 |
fn (x, seen) => |
|
176 |
if Inttab.defined seen i then (x, seen) |
|
177 |
else |
|
178 |
let |
|
179 |
val body' = Future.join body |
|
180 |
val (x', seen') = app (n + (if name = "" then 0 else 1)) body' |
|
181 |
(x, Inttab.update (i, ()) seen) |
|
182 |
in (x' |> n = 0 ? f (name, prop, body'), seen') end) |
|
183 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
|
184 |
||
185 |
in |
|
186 |
||
187 |
fun theorems_in_proof_term thm = |
|
188 |
let |
|
189 |
val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) |
|
190 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
|
191 |
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
192 |
fun resolve_thms names = map_filter (member_of names) all_thms |
|
193 |
in |
|
194 |
resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
195 |
end |
|
196 |
||
197 |
end |
|
198 |
||
199 |
fun theorems_of_sucessful_proof state = |
|
200 |
(case state of |
|
201 |
NONE => [] |
|
202 |
| SOME st => |
|
203 |
if not (Toplevel.is_proof st) then [] |
|
204 |
else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) |
|
205 |
||
206 |
fun get_setting settings (key, default) = |
|
207 |
the_default default (AList.lookup (op =) settings key) |
|
208 |
||
209 |
fun get_int_setting settings (key, default) = |
|
210 |
(case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
211 |
SOME (SOME i) => i |
|
212 |
| SOME NONE => error ("bad option: " ^ key) |
|
213 |
| NONE => default) |
|
214 |
||
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
215 |
fun cpu_time f x = |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
216 |
let |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
217 |
val start = start_timing () |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
218 |
val result = Exn.capture (fn () => f x) () |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
219 |
val time = Time.toMilliseconds (#cpu (end_timing start)) |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
220 |
in (Exn.release result, time) end |
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
221 |
|
32381 | 222 |
end |