From dd51ad5d96d1c100be48cf724e0a4375a512e117 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 8 Dec 2024 00:21:18 -0500
Subject: [PATCH] feat: part 6-1

---
 advent-of-code-2024.ipkg |  3 +-
 src/AllDays.idr          |  1 +
 src/Day6/Part1.idr       | 80 ++++++++++++++++++++++++++++++++++++++++
 src/Main.idr             |  2 +-
 4 files changed, 84 insertions(+), 2 deletions(-)
 create mode 100644 src/Day6/Part1.idr

diff --git a/advent-of-code-2024.ipkg b/advent-of-code-2024.ipkg
index 1c2bd0f..4a81040 100644
--- a/advent-of-code-2024.ipkg
+++ b/advent-of-code-2024.ipkg
@@ -19,4 +19,5 @@ modules = Main, Utils, AllDays,
           Day2.Part1, Day2.Part2,
           Day3.Part1, Day3.Part2,
           Day4.Part1, Day4.Part2,
-          Day5.Part1, Day5.Part2
+          Day5.Part1, Day5.Part2,
+          Day6.Part1
diff --git a/src/AllDays.idr b/src/AllDays.idr
index dfbce34..0fd2978 100644
--- a/src/AllDays.idr
+++ b/src/AllDays.idr
@@ -10,3 +10,4 @@ import public Day4.Part1
 import public Day4.Part2
 import public Day5.Part1
 import public Day5.Part2
+import public Day6.Part1
diff --git a/src/Day6/Part1.idr b/src/Day6/Part1.idr
new file mode 100644
index 0000000..1710ef6
--- /dev/null
+++ b/src/Day6/Part1.idr
@@ -0,0 +1,80 @@
+module Day6.Part1
+
+import Data.List
+import Data.Maybe
+import Data.Vect
+import Data.Vect.Quantifiers
+
+import Utils
+
+%default total
+
+--- TYPES
+
+data Direction = U | R | D | L
+
+-- True if there is a wall
+Map : Nat -> Nat -> Type
+Map h w = Grid h w Bool
+
+--- PARSING
+
+parseDir : Char -> Maybe Direction
+parseDir '^' = Just U
+parseDir '>' = Just R
+parseDir 'v' = Just D
+parseDir '<' = Just L
+parseDir _ = Nothing
+
+parseInput : String -> Maybe (h ** w ** (Map h w, Pos h w, Direction))
+parseInput inp = do
+  (h ** w ** grid) <- parseGrid inp
+  g <- findGuard grid
+  pure (h ** w ** ((map . map) (=='#') grid, g))
+  where
+    findGuard : Vect h (Vect w Char) -> Maybe (Pos h w, Direction)
+    findGuard [] = Nothing
+    findGuard (row :: vs) =
+      case any (\c => isItJust (parseDir c)) row of
+        Yes p => Just ((FZ, cast $ anyToFin p), fromJust _ @{anyToFinCorrect p})
+        No _ => map (mapFst (mapFst FS)) $ findGuard vs
+
+--- DATA
+
+predFin : Fin n -> Maybe (Fin n)
+predFin FZ = Nothing
+predFin (FS x) = Just $ weaken x
+
+moveDir : {h, w : _} -> Direction -> Pos h w -> Maybe (Pos h w)
+moveDir U (i, j) = (,j) <$> predFin i
+moveDir R (i, j) = (i,) <$> strengthen (FS j)
+moveDir D (i, j) = (,j) <$> strengthen (FS i)
+moveDir L (i, j) = (i,) <$> predFin j
+
+rotate : Direction -> Direction
+rotate U = R
+rotate R = D
+rotate D = L
+rotate L = U
+
+
+covering
+getRoute : {h, w : _} -> Direction -> Pos h w -> Map h w -> List (Pos h w)
+getRoute = go []
+  where
+    covering
+    go : List (Pos h w) -> Direction -> Pos h w -> Map h w -> List (Pos h w)
+    go route dir pos map =
+      let Just next = moveDir dir pos
+            | Nothing => pos :: route
+      in if index next map
+         then go (pos :: route) (rotate dir) pos map
+         else go (pos :: route) dir next map
+
+--- SOLUTION
+
+export covering
+solution : String -> Maybe Nat
+solution inp = do
+  (h ** w ** (mp, pos, dir)) <- parseInput inp
+  pure $ length $ nub $ getRoute dir pos mp
diff --git a/src/Main.idr b/src/Main.idr
index 1902a56..3f8d2d2 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -13,7 +13,7 @@ import AllDays
 ||| The latest problem that has been solved.
 -- NOTE: UPDATE AFTER EACH SOLUTION
 latest : Problem
-latest = Pr 5 Part2
+latest = Pr 6 Part1
 
 
 solMap : SortedMap Problem (String -> String)