sieve.agda

primes : ∀ n → List (Fin n)
primes zero = []
primes (suc zero) = []
primes (suc (suc zero)) = []
primes (suc (suc (suc m))) = sieve (tabulate (just ∘ Fin.suc))
  where
  cross-off : ∀ {n} → Fin _ → Vec (Maybe _) n → Vec (Maybe _) n

  sieve : ∀ {n} →  Vec (Maybe (Fin (2 + m))) n → List (Fin (3 + m))
  sieve [] = []
  sieve (nothing ∷ xs) =         sieve xs
  sieve (just x  ∷ xs) = suc x ∷ sieve (cross-off x xs)

  cross-off p fs = foldr B f (const []) fs p
    where
    B = λ n → ∀ {i} → Fin i → Vec (Maybe (Fin (2 + m))) n

    f : ∀ {n} → Maybe (Fin (2 + m)) → B n → B (suc n)
    f _ xs zero    = nothing ∷ xs p
    f x xs (suc y) = x       ∷ xs y