diff --git a/src/Years/Y2015/Day4.md b/src/Years/Y2015/Day4.md index cd1538b..29c4ca8 100644 --- a/src/Years/Y2015/Day4.md +++ b/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 key = findFirst' zeros key 1 - 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) +findFirst : (zeros : Nat) -> (key : String) -> (seed : Nat) -> Nat +findFirst zeros key current = + if checkZeros key current >= zeros + then current + 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 - pure (number, ()) + let number = findFirst 5 input 0 + 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 ```