Fizz-Buzz in LiquidHaskell

FizzBuzz.hs

// Run at: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1427132944.hs

module FizzBuzz where

---------------------------------------------------------------
-- | Implementation: Top level
---------------------------------------------------------------

main      :: IO ()
main      = mapM_ (putStrLn . say) (take 100 $ nums 0)
  where
   nums n = n : nums (n+1)

{-@ say    :: Nat -> String @-}
say n
  | f && b = sayFizzBuzz n
  | f      = sayFizz n
  | b      = sayBuzz n
  where
    f      = isFizzy n
    b      = isBuzzy n

---------------------------------------------------------------
-- | Specification: Fizziness and Buzziness
---------------------------------------------------------------

{-@ predicate IsFizz N = N mod 3 == 0 @-}
{-@ predicate IsBuzz N = N mod 5 == 0 @-}

{-@ type Fizz          = {v:Int | IsFizz v}             @-}
{-@ type Buzz          = {v:Int | IsBuzz v}             @-}
{-@ type FizzBuzz      = {v:Int | IsFizz v && IsBuzz v} @-}

-- | Specification: Only say "fizz" (resp. "buzz") for Fizz (resp. Buzz) numbers

{-@ sayFizz :: Fizz -> String @-}
sayFizz = ("fizz: " ++) . show

{-@ sayBuzz :: Buzz -> String @-}
sayBuzz     = ("Buzz: " ++) . show

{-@ sayFizzBuzz :: FizzBuzz -> String @-}
sayFizzBuzz = ("FizzBuzz: " ++) . show

-- | A few "tests"

{-@ x27 :: Fizz @-}
x27 = 27

{-@ x10 :: Buzz @-}
x10 = 10

{-@ x15 :: FizzBuzz @-}
x15 = 15

tests = [ sayFizz x15      -- OK
        , sayFizz x10      -- BAD
        , sayBuzz x15      -- OK
        , sayBuzz x27      -- BAD
        , sayFizzBuzz x15  -- OK
        , sayFizzBuzz x10  -- BAD
        ]

---------------------------------------------------------------
-- | Implementation: *zziness via `mod`
---------------------------------------------------------------

{-@ isFizzy :: n:Nat -> {v:Bool | Prop v <=> IsFizz n} @-}
isFizzy n   = n `mod` 3 == 0

{-@ isBuzzy :: n:Nat -> {v:Bool | Prop v <=> IsBuzz n} @-}
isBuzzy n   = n `mod` 5 == 0

---------------------------------------------------------------
-- | Implelementation: *zziness via recursion
---------------------------------------------------------------

{-@ isFizzy   :: n:Nat -> {v:Bool | Prop v <=> IsFizz n} @-}
isFizzy' n
  | n == 0    = True
  | n == 1    = False
  | n == 2    = False
  | otherwise = isFizzy' (n - 3)

{-@ isBuzzy' :: n:Nat -> {v:Bool | Prop v <=> IsBuzz n} @-}
isBuzzy' n
  | n == 0    = True
  | n == 1    = False
  | n == 2    = False
  | n == 3    = False
  | n == 4    = False
  | otherwise = isBuzzy' (n - 5)


---------------------------------------------------------------
-- Misc definitions to appease GHC
---------------------------------------------------------------

{-@ LIQUID "--no-termination" @-}

x10, x15, x27     :: Int
isFizzy, isFizzy' :: Int -> Bool
isBuzzy, isBuzzy' :: Int -> Bool