From fdfa15daf8cee041f70b1797f4208910a3e71578 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Mon, 6 Jan 2025 14:32:48 -0500
Subject: [PATCH] Year 2015 Day 3 Part 2

---
 src/Years/Y2015/Day3.md | 52 ++++++++++++++++++++++++++++++++++++++---
 1 file changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/Years/Y2015/Day3.md b/src/Years/Y2015/Day3.md
index 10c0b17..cb3edbc 100644
--- a/src/Years/Y2015/Day3.md
+++ b/src/Years/Y2015/Day3.md
@@ -1,5 +1,7 @@
 # Day 3
 
+This day provides a gentle introduction to `mutual` blocks and mutually recursive functions. 
+
 <!-- idris
 module Years.Y2015.Day3
 
@@ -10,10 +12,15 @@ 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
@@ -61,7 +68,35 @@ visitedLocations xs = visitor xs empty (0, 0)
     -> (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))
+    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
@@ -73,14 +108,25 @@ Similar to the previous day, we get our input, unpack it, and traverse our effec
 ```idris
 part1 : Eff (PartEff String) (Nat, List Movement)
 part1 = do
-  input <- map unpack $ askAt "input"
+  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 = First 3 part1
+day3 = Both 3 part1 part2
 -->