diff --git a/README.md b/README.md index 1fb5198..87ea2a4 100644 --- a/README.md +++ b/README.md @@ -20,4 +20,3 @@ 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 f015e61..5e4db45 100644 --- a/src/Util.md +++ b/src/Util.md @@ -4,10 +4,6 @@ This module contains functions that extend the functionality of standard data ty ```idris module Util - -import Data.SortedSet - -%default total ``` ## Either @@ -26,43 +22,3 @@ 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 27c379d..775cf7f 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -4,12 +4,10 @@ module Years.Y2015 import Structures.Dependent.FreshList import Runner -``` - +``` # Days @@ -19,25 +17,15 @@ y2015 : Year y2015 = MkYear 2015 [ ``` -## [Day 1](Y2015/Day1.md) +## [Day 1](./Day1.md) ```idris day1 ``` -## [Day 2](Y2015/Day2.md) +## [Day 2](./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 deleted file mode 100644 index cb3edbc..0000000 --- a/src/Years/Y2015/Day3.md +++ /dev/null @@ -1,132 +0,0 @@ -# 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 -``` - -