def depth_go

bend-collections@1.0.0.0 · src/containers/bitset.bend:152

import Base

152# The smallest depth whose 2^depth words hold n bits, capped at max_depth.
153# `fuel` bounds the search structurally, `cap` is 2^d and `done` is the exit
154# test `n <= 32 * cap`, so a depth that comes out of the loop below the cap
155# always satisfies it (proofs/bitset/depth.bend).
156def depth_go(fuel: Nat, +n: Nat, d: Nat, +cap: Nat, done: Bool) -> Nat:
157  match fuel done:
158    case 0n _:
159      d
160    case 1n+f True{}:
161      d
162    case 1n+f False{}:
163      depth_go(f, n, 1n+d, Nat.double(cap), Nat.is_le(n, Nat.mul(Nat.double(cap), 32n)))