Year 2015 Day 4 Part 2

src/Years/Y2015/Day4.md

@@ -116,33 +116,44 @@ checkZeros key number =
 
 ### Find the first input with a specific number of zeros
 
-Search numbers starting at 1 and counting up in a tail recursive helper function. This function is going to be effectively impossible to prove totality for, so we have removed our normal `%default total` annotation for this file
+Search numbers starting at the provided seed and counting up in a tail recursive helper function. This function is going to be effectively impossible to prove totality for, so we have removed our normal `%default total` annotation for this file
 
 ```idris
-findFirst : (zeros : Nat) -> (key : String) -> Nat
+findFirst : (zeros : Nat) -> (key : String) -> (seed : Nat) -> Nat
-findFirst zeros key = findFirst' zeros key 1
+findFirst zeros key current = 
-  where
-    findFirst' : (zeros : Nat) -> (key : String) -> (current : Nat) -> Nat
-    findFirst' zeros key current = 
   if checkZeros key current >= zeros 
     then current
-        else findFirst' zeros key (current + 1)
+    else findFirst zeros key (current + 1)
 ```
 
 ## Part Functions
 
 ### Part 1
 
+Pass the input into our `findFirst` function and use the result as both our output and context value. Since part2 is searching for a longer run of 0s than part 1, numbers already checked by part 1 can not possibly be valid solutions for part 2, so we can skip them in part 2.
+
 ```idris
-part1 : Eff (PartEff String) (Nat, ())
+part1 : Eff (PartEff String) (Nat, Nat)
 part1 = do
   input <- map trim $ askAt "input"
-  let number = findFirst 5 input
+  let number = findFirst 5 input 0
-  pure (number, ())
+  pure (number, number)
+```
+
+### Part 2
+
+Start the `findFirst` search from the point where part 1 left off.
+
+```idris
+part2 : Nat -> Eff (PartEff String) Nat
+part2 seed = do
+  input <- map trim $ askAt "input"
+  let number = findFirst 6 input seed
+  pure number
 ```
 
 <!-- idris
 public export
 day4 : Day
-day4 = First 4 part1
+day4 = Both 4 part1 part2
 -->