author | sultana |
Tue, 24 Apr 2012 13:59:29 +0100 | |
changeset 47730 | 15f4309bb9eb |
parent 47477 | src/HOL/Mirabelle/Actions/mirabelle.ML@3fabf352243e |
child 47847 | 7cddb6c8f93c |
permissions | -rw-r--r-- |
47477
3fabf352243e
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
sultana
parents:
43710
diff
changeset
|
1 |
(* Title: HOL/Mirabelle/Actions/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 |
|
33243 | 31 |
val theorems_in_proof_term : thm -> thm list |
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 |
||
42616
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42014
diff
changeset
|
45 |
val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "") |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42014
diff
changeset
|
46 |
val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30) |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42014
diff
changeset
|
47 |
val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0) |
92715b528e78
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
wenzelm
parents:
42014
diff
changeset
|
48 |
val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (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 => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
36787
diff
changeset
|
74 |
if Exn.is_interrupt exn then 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 => |
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
36787
diff
changeset
|
78 |
if Exn.is_interrupt exn then 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 |
32469 | 157 |
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) |
32381 | 158 |
in |
39451
8893562a954b
prevent exception when calling "Mirabelle.can_apply" on empty proof sequence;
blanchet
parents:
39377
diff
changeset
|
159 |
(case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of |
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 |
|
168 |
fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => |
|
169 |
fn (x, seen) => |
|
170 |
if Inttab.defined seen i then (x, seen) |
|
171 |
else |
|
172 |
let |
|
173 |
val body' = Future.join body |
|
174 |
val (x', seen') = app (n + (if name = "" then 0 else 1)) body' |
|
175 |
(x, Inttab.update (i, ()) seen) |
|
176 |
in (x' |> n = 0 ? f (name, prop, body'), seen') end) |
|
177 |
in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
|
178 |
||
179 |
in |
|
180 |
||
181 |
fun theorems_in_proof_term thm = |
|
182 |
let |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39451
diff
changeset
|
183 |
val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) |
32381 | 184 |
fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
185 |
fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
186 |
fun resolve_thms names = map_filter (member_of names) all_thms |
|
187 |
in |
|
188 |
resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
189 |
end |
|
190 |
||
191 |
end |
|
192 |
||
193 |
fun theorems_of_sucessful_proof state = |
|
194 |
(case state of |
|
195 |
NONE => [] |
|
196 |
| SOME st => |
|
197 |
if not (Toplevel.is_proof st) then [] |
|
35592
768d17f54125
use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
wenzelm
parents:
34052
diff
changeset
|
198 |
else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st)))) |
32381 | 199 |
|
200 |
fun get_setting settings (key, default) = |
|
201 |
the_default default (AList.lookup (op =) settings key) |
|
202 |
||
203 |
fun get_int_setting settings (key, default) = |
|
204 |
(case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
205 |
SOME (SOME i) => i |
|
206 |
| SOME NONE => error ("bad option: " ^ key) |
|
207 |
| NONE => default) |
|
208 |
||
42014
75417ef605ba
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
wenzelm
parents:
42012
diff
changeset
|
209 |
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
|
210 |
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
|
211 |
in (y, Time.toMilliseconds cpu) end |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32497
diff
changeset
|
212 |
|
32381 | 213 |
end |