fizzbuzz.idr

data FizzDataType : Type where
  FizzData : FizzDataType

data BuzzDataType : Type where
  BuzzData : BuzzDataType

data FizzBuzzDataType : Type where
  FizzBuzzData : FizzBuzzDataType

data NatDataType : (n : Nat) -> Type where
  NatData : (n : Nat) -> NatDataType n

implementation Show FizzDataType where
  show FizzData = "Fizz"

implementation Show BuzzDataType where
  show BuzzData = "Buzz"

implementation Show FizzBuzzDataType where
  show FizzBuzzDataType = "FizzBuzz"

implementation Show (NatDataType n) where
  show (NatData n) = show n

total FizzBuzzImpl : Nat -> Nat -> Nat -> Type
FizzBuzzImpl n (S (S (S a))) b                     = FizzBuzzImpl n a b
FizzBuzzImpl n a             (S (S (S (S (S b))))) = FizzBuzzImpl n a b
FizzBuzzImpl n Z             Z                     = FizzBuzzDataType
FizzBuzzImpl n Z             _                     = FizzDataType
FizzBuzzImpl n _             Z                     = BuzzDataType
FizzBuzzImpl n _             _                     = NatDataType n

total FizzBuzz : Nat -> Type
FizzBuzz n = FizzBuzzImpl n n n

total fizzbuzz : (n : Nat) -> FizzBuzz n
fizzbuzz n = fizzbuzzimpl n n where
  fizzbuzzimpl : (a : Nat) -> (b : Nat) -> FizzBuzzImpl n a b
  fizzbuzzimpl (S (S (S a))) b                     = fizzbuzzimpl a b
  fizzbuzzimpl Z             (S (S (S (S (S b))))) = fizzbuzzimpl Z b
  fizzbuzzimpl (S Z)         (S (S (S (S (S b))))) = fizzbuzzimpl (S Z) b
  fizzbuzzimpl (S (S Z))     (S (S (S (S (S b))))) = fizzbuzzimpl (S (S Z)) b
  fizzbuzzimpl Z             Z                     = FizzBuzzData
  fizzbuzzimpl Z             (S Z)                 = FizzData
  fizzbuzzimpl Z             (S (S Z))             = FizzData
  fizzbuzzimpl Z             (S (S (S Z)))         = FizzData
  fizzbuzzimpl Z             (S (S (S (S Z))))     = FizzData
  fizzbuzzimpl (S Z)         Z                     = BuzzData
  fizzbuzzimpl (S (S Z))     Z                     = BuzzData
  fizzbuzzimpl (S Z)         (S Z)                 = NatData n
  fizzbuzzimpl (S Z)         (S (S Z))             = NatData n
  fizzbuzzimpl (S Z)         (S (S (S Z)))         = NatData n
  fizzbuzzimpl (S Z)         (S (S (S (S Z))))     = NatData n
  fizzbuzzimpl (S (S Z))     (S Z)                 = NatData n
  fizzbuzzimpl (S (S Z))     (S (S Z))             = NatData n
  fizzbuzzimpl (S (S Z))     (S (S (S Z)))         = NatData n
  fizzbuzzimpl (S (S Z))     (S (S (S (S Z))))     = NatData n