recurrence.bend

bend-kit-scheduler@0.3.0.0 · 61 lines · 0 definitions

1# Pure recurrence on arbitrary-precision Nat ticks: no wrapping or U32 conversion.
2import Base
3
4type Missed is Data:
5  Skip{}
6  CatchUp{bound: Nat}
7
8type Cadence is Data:
9  FixedDelay{}
10  FixedRate{policy: Missed}
11
12type Plan is Data:
13  Planned{replay: List<&2, Nat>, next: Nat}
14
15def replay(p: Plan) -> List<&2, Nat>:
16  match p:
17    case Planned{ticks, next}:
18      ticks
19
20def next(p: Plan) -> Nat:
21  match p:
22    case Planned{ticks, next}:
23      next
24
25# Generate only the bounded replay prefix, never the skipped remainder.
26def ticks(count: Nat, +previous: Nat, +period: Nat) -> List<&2, Nat>:
27  match count:
28    case 0n:
29      Nil{}
30    case 1n+n:
31      +deadline = Nat.add(previous, period)
32      Con{deadline, ticks(n, deadline, period)}
33
34def limit(policy: Missed, overdue: Nat) -> Nat:
35  match policy:
36    case Skip{}:
37      0n
38    case CatchUp{bound}:
39      Nat.min(bound, overdue)
40
41# A tick equal to completion is overdue. The already-completed previous tick
42# is excluded. A positive period keeps all arithmetic exact, without overflow.
43def rate(+previous: Nat, +completion: Nat, +period: Nat, policy: Missed) -> Plan:
44  +overdue = Nat.div(Nat.sub(completion, previous), period)
45  Planned{ticks(limit(policy, overdue), previous, period),
46    Nat.add(previous, Nat.mul(1n+overdue, period))}
47
48def positive(cadence: Cadence, +previous: Nat, +completion: Nat, +period: Nat) -> Plan:
49  match cadence:
50    case FixedDelay{}:
51      Planned{Nil{}, Nat.add(completion, period)}
52    case FixedRate{policy}:
53      rate(previous, completion, period, policy)
54
55# None is an explicit invalid-zero-period result, not a zero cadence.
56def plan(previous: Nat, completion: Nat, period: Nat, cadence: Cadence) -> Maybe<&2, Plan>:
57  match period:
58    case 0n:
59      None{}
60    case 1n+p:
61      Some{positive(cadence, previous, completion, 1n+p)}