20 open Sledgehammer_Util |
20 open Sledgehammer_Util |
21 open Sledgehammer_Reconstructor |
21 open Sledgehammer_Reconstructor |
22 open Sledgehammer_Isar_Proof |
22 open Sledgehammer_Isar_Proof |
23 open Sledgehammer_Isar_Preplay |
23 open Sledgehammer_Isar_Preplay |
24 |
24 |
25 fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) = |
25 fun step_with_method meth (Prove (qs, xs, l, t, subproofs, (facts, _))) = |
26 map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths) |
26 Prove (qs, xs, l, t, subproofs, (facts, [meth])) |
27 | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step" |
|
28 |
27 |
29 val slack = seconds 0.05 |
28 val slack = seconds 0.05 |
30 |
29 |
31 fun try0_step _ _ (step as Let _) = step |
30 fun try0_step _ _ (step as Let _) = step |
32 | try0_step preplay_timeout |
31 | try0_step preplay_timeout |
33 ({preplay_outcome, set_preplay_outcomes, preplay_quietly, ...} : isar_preplay_data) |
32 ({preplay_step, set_preplay_outcomes, preplay_outcome, ...} : isar_preplay_data) |
34 (step as Prove (_, _, l, _, _, (_, meth :: _))) = |
33 (step as Prove (_, _, l, _, _, (_, meths as meth :: _))) = |
35 let |
34 let |
36 val timeout = |
35 val timeout = |
37 (case Lazy.force (preplay_outcome l meth) of |
36 (case Lazy.force (preplay_outcome l meth) of |
38 Played time => Time.+ (time, slack) |
37 Played time => Time.+ (time, slack) |
39 | _ => preplay_timeout) |
38 | _ => preplay_timeout) |
40 |
39 |
41 fun try_variant variant = |
40 fun try_method meth = |
42 (case preplay_quietly timeout variant of |
41 (case preplay_step timeout meth step of |
43 result as Played _ => SOME (variant, result) |
42 outcome as Played _ => SOME (meth, outcome) |
44 | _ => NONE) |
43 | _ => NONE) |
45 in |
44 in |
46 (* FIXME: create variant after success *) |
45 (* FIXME: create variant after success *) |
47 (case Par_List.get_some try_variant (variants_of_step step) of |
46 (case Par_List.get_some try_method meths of |
48 SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), outcome) => |
47 SOME (meth', outcome) => |
49 (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step') |
48 (set_preplay_outcomes l [(meth', Lazy.value outcome)]; step_with_method meth' step) |
50 | NONE => step) |
49 | NONE => step) |
51 end |
50 end |
52 |
51 |
53 val try0_isar_proof = map_isar_steps oo try0_step |
52 val try0_isar_proof = map_isar_steps oo try0_step |
54 |
53 |