35 sig |
35 sig |
36 include BASIC_PROOFTERM |
36 include BASIC_PROOFTERM |
37 |
37 |
38 type oracle = string * term |
38 type oracle = string * term |
39 type pthm = serial * (string * term * proof_body future) |
39 type pthm = serial * (string * term * proof_body future) |
|
40 val join_body: proof_body -> unit |
40 val proof_of: proof_body -> proof |
41 val proof_of: proof_body -> proof |
41 val join_proof: proof_body future -> proof |
42 val join_proof: proof_body future -> proof |
42 val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a |
43 val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a |
43 val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a |
44 val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a |
44 val join_bodies: proof_body list -> unit |
|
45 val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} |
45 val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool} |
46 |
46 |
47 val oracle_ord: oracle * oracle -> order |
47 val oracle_ord: oracle * oracle -> order |
48 val thm_ord: pthm * pthm -> order |
48 val thm_ord: pthm * pthm -> order |
49 val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T |
49 val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T |
169 proof: proof}; |
169 proof: proof}; |
170 |
170 |
171 type oracle = string * term; |
171 type oracle = string * term; |
172 type pthm = serial * (string * term * proof_body future); |
172 type pthm = serial * (string * term * proof_body future); |
173 |
173 |
|
174 fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm))); |
|
175 fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms); |
|
176 fun join_body (PBody {thms, ...}) = join_thms thms; |
|
177 |
174 fun proof_of (PBody {proof, ...}) = proof; |
178 fun proof_of (PBody {proof, ...}) = proof; |
175 val join_proof = Future.join #> proof_of; |
179 val join_proof = Future.join #> proof_of; |
176 |
180 |
177 |
181 |
178 (***** proof atoms *****) |
182 (***** proof atoms *****) |
193 in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; |
197 in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; |
194 |
198 |
195 fun fold_body_thms f = |
199 fun fold_body_thms f = |
196 let |
200 let |
197 fun app (PBody {thms, ...}) = |
201 fun app (PBody {thms, ...}) = |
198 (Future.join_results (map (#3 o #2) thms); |
202 tap join_thms thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) => |
199 thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) => |
|
200 if Inttab.defined seen i then (x, seen) |
203 if Inttab.defined seen i then (x, seen) |
201 else |
204 else |
202 let |
205 let |
203 val body' = Future.join body; |
206 val body' = Future.join body; |
204 val (x', seen') = app body' (x, Inttab.update (i, ()) seen); |
207 val (x', seen') = app body' (x, Inttab.update (i, ()) seen); |
205 in (f (name, prop, body') x', seen') end)); |
208 in (f (name, prop, body') x', seen') end); |
206 in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; |
209 in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; |
207 |
|
208 fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies (); |
|
209 |
210 |
210 fun status_of bodies = |
211 fun status_of bodies = |
211 let |
212 let |
212 fun status (PBody {oracles, thms, ...}) x = |
213 fun status (PBody {oracles, thms, ...}) x = |
213 let |
214 let |
240 val merge_thms = Ord_List.union thm_ord; |
241 val merge_thms = Ord_List.union thm_ord; |
241 |
242 |
242 val all_oracles_of = |
243 val all_oracles_of = |
243 let |
244 let |
244 fun collect (PBody {oracles, thms, ...}) = |
245 fun collect (PBody {oracles, thms, ...}) = |
245 (Future.join_results (map (#3 o #2) thms); |
246 tap join_thms thms |> fold (fn (i, (_, _, body)) => fn (x, seen) => |
246 thms |> fold (fn (i, (_, _, body)) => fn (x, seen) => |
|
247 if Inttab.defined seen i then (x, seen) |
247 if Inttab.defined seen i then (x, seen) |
248 else |
248 else |
249 let |
249 let |
250 val body' = Future.join body; |
250 val body' = Future.join body; |
251 val (x', seen') = collect body' (x, Inttab.update (i, ()) seen); |
251 val (x', seen') = collect body' (x, Inttab.update (i, ()) seen); |
252 in (merge_oracles oracles x', seen') end)); |
252 in (merge_oracles oracles x', seen') end); |
253 in fn body => #1 (collect body ([], Inttab.empty)) end; |
253 in fn body => #1 (collect body ([], Inttab.empty)) end; |
254 |
254 |
255 fun approximate_proof_body prf = |
255 fun approximate_proof_body prf = |
256 let |
256 let |
257 val (oracles, thms) = fold_proof_atoms false |
257 val (oracles, thms) = fold_proof_atoms false |
1394 NONE => NONE |
1394 NONE => NONE |
1395 | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel)) |
1395 | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel)) |
1396 | fill _ = NONE; |
1396 | fill _ = NONE; |
1397 val (rules, procs) = get_data thy; |
1397 val (rules, procs) = get_data thy; |
1398 val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0; |
1398 val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0; |
|
1399 val _ = join_thms thms; |
1399 in PBody {oracles = oracles, thms = thms, proof = proof} end; |
1400 in PBody {oracles = oracles, thms = thms, proof = proof} end; |
1400 |
1401 |
1401 fun fulfill_proof_future _ [] postproc body = |
1402 fun fulfill_proof_future _ [] postproc body = |
1402 if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body)) |
1403 if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body)) |
1403 else Future.map postproc body |
1404 else Future.map postproc body |