27 structure Label_Table = Table( |
27 structure Label_Table = Table( |
28 type key = label |
28 type key = label |
29 val ord = label_ord) |
29 val ord = label_ord) |
30 |
30 |
31 (* Timing *) |
31 (* Timing *) |
32 type ext_time = bool * Time.time |
32 fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2)) |
33 fun ext_time_add (b1, t1) (b2, t2) : ext_time = (b1 orelse b2, t1+t2) |
|
34 val no_time = (false, seconds 0.0) |
33 val no_time = (false, seconds 0.0) |
35 fun take_time timeout tac arg = |
34 fun take_time timeout tac arg = |
36 let val timing = Timing.start () in |
35 let val timing = Timing.start () in |
37 (TimeLimit.timeLimit timeout tac arg; |
36 (TimeLimit.timeLimit timeout tac arg; |
38 Timing.result timing |> #cpu |> SOME) |
37 Timing.result timing |> #cpu |> SOME) |
39 handle _ => NONE |
38 handle _ => NONE |
40 end |
39 end |
41 fun sum_up_time timeout lazy_time_vector = |
40 fun sum_up_time timeout lazy_time_vector = |
42 Vector.foldl |
41 Vector.foldl |
43 ((fn (SOME t, (b, ts)) => (b, t+ts) |
42 ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) |
44 | (NONE, (_, ts)) => (true, ts+timeout)) o apfst Lazy.force) |
43 | (NONE, (_, ts)) => (true, Time.+(ts, timeout))) o apfst Lazy.force) |
45 no_time lazy_time_vector |
44 no_time lazy_time_vector |
46 |
45 |
47 (* clean vector interface *) |
46 (* clean vector interface *) |
48 fun get i v = Vector.sub (v, i) |
47 fun get i v = Vector.sub (v, i) |
49 fun replace x i v = Vector.update (v, i, x) |
48 fun replace x i v = Vector.update (v, i, x) |
140 (case get j metis_time |> Lazy.force of |
139 (case get j metis_time |> Lazy.force of |
141 NONE => (NONE, metis_time) |
140 NONE => (NONE, metis_time) |
142 | SOME t2 => |
141 | SOME t2 => |
143 let |
142 let |
144 val s12 = merge s1 s2 |
143 val s12 = merge s1 s2 |
145 val timeout = time_mult merge_timeout_slack (t1 + t2) |
144 val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) |
146 in |
145 in |
147 case try_metis timeout s12 () of |
146 case try_metis timeout s12 () of |
148 NONE => (NONE, metis_time) |
147 NONE => (NONE, metis_time) |
149 | some_t12 => |
148 | some_t12 => |
150 (SOME s12, metis_time |
149 (SOME s12, metis_time |