125 lines
3.2 KiB
Markdown
125 lines
3.2 KiB
Markdown
# [Year 2015 Day 10](https://adventofcode.com/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
|
|
module Years.Y2015.Day10
|
|
|
|
import Control.Eff
|
|
|
|
import Runner
|
|
-->
|
|
|
|
```idris
|
|
import Data.String
|
|
import Data.List1
|
|
import Data.List.Lazy
|
|
import Data.Monoid.Exponentiation
|
|
import Data.Nat.Views
|
|
|
|
import Util
|
|
import Util.Digits
|
|
```
|
|
|
|
<!-- idris
|
|
%default total
|
|
-->
|
|
|
|
# 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#descending-order) 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 millions 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, LazyList Integer)
|
|
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, output)
|
|
```
|
|
|
|
## Part 2
|
|
|
|
Same thing, but 10 more times
|
|
|
|
```idris
|
|
part2 : (digits : LazyList Integer) -> Eff (PartEff String) Nat
|
|
part2 digits = do
|
|
output <- repeatLogged 10 digits
|
|
pure $ count (const True) output
|
|
```
|
|
|
|
<!-- idris
|
|
public export
|
|
day10 : Day
|
|
day10 = Both 10 part1 part2
|
|
-->
|