1 (* Title: mirabelle.ML |
|
2 Author: Jasmin Blanchette and Sascha Boehme |
|
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 val setup : theory -> theory |
|
13 |
|
14 (* core *) |
|
15 type action |
|
16 val register : string * action -> theory -> theory |
|
17 val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state -> |
|
18 unit |
|
19 |
|
20 (* utility functions *) |
|
21 val goal_thm_of : Proof.state -> thm |
|
22 val can_apply : Time.time -> (Proof.context -> int -> tactic) -> |
|
23 Proof.state -> bool |
|
24 val theorems_in_proof_term : Thm.thm -> Thm.thm list |
|
25 val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list |
|
26 val get_setting : (string * string) list -> string * string -> string |
|
27 val get_int_setting : (string * string) list -> string * int -> int |
|
28 end |
|
29 |
|
30 |
|
31 |
|
32 structure Mirabelle : MIRABELLE_EXT = |
|
33 struct |
|
34 |
|
35 (* Mirabelle configuration *) |
|
36 |
|
37 val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" |
|
38 val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 |
|
39 val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 |
|
40 val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 |
|
41 |
|
42 val setup = setup1 #> setup2 #> setup3 #> setup4 |
|
43 |
|
44 |
|
45 |
|
46 (* Mirabelle core *) |
|
47 |
|
48 type action = {pre: Proof.state, post: Toplevel.state option, |
|
49 timeout: Time.time, log: string -> unit} -> unit |
|
50 |
|
51 structure Actions = TheoryDataFun |
|
52 ( |
|
53 type T = action Symtab.table |
|
54 val empty = Symtab.empty |
|
55 val copy = I |
|
56 val extend = I |
|
57 fun merge _ = Symtab.merge (K true) |
|
58 ) |
|
59 |
|
60 val register = Actions.map o Symtab.update_new |
|
61 |
|
62 local |
|
63 |
|
64 fun log thy s = |
|
65 let fun append_to n = if n = "" then K () else File.append (Path.explode n) |
|
66 in append_to (Config.get_thy thy logfile) (s ^ "\n") end |
|
67 (* FIXME: with multithreading and parallel proofs enabled, we might need to |
|
68 encapsulate this inside a critical section *) |
|
69 |
|
70 fun log_block thy msg = log thy (msg ^ "\n------------------") |
|
71 fun log_action thy name msg = log_block thy (name ^ ": " ^ msg) |
|
72 |
|
73 fun capture_exns logf f x = |
|
74 let |
|
75 fun f' x = f x |
|
76 handle TimeLimit.TimeOut => logf "time out" |
|
77 | ERROR msg => logf ("error: " ^ msg) |
|
78 in (case try f' x of NONE => logf "exception" | _ => ()) end |
|
79 |
|
80 fun apply_actions thy info (pre, post, time) actions = |
|
81 let |
|
82 val _ = log_block thy info |
|
83 fun apply (name, action) = |
|
84 let val st = {pre=pre, post=post, timeout=time, log=log_action thy name} |
|
85 in capture_exns (log_action thy name) action st end |
|
86 in List.app apply actions end |
|
87 |
|
88 fun in_range _ _ NONE = true |
|
89 | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) |
|
90 |
|
91 fun only_within_range thy pos f x = |
|
92 let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line |
|
93 in if in_range l r (Position.line_of pos) then f x else () end |
|
94 |
|
95 in |
|
96 |
|
97 fun basic_hook tr pre post = |
|
98 let |
|
99 val thy = Proof.theory_of pre |
|
100 val pos = Toplevel.pos_of tr |
|
101 val name = Toplevel.name_of tr |
|
102 val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout)) |
|
103 |
|
104 val str0 = string_of_int o the_default 0 |
|
105 val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) |
|
106 val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):" |
|
107 in |
|
108 Actions.get thy |
|
109 |> Symtab.dest |
|
110 |> only_within_range thy pos (apply_actions thy info st) |
|
111 end |
|
112 |
|
113 end |
|
114 |
|
115 val blacklist = ["disable_pr", "enable_pr", "done", ".", "using", "txt"] |
|
116 |
|
117 fun step_hook tr pre post = |
|
118 (* FIXME: might require wrapping into "interruptible" *) |
|
119 if can (Proof.assert_backward o Toplevel.proof_of) pre andalso |
|
120 not (member (op =) blacklist (Toplevel.name_of tr)) |
|
121 then basic_hook tr (Toplevel.proof_of pre) (SOME post) |
|
122 else () (* FIXME: add theory_hook here *) |
|
123 |
|
124 |
|
125 |
|
126 (* Mirabelle utility functions *) |
|
127 |
|
128 val goal_thm_of = snd o snd o Proof.get_goal |
|
129 |
|
130 fun can_apply time tac st = |
|
131 let |
|
132 val (ctxt, (facts, goal)) = Proof.get_goal st |
|
133 val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) |
|
134 in |
|
135 (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of |
|
136 SOME (thm, _) => true |
|
137 | NONE => false) |
|
138 end |
|
139 |
|
140 local |
|
141 |
|
142 fun fold_body_thms f = |
|
143 let |
|
144 fun app n (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => |
|
145 fn (x, seen) => |
|
146 if Inttab.defined seen i then (x, seen) |
|
147 else |
|
148 let |
|
149 val body' = Future.join body |
|
150 val (x', seen') = app (n + (if name = "" then 0 else 1)) body' |
|
151 (x, Inttab.update (i, ()) seen) |
|
152 in (x' |> n = 0 ? f (name, prop, body'), seen') end) |
|
153 in fn bodies => fn x => #1 (fold (app 0) bodies (x, Inttab.empty)) end |
|
154 |
|
155 in |
|
156 |
|
157 fun theorems_in_proof_term thm = |
|
158 let |
|
159 val all_thms = PureThy.all_thms_of (Thm.theory_of_thm thm) |
|
160 fun collect (s, _, _) = if s <> "" then insert (op =) s else I |
|
161 fun member_of xs (x, y) = if member (op =) xs x then SOME y else NONE |
|
162 fun resolve_thms names = map_filter (member_of names) all_thms |
|
163 in |
|
164 resolve_thms (fold_body_thms collect [Thm.proof_body_of thm] []) |
|
165 end |
|
166 |
|
167 end |
|
168 |
|
169 fun theorems_of_sucessful_proof state = |
|
170 (case state of |
|
171 NONE => [] |
|
172 | SOME st => |
|
173 if not (Toplevel.is_proof st) then [] |
|
174 else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st))) |
|
175 |
|
176 fun get_setting settings (key, default) = |
|
177 the_default default (AList.lookup (op =) settings key) |
|
178 |
|
179 fun get_int_setting settings (key, default) = |
|
180 (case Option.map Int.fromString (AList.lookup (op =) settings key) of |
|
181 SOME (SOME i) => i |
|
182 | SOME NONE => error ("bad option: " ^ key) |
|
183 | NONE => default) |
|
184 |
|
185 end |
|