def depth_go

bend-ml-tensor-fork@0.1.6.0 · main.bend:113

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

113# the smallest d with 2^d >= n (TA.cap_depth's answer) by doubling a U32: log2(n) steps, where cap_depth compares Nats
114# (a share of every product's time at 512 x 1536)
115def depth_go(f: Nat, ok: Bool, +n: U32, +p: U32, d: Nat) -> Nat:
116  match f ok:
117    case _ True{}:
118      d
119    case 0n False{}:
120      d
121    case 1n+g False{}:
122      depth_go(g, U32.is_le(n, (p + p : U32)), n, (p + p : U32), 1n+d)