Year 2015 Day 3 Part 1

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)

src/Years/Y2015.md

@@ -4,10 +4,12 @@ module Years.Y2015
 import Structures.Dependent.FreshList
 
 import Runner
-
+```
+<!-- idris
 import Years.Y2015.Day1
 import Years.Y2015.Day2
-```
+import Years.Y2015.Day3
+-->
 
 # 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
   ]
 ```
+

src/Years/Y2015/Day3.md

@@ -0,0 +1,86 @@
+# Day 3
+
+<!-- idris
+module Years.Y2015.Day3
+
+import Control.Eff
+
+import Runner
+-->
+
+```idris
+import Data.SortedSet
+
+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))
+```
+
+## 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 $ askAt "input"
+  movements <- traverse parseMovement input
+  let locations = visitedLocations movements
+  pure (length locations, movements)
+```
+
+<!-- idris
+public export
+day3 : Day
+day3 = First 3 part1
+-->