Year 2015 Day 10 Part 2

This commit is contained in:
Nathan McCarty 2025-01-22 22:23:05 -05:00
parent 71c29bbea4
commit 13b05ceb86
2 changed files with 21 additions and 9 deletions

View file

@ -38,3 +38,4 @@ solution.
- [Day 7](src/Years/Y2015/Day7.md)
- [Day 8](src/Years/Y2015/Day8.md)
- [Day 9](src/Years/Y2015/Day9.md)
- [Day 10](src/Years/Y2015/Day10.md)

View file

@ -30,7 +30,7 @@ import Util.Digits
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`.
[`Descending`](../../Util/Digits.md#descending-order) view to a `LazyList`.
```idris
lazyDigits : Integer -> LazyList Integer
@ -42,11 +42,11 @@ lazyDigits i with (descending i)
```
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.
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
@ -98,17 +98,28 @@ 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 : 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, ())
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 = First 10 part1
day10 = Both 10 part1 part2
-->