def prime_go

bend-collections-laws-math@1.0.0.0 · src/math/number.bend:63

import Base

63# trial division: no d in [2, n) divides n iff none in [2, isqrt(n)] does.
64# `done` is n < d*d, `divides` is d | n, both for the current d.
65def prime_go(fuel: Nat, +n: Nat, +d: Nat, done: Bool, divides: Bool) -> Bool:
66  match fuel done divides:
67    case 0n _ _:
68      True{}
69    case 1n+f True{} _:
70      True{}
71    case 1n+f False{} True{}:
72      False{}
73    case 1n+ +f False{} False{}:
74      prime_go(f, n, 1n+d, Nat.is_lt(n, Nat.mul(1n+d, 1n+d)), Nat.is_eq(Nat.mod(n, 1n+d), 0n))