1 (* Title: HOL/Mirabelle/Tools/mirabelle.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme, TU Munich |
|
3 *) |
|
4 |
|
5 signature MIRABELLE = |
|
6 sig |
|
7 (*configuration*) |
|
8 val logfile : string Config.T |
|
9 val timeout : int Config.T |
|
10 val start_line : int Config.T |
|
11 val end_line : int Config.T |
|
12 |
|
13 (*core*) |
|
14 type init_action = int -> theory -> theory |
|
15 type done_args = {last: Toplevel.state, log: string -> unit} |
|
16 type done_action = int -> done_args -> unit |
|
17 type run_args = {pre: Proof.state, post: Toplevel.state option, |
|
18 timeout: Time.time, log: string -> unit, pos: Position.T, name: string} |
|
19 type run_action = int -> run_args -> unit |
|
20 type action = init_action * run_action * done_action |
|
21 val catch : (int -> string) -> run_action -> run_action |
|
22 val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) -> |
|
23 int -> run_args -> 'a |
|
24 val register : action -> theory -> theory |
|
25 val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
|
26 unit |
|
27 |
|
28 (*utility functions*) |
|
29 val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
|
30 Proof.state -> bool |
|
31 val theorems_in_proof_term : thm -> thm list |
|
32 val theorems_of_sucessful_proof : Toplevel.state option -> thm list |
|
33 val get_setting : (string * string) list -> string * string -> string |
|
34 val get_int_setting : (string * string) list -> string * int -> int |
|
35 val cpu_time : ('a -> 'b) -> 'a -> 'b * int |
|
36 end |
|
37 |
|
38 |
|
39 |
|
40 structure Mirabelle : MIRABELLE = |
|
41 struct |
|
42 |
|
43 (* Mirabelle configuration *) |
|
44 |
|
45 val logfile = Attrib.setup_config_string @{binding mirabelle_logfile} (K "") |
|
46 val timeout = Attrib.setup_config_int @{binding mirabelle_timeout} (K 30) |
|
47 val start_line = Attrib.setup_config_int @{binding mirabelle_start_line} (K 0) |
|
48 val end_line = Attrib.setup_config_int @{binding mirabelle_end_line} (K ~1) |
|
49 |
|
50 |
|
51 (* Mirabelle core *) |
|
52 |
|
53 type init_action = int -> theory -> theory |
|
54 type done_args = {last: Toplevel.state, log: string -> unit} |
|
55 type done_action = int -> done_args -> unit |
|
56 type run_args = {pre: Proof.state, post: Toplevel.state option, |
|
57 timeout: Time.time, log: string -> unit, pos: Position.T, name: string} |
|
58 type run_action = int -> run_args -> unit |
|
59 type action = init_action * run_action * done_action |
|
60 |
|
61 structure Actions = Theory_Data |
|
62 ( |
|
63 type T = (int * run_action * done_action) list |
|
64 val empty = [] |
|
65 val extend = I |
|
66 fun merge data = Library.merge (K true) data (* FIXME potential data loss because of (K true) *) |
|
67 ) |
|
68 |
|
69 |
|
70 fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e) |
|
71 |
|
72 fun catch tag f id (st as {log, ...}: run_args) = (f id st; ()) |
|
73 handle exn => |
|
74 if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ()) |
|
75 |
|
76 fun catch_result tag d f id (st as {log, ...}: run_args) = f id st |
|
77 handle exn => |
|
78 if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d) |
|
79 |
|
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 |
|
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) |
|
92 in append_to (Config.get_global thy logfile) (s ^ "\n") end |
|
93 (* FIXME: with multithreading and parallel proofs enabled, we might need to |
|
94 encapsulate this inside a critical section *) |
|
95 |
|
96 fun log_sep thy = log thy "------------------" |
|
97 |
|
98 fun apply_actions thy pos name info (pre, post, time) actions = |
|
99 let |
|
100 fun apply f = f {pre=pre, post=post, timeout=time, log=log thy, pos=pos, name=name} |
|
101 fun run (id, run, _) = (apply (run id); log_sep thy) |
|
102 in (log thy info; log_sep thy; List.app run actions) end |
|
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 = |
|
108 let val l = Config.get_global thy start_line and r = Config.get_global thy end_line |
|
109 in if in_range l r (Position.line_of pos) then f x else () end |
|
110 |
|
111 in |
|
112 |
|
113 fun run_actions tr pre post = |
|
114 let |
|
115 val thy = Proof.theory_of pre |
|
116 val pos = Toplevel.pos_of tr |
|
117 val name = Toplevel.name_of tr |
|
118 val st = (pre, post, Time.fromSeconds (Config.get_global thy timeout)) |
|
119 |
|
120 val str0 = string_of_int o the_default 0 |
|
121 val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.offset_of pos) |
|
122 val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" |
|
123 in |
|
124 only_within_range thy pos (apply_actions thy pos name info st) (Actions.get thy) |
|
125 end |
|
126 |
|
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 |
|
137 end |
|
138 |
|
139 val whitelist = ["apply", "by", "proof"] |
|
140 |
|
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 |
|
144 member (op =) whitelist (Toplevel.name_of tr) |
|
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 |
|
148 else () (* FIXME: add theory_hook here *) |
|
149 |
|
150 |
|
151 |
|
152 (* Mirabelle utility functions *) |
|
153 |
|
154 fun can_apply time tac st = |
|
155 let |
|
156 val {context = ctxt, facts, goal} = Proof.goal st |
|
157 val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) |
|
158 in |
|
159 (case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of |
|
160 SOME (SOME _) => true |
|
161 | _ => false) |
|
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 |
|
183 val all_thms = Global_Theory.all_thms_of (Thm.theory_of_thm thm) |
|
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 [] |
|
198 else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st)))) |
|
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 |
|
209 fun cpu_time f x = |
|
210 let val ({cpu, ...}, y) = Timing.timing f x |
|
211 in (y, Time.toMilliseconds cpu) end |
|
212 |
|
213 end |
|