diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 0225c82..8a7b278 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -16,6 +16,7 @@ import Years.Y2015.Day6 import Years.Y2015.Day7 import Years.Y2015.Day8 import Years.Y2015.Day9 +import Years.Y2015.Day10 --> # Days @@ -80,6 +81,12 @@ y2015 = MkYear 2015 [ , day9 ``` +## [Day 10](Y2015/Day10.md) + +```idris + , day10 +``` + ```idris ] ``` diff --git a/src/Years/Y2015/Day10.md b/src/Years/Y2015/Day10.md new file mode 100644 index 0000000..da03797 --- /dev/null +++ b/src/Years/Y2015/Day10.md @@ -0,0 +1,114 @@ +# Year 2015 Day 10 + +This day doesn't really add anything new, but we will show off our new views for +viewing integers as lists of digits. + + + +```idris +import Data.String +import Data.List1 +import Data.List.Lazy +import Data.Monoid.Exponentiation +import Data.Nat.Views + +import Util +import Util.Digits +``` + + + +# Solver Functions + +Produce a lazy lists of the digits of a number, in descending order of +significance. This effectively translates our new +[`Descending`](../../Util/Digits.md) view to a `LazyList`. + +```idris +lazyDigits : Integer -> LazyList Integer +lazyDigits i with (descending i) + lazyDigits i | (NegDec rec) = lazyDigits _ | rec + lazyDigits 0 | Start = [] + lazyDigits ((digit * (10 ^ magnitude)) + rest) | (Prev _ digit rest rec) = + digit :: lazyDigits _ | rec +``` + +Apply the look-and-say rule to list of digits. We operate in the list-of-digits +space for efficiency, this number will grow into the hundreds of thousands of +digits, and Idris is currently lacking some needed primitive operations to +perform this operation in `Integer` space reasonably efficiently. A `LazyList` +is used here to avoid having to actually instantiate the entirety of these +reasonably large lists. + +```idris +lookAndSay : LazyList Integer -> LazyList Integer +lookAndSay digits = + -- Flatten the list once more + lazyConcat + -- Convert the produced numbers into lists of their digits + . map lazyDigits + -- re-flatten our list + . lazyConcat + -- Count the number of occurrences of each digit and emit [occurances, digit] + . map (\xs@(head ::: tail) => + (the (LazyList _) [natToInteger $ length xs, head])) + -- Group identical digits + . lazyGroup + $ digits +``` + +Apply the look-and-say rule to an integer, for repl testing + +```idris +lookAndSay' : Integer -> Integer +lookAndSay' i = + let digits = lazyDigits i + res = lookAndSay digits + in unDigits res 0 + where + unDigits : LazyList Integer -> (acc : Integer) -> Integer + unDigits [] acc = acc + unDigits (x :: xs) acc = unDigits xs (acc * 10 + x) +``` + +Repeatedly apply `lookAndSay` to a seed value, with logging + +```idris +repeatLogged : Has Logger fs => + (count : Nat) -> (seed : LazyList Integer) -> Eff fs $ LazyList Integer +repeatLogged 0 seed = pure seed +repeatLogged (S k) seed = do + trace "Remaining iterations: \{show (S k)} digits: \{show . count (const True) $ seed}" + repeatLogged k (lookAndSay seed) +``` + +# Part Functions + +## Part 1 + +Parse our input, convert it into a list of digits, then run our `lookAndSay` +function on it 40 times, and count the output digits. + +```idris +part1 : Eff (PartEff String) (Nat, ()) +part1 = do + input <- askAt "input" >>= (note "Invalid input" . parsePositive) + let input = lazyDigits input + info "Input: \{show input}" + output <- repeatLogged 40 input + pure (count (const True) output, ()) +``` + +