Add Util.Digits modules

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/Digits.md

@@ -0,0 +1,189 @@
+# Viewing Integers as lists of digits
+
+```idris
+module Util.Digits
+
+import Data.Monoid.Exponentiation
+```
+
+<!-- idris
+-- TODO: Make these views sign-aware
+import System
+-->
+
+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
+-->
+
+## Primative functionality
+
+Take the integer log base 10 of an `Integer`
+
+```idris
+  log10 : Integer -> Nat
+  log10 i = log10' i 0
+    where
+      log10' : Integer -> (acc : Nat) -> Nat
+      log10' i acc = 
+        if 10 ^ acc > i
+          then acc
+          else log10' i (acc + 1)
+```
+
+## 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 (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 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 (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/Day9.md

@@ -1,4 +1,4 @@
-# Year 2016 Day 9
+# Year 2015 Day 9
 
 This day provides our first example of a graph traversal problem. We'll use a
 `Choose` based effectful breath first search to identify all the possible paths
@@ -210,11 +210,9 @@ lengths.
 
 ```idris
 shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
-  (paths : List (List Location)) -> Eff fs (List Location, Integer)
+  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
 shortestPath paths = do
-  lens <- traverse pathLen paths
+  shortest paths Nothing
-  let pairs = zip paths lens
-  shortest pairs Nothing
   where
     shortest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
       -> Eff fs (a, Integer)
@@ -228,6 +226,27 @@ shortestPath paths = do
             else shortest xs (Just y)
 ```
 
+Calculate the longest path from a list of paths by recursively comparing
+lengths.
+
+```idris
+longestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
+  (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer)
+longestPath paths = do
+  longest paths Nothing
+  where
+    longest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
+      -> Eff fs (a, Integer)
+    longest [] acc = note "No paths" acc
+    longest (x :: xs) acc = 
+      case acc of
+        Nothing => longest xs (Just x)
+        Just y => 
+          if (snd x) > (snd y)
+            then longest xs (Just x)
+            else longest xs (Just y)
+```
+
 ## Part Functions
 
 ### Part 1
@@ -236,7 +255,8 @@ Parse our locations, turn them into a `DistanceMap`, load that into our reader,
 generate our paths, then find the one with the shortest length.
 
 ```idris
-part1 : Eff (PartEff String) (Integer, ())
+part1 : 
+  Eff (PartEff String) (Integer, (DistanceMap, List (List Location, Integer)))
 part1 = do
   locations <- map lines (askAt "input") >>= traverse parseLocationPair
   info "Locations: \{show locations}"
@@ -246,13 +266,30 @@ part1 = do
   paths <- map Prelude.toList allPaths
   trace "Paths: \{show paths}"
   info "Found \{show $ length paths} paths"
-  (path, len) <- shortestPath paths
+  distances <- traverse pathLen paths
+  let pairs = zip paths distances
+  (path, len) <- shortestPath pairs
   info "Shortest Path: \{show path} \{show len}"
-  pure (len, ())
+  pure (len, (distance_map, pairs))
+```
+
+### Part 2
+
+Feed the locations back into a longest path function
+
+```idris
+part2 : (DistanceMap, List (List Location, Integer))
+  -> Eff (PartEff String) Integer
+part2 (distance_map, pairs) = do
+  runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
+  (path, len) <- longestPath pairs
+  info "Longest Path: \{show path} \{show len}"
+  pure len
 ```
 
 <!-- idris
 public export
 day9 : Day
-day9 = First 9 part1
+day9 = Both 9 part1 part2
 -->
+