Year 2015 Day 10 Part 1

Contains views for seeing integers as lists of digits

advent.ipkg

@@ -26,6 +26,7 @@ depends = base
 modules = Runner
         , Util
         , Util.Eff
+        , Util.Digits
         , Grid
 
 -- main file (i.e. file to load at REPL)

src/Util.md

@@ -9,10 +9,24 @@ module Util
 import Data.SortedSet
 import Data.String
 import Data.List.Lazy
+import Data.List1
 
 %default total
 ```
 
+## Functions
+
+### repeatN
+
+Recursively applies `f` to `seed` N times
+
+```idris
+export
+repeatN : (times : Nat) -> (f : a -> a) -> (seed : a) -> a
+repeatN 0 f seed = seed
+repeatN (S times') f seed = repeatN times' f (f seed)
+```
+
 ## Either
 
 <!-- idris
@@ -167,3 +181,32 @@ cartProd x y =
     combine x [] rest = rest
     combine x (y :: ys) rest = (x, y) :: combine x ys rest
 ```
+
+### Concat
+
+Lazily concatenate a LazyList of LazyLists
+
+```idris
+export
+lazyConcat : LazyList (LazyList a) -> LazyList a
+lazyConcat [] = []
+lazyConcat (x :: xs) = x ++ lazyConcat xs
+```
+
+### Group
+
+Lazily group a LazyList
+
+```idris
+export
+lazyGroup : Eq a => LazyList a -> LazyList (List1 a)
+lazyGroup [] = []
+lazyGroup (x :: xs) = lazyGroup' xs x (x ::: [])
+  where
+    lazyGroup' : LazyList a -> (current : a) -> (acc : List1 a) -> LazyList (List1 a)
+    lazyGroup' [] current acc = [acc]
+    lazyGroup' (y :: ys) current acc@(head ::: tail) = 
+      if y == current
+        then lazyGroup' ys current (head ::: (y :: tail))
+        else acc :: lazyGroup (y :: ys)
+```

src/Util/Digits.md

@@ -0,0 +1,192 @@
+# Viewing Integers as lists of digits
+
+```idris
+module Util.Digits
+
+import Data.Monoid.Exponentiation
+```
+
+<!-- idris
+import System
+
+%default total
+-->
+
+This module provides views and associated functionality for treating `Integers`
+as if they were lists of numbers.
+
+Since `Integer` is a primitive type, that Idris can't directly reason about the
+structure of, we need to use some `believe_me`s, a hideously unsafe operation
+that completely bypasses the type checker, somewhere along the line. For
+teaching purposes, we'll do it here, but please consider a library like
+[prim](https://github.com/stefan-hoeck/idris2-prim) if you find yourself needing
+to prove properties about primitive types.
+
+<!-- idris
+-- This mutual block isn't strictly required, but is useful for literate purposes
+mutual
+-->
+
+## Primitive functionality
+
+Take the integer log base 10 of an `Integer`
+
+```idris
+  log10 : Integer -> Nat
+  log10 i = assert_total $ log10' i 0
+    where
+      covering
+      log10' : Integer -> (acc : Nat) -> Nat
+      log10' i acc = 
+        if i > 0
+          then log10' (i `div` 10) (S acc)
+          else acc
+```
+
+## Ascending Order
+
+View an integer as a list of digits, ordered from least significant digit to
+most significant digit.
+
+For a clarifying example:
+
+<!-- idris
+  -- @@test Ascending Digits Example
+  ascendingExample : IO Bool
+  ascendingExample = do
+    putStrLn "Expecting: \{show [5, 4, 3, 2, 1]}"
+    putStrLn "Got: \{show . ascList $ ascending 12345}"
+    pure $
+-->
+
+```idris
+    ascList (ascending 12345) == [5, 4, 3, 2, 1]
+```
+
+The view itself, storing the current digit, and the rest of the number, both as
+a raw integer and by a recursive `Ascending`. Acts as a proof that the number
+can be reproduced by multiplying the rest by 10 and then adding the current
+digit.
+
+```idris
+  ||| A view of an integer as a list of digits in order of ascending signifigance
+  public export
+  data Ascending : Integer -> Type where
+    ||| Indicates that the number was negative
+    NegAsc : (rec : Lazy (Ascending (negate i))) -> Ascending i
+    ||| Indicates we have already seen all the digits of a number
+    End : Ascending 0
+    ||| A digit and all the preceeding ones
+    Next : (digit : Integer) 
+        -> (rest : Integer)
+        -> (rec : Lazy (Ascending rest))
+        -> Ascending (rest * 10 + digit)
+  %name Ascending as, bs, cs
+```
+
+Generate an `Ascending` from an integer.
+
+```idris
+  ||| Covering function for `Ascending`
+  export
+  ascending : (i : Integer) -> Ascending i
+  ascending i = 
+    if i < 0 then NegAsc (ascending (assert_smaller i $ negate i)) else
+    let digit = i `mod` 10
+        rest = i `div` 10
+    in if rest == 0 
+      then believe_me $ Next digit rest (believe_me End)
+      else believe_me $ Next digit rest (ascending (assert_smaller i rest))
+```
+
+Convert an `Ascending` to a list
+
+```idris
+  export
+  ascList : {i : Integer} -> Ascending i -> List Integer
+  ascList as = reverse $ ascList' i as []
+    where
+      ascList' : (j : Integer) -> Ascending j -> (acc : List Integer) 
+        -> List Integer
+      ascList' k (NegAsc rec) acc = ascList' (negate k) rec acc
+      ascList' 0 End acc = acc
+      ascList' ((rest * 10) + digit) (Next digit rest rec) acc = 
+        ascList' rest rec (digit :: acc)
+```
+
+## Descending Order
+
+View an integer as a list of digits, ordered from most significant digit to
+least significant digit.
+
+For a clarifying example:
+
+<!-- idris
+  -- @@test Descending Digits Example
+  descendingExample : IO Bool
+  descendingExample = do
+    putStrLn "Expecting: \{show [1, 2, 3, 4, 5]}"
+    putStrLn "Got: \{show . decList $ descending 12345}"
+    pure $
+-->
+
+```idris
+    decList (descending 12345) == [1, 2, 3, 4, 5]
+```
+
+The view itself, storing the current digit, and the rest of the number, both as
+a raw integer and by a recursive `Ascending`. Acts as a proof that the number
+can be reproduced by appending the current digit to the rest of the number.
+
+```idris
+  ||| A view of an integer as a list of digits in order of descending 
+  ||| signifigance
+  public export
+  data Descending : Integer -> Type where
+    ||| Indicates that the number was negative
+    NegDec : (rec : Lazy (Descending (negate i))) -> Descending i
+    ||| Indicates we have already seen all the digits of a number
+    Start : Descending 0
+    ||| A digit and all the preceeding ones
+    Prev : (magnitude : Nat)
+        -> (digit : Integer)
+        -> (rest : Integer)
+        -> (rec : Lazy (Descending rest))
+        -> Descending ((digit * 10 ^ magnitude) + rest)
+  %name Descending ds, es, fs
+```
+
+Generate a `Descending` from an `Integer`
+
+```idris
+  export
+  descending : (i : Integer) -> Descending i 
+  descending i = 
+    if i < 0 then NegDec (descending (assert_smaller i $ negate i)) else
+    let magnitude = log10 i
+    in if magnitude == 0
+      then believe_me $ Prev 0 0 0 Start
+      else descending' magnitude i
+    where
+      descending' : (magnitude : Nat) -> (j : Integer) -> Descending j 
+      descending' 0 j = believe_me Start
+      descending' magnitude@(S m) j = 
+        let digit = j `div` 10 ^ m
+            rest = j - digit * 10 ^ m 
+        in believe_me $ Prev m digit rest (descending' m rest) 
+```
+
+Convert a `Descending` to a list
+
+```idris
+  export
+  decList : {i : Integer} -> Descending i -> List Integer
+  decList ds = reverse $ decList' ds []
+    where
+     decList' : {i : Integer} -> Descending i -> (acc : List Integer) -> 
+       List Integer
+     decList' (NegDec rec) acc = decList' rec acc
+     decList' Start acc = acc
+     decList' (Prev magnitude digit rest rec) acc = 
+       decList' rec (digit :: acc)
+```

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
+-->