def cap_dbl

bend-ml-tensor-array@0.1.19.0 · main.bend:612

import Base

612# the same pair by doubling (0.1.10.0): p doubles until n <= p, log2(n) steps in a tail loop, where cap_pair takes n
613# steps of a recursion that is not a tail call, each with a comparison of up to n steps. Its fuel is n, which always
614# suffices (2^n >= n); if it ran out, the answer would be cap_pair's, so the law below needs no arithmetic about how
615# many doublings there are. ok is Nat.is_le(n, p), computed by the caller (match only inspects a parameter); with leb
616# it was n steps in all, 152 ms for n = 786,432 on one GPU lane (0.1.13.0).
617def cap_dbl(f: Nat, ok: Bool, +n: Nat, +d: Nat, +p: Nat) -> Nat & Nat:
618  match f ok:
619    case _ True{}:
620      (d, p)
621    case 0n False{}:
622      cap_pair(n)
623    case 1n+g False{}:
624      cap_dbl(g, Nat.is_le(n, Nat.add(p, p)), n, 1n+d, Nat.add(p, p))