def plan_go

mylsm-lsm-store@0.3.2.0 · src/BitTree.bend:28

import Base

28# Find the least power of two >= need. `fuel = need` is a conservative
29# termination bound; each non-final step doubles capacity.
30def plan_go(fuel: Nat, +need: Nat, +capacity: Nat, +height: Nat, done: Bool) -> Plan:
31  match fuel:
32    case 0n:
33      Plan{capacity, height}
34    case 1n+f:
35      match done:
36        case True{}:
37          Plan{capacity, height}
38        case False{}:
39          +next = Nat.double(capacity)
40          plan_go(f, need, next, Nat.add(height, 1n), Nat.is_le(need, next))