79 | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") |
79 | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps") |
80 end |
80 end |
81 |
81 |
82 fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1))) |
82 fun try_merge (Prove (_, [], l1, _, [], ((lfs1, gfs1), meths1))) |
83 (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) = |
83 (Prove (qs2, fix, l2, t, subproofs, ((lfs2, gfs2), meths2))) = |
84 let |
84 (case inter (op =) meths1 meths2 of |
85 val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) |
85 [] => NONE |
86 val gfs = union (op =) gfs1 gfs2 |
86 | meths => |
87 val meths = fold_rev (insert (op =)) meths1 meths2 |
87 let |
88 in |
88 val lfs = union (op =) lfs1 (remove (op =) l1 lfs2) |
89 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
89 val gfs = union (op =) gfs1 gfs2 |
90 end |
90 in |
|
91 SOME (Prove (qs2, fix, l2, t, subproofs, ((lfs, gfs), meths))) |
|
92 end) |
91 | try_merge _ _ = NONE |
93 | try_merge _ _ = NONE |
92 |
94 |
93 val compress_degree = 2 |
95 val compress_degree = 2 |
94 val merge_timeout_slack = 1.2 |
96 val merge_timeout_slack = 1.2 |
95 |
97 |
235 |
237 |
236 (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) |
238 (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *) |
237 val play_outcomes = map2 preplay_quietly timeouts succs' |
239 val play_outcomes = map2 preplay_quietly timeouts succs' |
238 |
240 |
239 (* ensure none of the modified successors timed out *) |
241 (* ensure none of the modified successors timed out *) |
240 val true = List.all (fn Played _ => true) play_outcomes |
242 val true = forall (fn Played _ => true) play_outcomes |
241 |
243 |
242 val (steps1, _ :: steps2) = chop i steps |
244 val (steps1, _ :: steps2) = chop i steps |
243 (* replace successors with their modified versions *) |
245 (* replace successors with their modified versions *) |
244 val steps2 = update_steps steps2 succs' |
246 val steps2 = update_steps steps2 succs' |
245 in |
247 in |