def depth_go

import bendtorch@1.3.0.0/main.bend as Bendtorch

import Base
import bend-ml-tensor-array@0.1.18.0/main.bend as TA

211# the smallest d with 2^d >= n (TA.cap_depth's answer), by doubling a U32: log2(n) cheap steps, where cap_depth
212# compares Nats one unit at a time at each doubling; f is fuel (32 doublings cover every U32)
213def depth_go(f: Nat, ok: Bool, +n: U32, +p: U32, d: Nat) -> Nat:
214  match f ok:
215    case _ True{}:
216      d
217    case 0n False{}:
218      d
219    case 1n+g False{}:
220      depth_go(g, U32.is_le(n, (p + p : U32)), n, (p + p : U32), 1n+d)

Uses (5)

U32
Bool
Nat
U32.add
U32.is_le

Used by (1)

bendtorch@1.3.0.0/main:depth