module Main
import Data.Vect

isOdd : (x : Int) -> Bool
isOdd x = case mod x 2 of
            0 => False
            1 => True

popcnt : Int -> Int
popcnt 0 = 0
popcnt x = case isOdd x of
  False => popcnt (shiftR x 1)
  True => 1 + popcnt (shiftR x 1)

isOdious : Int -> Bool
isOdious k = isOdd (popcnt k)

isEvil : Int -> Bool
isEvil k = not (isOdious k)

filterUnfoldN : (n : Nat) ->
                (pred : Int -> Bool) -> (f : Int -> a) ->
                (next : Int -> Int) -> (seed : Int) ->
                Vect n a
filterUnfoldN Z pred f next seed = []
filterUnfoldN (S k) pred f next seed =
  if pred seed
  then (f seed) :: filterUnfoldN k pred f next (next seed)
  else filterUnfoldN (S k) pred f next (next seed)

printCompact : (Show a) => Vect n a -> IO ()
printCompact v = putStrLn (unwords (map show (toList v)))

main : IO ()
main = do putStr "popcnt(3**i): "
          printCompact (filterUnfoldN 30 (\_ => True) popcnt (3 *) 1)
          putStr "Evil:         "
          printCompact (filterUnfoldN 30 isEvil id (1 +) 0)
          putStr "Odious:       "
          printCompact (filterUnfoldN 30 isOdious id (1 +) 0)