advent.ipkg

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

src/Util/Digits.md

@@ -1,189 +0,0 @@
-# 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 2015 Day 9
+# Year 2016 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
@@ -292,4 +292,3 @@ public export
 day9 : Day
 day9 = Both 9 part1 part2
 -->
-