oisdk · September 4, 2022 23:44
diff --git a/sieve.agda b/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
	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