26 fun run_tac timeout_opt tac st = |
26 fun run_tac timeout_opt tac st = |
27 let val with_timeout = |
27 let val with_timeout = |
28 (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) |
28 (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I) |
29 in with_timeout (Seq.pull o tac) st |> Option.map fst end |
29 in with_timeout (Seq.pull o tac) st |> Option.map fst end |
30 |
30 |
31 fun apply_recursive recurse elapsed0 timeout_opt post apply st = |
31 val num_goals = Thm.nprems_of o #goal o Proof.goal |
|
32 fun apply_recursive recurse elapsed0 timeout_opt apply st = |
32 (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of |
33 (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of |
33 ({elapsed, ...}, SOME st') => |
34 ({elapsed, ...}, SOME st') => |
34 if recurse andalso (st' |> Thm.nprems_of o #goal o Proof.goal) > 0 then |
35 if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then |
35 let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) |
36 let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt) |
36 in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 post apply st' end |
37 in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end |
37 else (elapsed0 + elapsed, st') |
38 else (elapsed0 + elapsed, st') |
38 |_ => (elapsed0, st)) |
39 |_ => (elapsed0, st)) |
39 |
40 |
40 fun parse_method ctxt s = |
41 fun parse_method ctxt s = |
41 enclose "(" ")" s |
42 enclose "(" ")" s |
84 |> Method.Basic |
85 |> Method.Basic |
85 |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) |
86 |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m])) |
86 |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m])) |
87 |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Then, [using_text, m])) |
87 |
88 |
88 val apply = text |> Proof.refine #> Seq.filter_results |
89 val apply = text |> Proof.refine #> Seq.filter_results |
89 val the_goal = #goal o Proof.goal |
90 val num_before = num_goals st |
90 val num_before = Thm.nprems_of (the_goal st) |
|
91 val multiple_goals = all_goals andalso num_before > 1 |
91 val multiple_goals = all_goals andalso num_before > 1 |
92 val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt the_goal apply st |
92 val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st |
93 val num_after = Thm.nprems_of (the_goal st') |
93 val num_after = num_goals st' |
94 val select = "[" ^ string_of_int (num_before - num_after) ^ "]" |
94 val select = "[" ^ string_of_int (num_before - num_after) ^ "]" |
95 val unused = implode_space (unused |> map string_of_xthm) |
95 val unused = implode_space (unused |> map string_of_xthm) |
96 val command = |
96 val command = |
97 (if unused <> "" then "using " ^ unused ^ " " else "") ^ |
97 (if unused <> "" then "using " ^ unused ^ " " else "") ^ |
98 (if num_after = 0 then "by " else "apply ") ^ |
98 (if num_after = 0 then "by " else "apply ") ^ |