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, methss))) = |
25 fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) = |
26 map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss)) |
26 map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths) |
27 | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step" |
27 | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step" |
28 |
28 |
29 val slack = seconds 0.05 |
29 val slack = seconds 0.05 |
30 |
30 |
31 fun try0_step _ _ (step as Let _) = step |
31 fun try0_step _ _ (step as Let _) = step |
32 | try0_step preplay_timeout |
32 | try0_step preplay_timeout |
33 ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) |
33 ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data) |
34 (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) = |
34 (step as Prove (_, _, l, _, _, (_, meth :: _))) = |
35 let |
35 let |
36 val timeout = |
36 val timeout = |
37 (case Lazy.force (preplay_outcome l meth) of |
37 (case Lazy.force (preplay_outcome l meth) of |
38 Played time => Time.+ (time, slack) |
38 Played time => Time.+ (time, slack) |
39 | _ => preplay_timeout) |
39 | _ => preplay_timeout) |
43 result as Played _ => SOME (variant, result) |
43 result as Played _ => SOME (variant, result) |
44 | _ => NONE) |
44 | _ => NONE) |
45 in |
45 in |
46 (* FIXME: create variant after success *) |
46 (* FIXME: create variant after success *) |
47 (case Par_List.get_some try_variant (variants_of_step step) of |
47 (case Par_List.get_some try_variant (variants_of_step step) of |
48 SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) => |
48 SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) => |
49 (set_preplay_outcome l meth' result; step') |
49 (set_preplay_outcome l meth' result; step') |
50 | NONE => step) |
50 | NONE => step) |
51 end |
51 end |
52 |
52 |
53 val try0_isar_proof = map_isar_steps oo try0_step |
53 val try0_isar_proof = map_isar_steps oo try0_step |