# Year 2015 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
-->