50 lines
1.2 KiB
Agda
50 lines
1.2 KiB
Agda
module FizzBuzz where
|
||
|
||
open import Agda.Builtin.IO using (IO)
|
||
|
||
open import Agda.Builtin.Unit renaming (⊤ to Unit)
|
||
|
||
open import Data.Bool using (Bool ; false ; true ; if_then_else_)
|
||
|
||
open import Data.Nat using (ℕ ; zero ; suc ; _≡ᵇ_ ; _%_)
|
||
|
||
open import Data.Nat.Show using (show)
|
||
|
||
open import Data.List using (List ; [] ; _∷_ ; map)
|
||
|
||
open import Data.String using (String ; _++_ ; unlines)
|
||
|
||
postulate putStrLn : String -> IO Unit
|
||
{-# FOREIGN GHC import qualified Data.Text as T #-}
|
||
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
|
||
|
||
fizz : String
|
||
fizz = "Fizz"
|
||
|
||
buzz : String
|
||
buzz = "Buzz"
|
||
|
||
_isDivisibleBy_ : (n : ℕ) -> (m : ℕ) -> Bool
|
||
n isDivisibleBy zero = false
|
||
n isDivisibleBy (suc k) = ((n % (suc k)) ≡ᵇ 0)
|
||
|
||
getTerm : (n : ℕ) -> String
|
||
getTerm n =
|
||
if (n isDivisibleBy 15) then (fizz ++ buzz)
|
||
else if (n isDivisibleBy 3) then fizz
|
||
else if (n isDivisibleBy 5) then buzz
|
||
else (show n)
|
||
|
||
range : (a : ℕ) -> (b : ℕ) -> List (ℕ)
|
||
range k zero = []
|
||
range k (suc m) = k ∷ (range (suc k) m)
|
||
|
||
getTerms : (n : ℕ) -> List (String)
|
||
getTerms n = map getTerm (range 1 n)
|
||
|
||
fizzBuzz : String
|
||
fizzBuzz = unlines (getTerms 100)
|
||
|
||
main : IO Unit
|
||
main = putStrLn fizzBuzz
|