david-christiansen · August 29, 2015 14:04 · Jul 20, 2014 · Jul 20, 2014 · Jul 20, 2014
diff --git a/FizzBuzz.idr b/FizzBuzz.idr
@@ -4,7 +4,7 @@ module FizzBuzz
 
 -- A specification of the problem.  Each constructor tells the conditions
 -- under which it can be applied, and the "auto" keyword means that proof
--- search will be used in the constext where they are applied to fill them
+-- search will be used in the context where they are applied to fill them
 -- out. For instance, applying `N` to some Nat fails unless there's a proof in
 -- scope that the argument meets the criteria.
 data FB : Nat -> Type where

diff --git a/FizzBuzz.idr b/FizzBuzz.idr
@@ -1,33 +1,51 @@
 module FizzBuzz
 
+-- Dependently-typed FizzBuzz, about 5 years late to the party.
+
+-- A specification of the problem.  Each constructor tells the conditions
+-- under which it can be applied, and the "auto" keyword means that proof
+-- search will be used in the constext where they are applied to fill them
+-- out. For instance, applying `N` to some Nat fails unless there's a proof in
+-- scope that the argument meets the criteria.
 data FB : Nat -> Type where
   N        : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
-  Fizz     : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto not4 : Not (n `mod` 5 = 0)} -> FB n
+  Fizz     : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
   Buzz     : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto div5 : n `mod` 5 = 0}       -> FB n
   FizzBuzz : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto div5 : n `mod` 5 = 0}       -> FB n
 
+-- A function to calculate what to output for a given number. decEq leaves
+-- proofs in scope (the arguments to `Yes` and `No`) that will be found by
+-- proof search when applying the constructors.
 fb : (n : Nat) -> FB n
 fb n with (decEq (n `mod` 3) 0)
-  fb n | (Yes prf) with (decEq (n `mod` 5) 0)
-    fb n | (Yes prf) | (Yes x) = FizzBuzz n
-    fb n | (Yes prf) | (No contra) = Fizz n
+  fb n | (Yes prf)   with (decEq (n `mod` 5) 0)
+    fb n | (Yes prf)   | (Yes x)     = FizzBuzz n
+    fb n | (Yes prf)   | (No contra) = Fizz n
   fb n | (No contra) with (decEq (n `mod` 5) 0)
     fb n | (No contra) | (Yes prf) = Buzz n
-    fb n | (No contra) | (No f) = N n
+    fb n | (No contra) | (No f)    = N n
 
 
+-- An infinite stream of the natural numbers, starting at 0 and going up. Z is
+-- 0, S is one plus its argument. `iterate` starts a stream with its second
+-- argument, then generates each new element by applying its first argument to
+-- the previous element.
 nats : Stream Nat
 nats = iterate S Z
 
+--- A stream of pairs of Nats and their corresponding output. Use `tail`
+--- because the problem says to start at 1.
 fizzBuzz : Stream (n : Nat ** FB n)
 fizzBuzz = map (\n => (n ** (fb n))) (tail nats)
 
+-- Generate output for the screen. The type system can't help us here!
 instance Show (n : Nat ** FB n) where
   show (x ** N x)        = show x
   show (x ** Fizz x)     = "Fizz"
   show (x ** Buzz x)     = "Buzz"
   show (x ** FizzBuzz x) = "FizzBuzz"
 
+-- Take the first 100 numbers' FizzBuzzes, then print them to the screen.
 namespace Main
   main : IO ()
   main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz

diff --git a/FizzBuzz.idr b/FizzBuzz.idr
@@ -0,0 +1,34 @@
+module FizzBuzz
+
+data FB : Nat -> Type where
+  N        : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto not5 : Not (n `mod` 5 = 0)} -> FB n
+  Fizz     : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto not4 : Not (n `mod` 5 = 0)} -> FB n
+  Buzz     : (n : Nat) -> {auto not3 : Not (n `mod` 3 = 0)} -> {auto div5 : n `mod` 5 = 0}       -> FB n
+  FizzBuzz : (n : Nat) -> {auto div3 : n `mod` 3 = 0}       -> {auto div5 : n `mod` 5 = 0}       -> FB n
+
+fb : (n : Nat) -> FB n
+fb n with (decEq (n `mod` 3) 0)
+  fb n | (Yes prf) with (decEq (n `mod` 5) 0)
+    fb n | (Yes prf) | (Yes x) = FizzBuzz n
+    fb n | (Yes prf) | (No contra) = Fizz n
+  fb n | (No contra) with (decEq (n `mod` 5) 0)
+    fb n | (No contra) | (Yes prf) = Buzz n
+    fb n | (No contra) | (No f) = N n
+
+
+nats : Stream Nat
+nats = iterate S Z
+
+fizzBuzz : Stream (n : Nat ** FB n)
+fizzBuzz = map (\n => (n ** (fb n))) (tail nats)
+
+instance Show (n : Nat ** FB n) where
+  show (x ** N x)        = show x
+  show (x ** Fizz x)     = "Fizz"
+  show (x ** Buzz x)     = "Buzz"
+  show (x ** FizzBuzz x) = "FizzBuzz"
+
+namespace Main
+  main : IO ()
+  main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz
+
No results found