Year 2015 Day 10 Part 1

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
   ]
 ```

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
+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) 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, ())
+```
+
+<!-- idris
+public export
+day10 : Day
+day10 = First 10 part1
+-->