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.

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 view to a LazyList.

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.

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

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

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.

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

part2 : (digits : LazyList Integer) -> Eff (PartEff String) Nat
part2 digits = do
  output <- repeatLogged 10 digits
  pure $ count (const True) output