src/math/pow2.bend

bend-collections-laws-math@1.0.0.0 · 19 lines · 2 definitions

1import Base
2
3# 2^d by a TAIL recursion (an accumulator), so every def that calls it can
4# compile to a flat native loop. The structures' own `pow2` (the structural
5# `double(pow2(p))`, which the proofs unfold) is a non-tail recursion; the
6# native backend compiles a def that calls a non-tail recursion as a
7# segmented continuation instead of a flat loop, which made count, to_list,
8# the bitwise combinators and reserve several times slower than they need to
9# be. proofs/lib/pow2t.bend proves pow2t(d) == 2^d.
10
11def go(d: Nat, acc: Nat) -> Nat:
12  match d:
13    case 0n:
14      acc
15    case 1n+p:
16      go(p, Nat.double(acc))
17
18def pow2t(+d: Nat) -> Nat:
19  go(d, 1n)