-
Notifications
You must be signed in to change notification settings - Fork 89
/
Heartbeats.lean
33 lines (28 loc) · 1.2 KB
/
Heartbeats.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
/-
Copyright (c) 2023 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Std.Data.MLList.Basic
import Lean.Util.Heartbeats
/-!
# Truncate a `MLList` when running out of available heartbeats.
-/
open Lean
open Lean.Core (CoreM)
/-- Take an initial segment of a monadic lazy list,
stopping when there is less than `percent` of the remaining allowed heartbeats.
If `getMaxHeartbeats` returns `0`, then this passes through the original list unmodified.
The `initial` heartbeat counter is recorded when the first element of the list is requested.
Then each time an element is requested from the wrapped list the heartbeat counter is checked, and
if `current * 100 / initial < percent` then that element is returned,
but no further elements.
-/
def MLList.whileAtLeastHeartbeatsPercent [Monad m] [MonadLiftT CoreM m]
(L : MLList m α) (percent : Nat := 10) : MLList m α :=
MLList.squash fun _ => do
if (← getMaxHeartbeats) = 0 then do
return L
let initialHeartbeats ← getRemainingHeartbeats
return L.takeUpToFirstM fun _ => do
pure <| .up <| (← getRemainingHeartbeats) * 100 / initialHeartbeats < percent