Year 2015 Day 3 Part 2

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/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
+export infixl 8 >+<
+export infixl 8 >-<
+
+namespace Pair
+-->
+
+```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`
+
+<!-- idris
+namespace Set
+-->
+
+### 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
+```

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,132 @@
+# Day 3
+
+This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. 
+
+<!-- idris
+module Years.Y2015.Day3
+
+import Control.Eff
+
+import Runner
+-->
+
+```idris
+import Data.SortedSet
+import Data.String
+
+import Util
+```
+
+<!-- idris
+%default total
+-->
+
+## 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
+```
+
+<!-- idris
+public export
+day3 : Day
+day3 = Both 3 part1 part2
+-->