diff --git a/advent.ipkg b/advent.ipkg index 1ac1a6e..e915d93 100644 --- a/advent.ipkg +++ b/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) diff --git a/src/Util/Digits.md b/src/Util/Digits.md new file mode 100644 index 0000000..2df910c --- /dev/null +++ b/src/Util/Digits.md @@ -0,0 +1,190 @@ +# 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 acb702c..cf83b37 100644 --- a/src/Years/Y2015/Day9.md +++ b/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 - let pairs = zip paths lens - shortest pairs Nothing + shortest paths 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,29 @@ 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 ```