159 lines
5.1 KiB
Markdown
159 lines
5.1 KiB
Markdown
# [Year 2015 Day 3](https://adventofcode.com/2015/day/3)
|
|
|
|
This day provides a gentle introduction to `mutual` blocks and mutually
|
|
recursive functions.
|
|
|
|
```idris hide
|
|
module Years.Y2015.Day3
|
|
|
|
import Control.Eff
|
|
|
|
import Runner
|
|
```
|
|
|
|
```idris
|
|
import Data.SortedSet
|
|
import Data.String
|
|
|
|
import Util
|
|
```
|
|
|
|
```idris hide
|
|
%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 hide
|
|
public export
|
|
day3 : Day
|
|
day3 = Both 3 part1 part2
|
|
```
|