import Data.Vect

%default total

-- 0 indexed sieve
Sieve : Nat -> Type
Sieve n = Vect n Bool

take : (n : Nat) -> Stream t -> Vect n t
take Z _ = Nil
take (S n) (x::xs) = x::take n xs

plusAndMinusCancel : (n : Nat) -> (S n `minus` (S Z)) = n
plusAndMinusCancel Z = Refl
plusAndMinusCancel (S n) = Refl

minusZeroRightNeutral : (n : Nat) -> n `minus` 0 = n
minusZeroRightNeutral Z = Refl
minusZeroRightNeutral (S n) = Refl

sieve0 : (n : Nat) -> {auto prf : 2 `LTE` n} -> Sieve n
sieve0 k =
	rewrite plusAndMinusCancel k in
		False :: False :: (take (k `minus` 2) $ repeat True)

mark_multiples : Nat -> Sieve n -> Sieve n
mark_multiples k s = go Z s where
	go : Nat -> Sieve n -> Sieve n
	go _ Nil = Nil
	go (S m) (x::xs) = x :: go m xs
	go Z (_::xs) = False :: go k xs