diff --git a/README.md b/README.md index 87ea2a4..1fb5198 100644 --- a/README.md +++ b/README.md @@ -20,3 +20,4 @@ The goal of this project is to get all 500 currently available stars in the form - 2015 - [Day 1](src/Years/Y2015/Day1.md) - [Day 2](src/Years/Y2015/Day2.md) + - [Day 3](src/Years/Y2015/Day3.md) diff --git a/src/Util.md b/src/Util.md index 5e4db45..f015e61 100644 --- a/src/Util.md +++ b/src/Util.md @@ -4,6 +4,10 @@ This module contains functions that extend the functionality of standard data ty ```idris module Util + +import Data.SortedSet + +%default total ``` ## Either @@ -22,3 +26,43 @@ Applies a function to the contents of a `Left` if the value of the given `Either mapLeft f (Left x) = Left (f x) mapLeft f (Right x) = Right x ``` +## Vectors + +Define some operations for pairs of numbers, treating them roughly like vectors + +### Addition and Subtraction + + + +```idris + public export + (>+<) : Num a => (x, y : (a, a)) -> (a, a) + (x_1, x_2) >+< (y_1, y_2) = (x_1 + y_1, x_2 + y_2) + + public export + (>-<) : Neg a => (x, y : (a, a)) -> (a, a) + (x_1, x_2) >-< (y_1, y_2) = (x_1 - y_1, x_2 - y_2) +``` + +## Set + +Extend `Data.SortedSet` + + + +### length + +Count the number of elements in a sorted set + +```idris + export + length : SortedSet k -> Nat + length x = foldl (\acc, e => acc + 1) 0 x +``` diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 775cf7f..27c379d 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -4,10 +4,12 @@ module Years.Y2015 import Structures.Dependent.FreshList import Runner - +``` + # Days @@ -17,15 +19,25 @@ y2015 : Year y2015 = MkYear 2015 [ ``` -## [Day 1](./Day1.md) +## [Day 1](Y2015/Day1.md) ```idris day1 ``` -## [Day 2](./Day2.md) +## [Day 2](Y2015/Day2.md) ```idris , day2 +``` + +## [Day 3](Y2015/Day3.md) + +```idris + , day3 +``` + +```idris ] ``` + diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md new file mode 100644 index 0000000..cb3edbc --- /dev/null +++ b/src/Years/Y2015/Day3.md @@ -0,0 +1,132 @@ +# Day 3 + +This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. + + + +```idris +import Data.SortedSet +import Data.String + +import Util +``` + + + +## Parsing and data structures + +We'll do parsing a little more properly this time, turning the input into a list of movement commands + +```idris +data Movement = North | East | South | West +``` + +We need an effectful operation to parse a single char into a movement. We'll pattern match on the char, and include a catch-all case that throws an error in the event of an invalid char + +```idris +parseMovement : Has (Except String) fs => (x : Char) -> Eff fs Movement +parseMovement '^' = pure North +parseMovement '>' = pure East +parseMovement 'v' = pure South +parseMovement '<' = pure West +parseMovement x = throw "Invalid Movement: \{show x}" +``` + +We also need to be able to translate a `Movement` into a vector of length one pointing in the given direction in coordinate space. Somewhat arbitrarily, we chose 'North' to be positive x and 'East' to be positive y. + +```idris +vector : Movement -> (Integer, Integer) +vector North = (1, 0) +vector East = (0, 1) +vector South = (-1, 0) +vector West = (0, -1) +``` + +## Solver functions + +### Visited houses + +This is a pretty simple task, we are just applying the movements to our current position, and adding our current position to the set of visited locations, so we'll handle this with a normal tail recursive function. + +To keep the api nice, we wont ask for the set or the starting location in the top-level function, and instead have the top level function initialize the set and location before passing control to the inner tail-recursive variant. + +Because the starting location gets a present, we'll add our location to the set before performing the movement, so we will need to add our final location to the set in the recursive base case. + +```idris +visitedLocations : List Movement -> SortedSet (Integer, Integer) +visitedLocations xs = visitor xs empty (0, 0) + where + visitor : (moves : List Movement) -> (set : SortedSet (Integer, Integer)) + -> (location : (Integer, Integer)) -> SortedSet (Integer, Integer) + visitor [] set location = insert location set + visitor (x :: xs) set location = + visitor xs (insert location set) (location >+< vector x) +``` + +### Robo Santa + +This one gets a bit more interesting, we'll adopt the same tail recursive approach, but instead use a `mutual` block and two mutually recursive functions to handle the alternation between santa and robo santa. The `visitSanta` function will pass control to `visitRobo` after executing its movement, and vise versa. + +We'll want to insert both present deliverer's locations in the recursive base case, this may result in a duplicate location, but that's okay because `SortedSet` will only hold at most one of each item inserted into it. + +In idris, there is a general requirement that values be defined before their use, a common feature of dependently typed languages, resulting from the fact that just having the type signature of a function/value alone is not always enough to perform type checking, as functions can appear as part of types, requiring evaluation of the function and making automatic dependency analysis effectively impossible. + +Inside a `mutual` block, elaboration behaves differently, elaborating types first and then values in separate passes. This restricts what you can do a little, but enables mutually recursive functions. + +```idris +visitedLocations' : List Movement -> SortedSet (Integer, Integer) +visitedLocations' xs = visitSanta xs empty (0, 0) (0, 0) + where + mutual + visitSanta : (moves : List Movement) -> (set : SortedSet (Integer, Integer)) + -> (santa, robo : (Integer, Integer)) -> SortedSet (Integer, Integer) + visitSanta [] set santa robo = insert santa . insert robo $ set + visitSanta (x :: xs) set santa robo = + visitRobo xs (insert santa set) (santa >+< vector x) robo + + visitRobo : (moves : List Movement) -> (set : SortedSet (Integer, Integer)) + -> (santa, robo : (Integer, Integer)) -> SortedSet (Integer, Integer) + visitRobo [] set santa robo = insert santa . insert robo $ set + visitRobo (x :: xs) set santa robo = + visitSanta xs (insert robo set) santa (robo >+< vector x) +``` + +## Part Functions + +### Part 1 + +Similar to the previous day, we get our input, unpack it, and traverse our effectful movement parsing function over it, before feeding that into our solving function. + +```idris +part1 : Eff (PartEff String) (Nat, List Movement) +part1 = do + input <- map (unpack . trim) $ askAt "input" + movements <- traverse parseMovement input + let locations = visitedLocations movements + pure (length locations, movements) +``` + +### Part 2 + +Same as Part 1, but with a different solving function + +```idris +part2 : (movements : List Movement) -> Eff (PartEff String) Nat +part2 movements = do + let locations = visitedLocations' movements + pure . length $ locations +``` + +