1	# Pure recurrence on arbitrary-precision Nat ticks: no wrapping or U32 conversion.
2	import Base
3	
4	type Missed is Data:
5	  Skip{}
6	  CatchUp{bound: Nat}
7	
8	type Cadence is Data:
9	  FixedDelay{}
10	  FixedRate{policy: Missed}
11	
12	type Plan is Data:
13	  Planned{replay: List<&2, Nat>, next: Nat}
14	
15	def replay(p: Plan) -> List<&2, Nat>:
16	  match p:
17	    case Planned{ticks, next}:
18	      ticks
19	
20	def 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.
26	def 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	
34	def 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.
43	def 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	
48	def 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.
56	def 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)}