def plan_go

mylsm-lsm-store@0.6.0.1 · src/BitTree.bend:31

import Base

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