diff --git a/advent.ipkg b/advent.ipkg index e915d93..1ac1a6e 100644 --- a/advent.ipkg +++ b/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) diff --git a/src/Util/Digits.md b/src/Util/Digits.md deleted file mode 100644 index 3cde674..0000000 --- a/src/Util/Digits.md +++ /dev/null @@ -1,189 +0,0 @@ -# Viewing Integers as lists of digits - -```idris -module Util.Digits - -import Data.Monoid.Exponentiation -``` - - - -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. - - - -## 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 - 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 - 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) -``` - diff --git a/src/Years/Y2015/Day9.md b/src/Years/Y2015/Day9.md index 1473ae2..8abf4b2 100644 --- a/src/Years/Y2015/Day9.md +++ b/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 --> -