From d47a964c47eb76b0fe0ebfed758e2f8eca675661 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 8 Dec 2024 00:20:53 -0500
Subject: [PATCH] refactor: factor out grid code into `Utils`

---
 src/Day4/Part1.idr | 19 ++++---------------
 src/Day4/Part2.idr |  1 +
 src/Utils.idr      | 23 +++++++++++++++++++++++
 3 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/src/Day4/Part1.idr b/src/Day4/Part1.idr
index 73a5b10..eb2a57f 100644
--- a/src/Day4/Part1.idr
+++ b/src/Day4/Part1.idr
@@ -3,17 +3,15 @@ module Day4.Part1
 import Data.String
 import Data.Vect
 
+import Utils
+
 %default total
 
 --- TYPES
 
 public export
 Board : Nat -> Nat -> Type
-Board h w = Vect h (Vect w Char)
-
-public export
-Pos : Nat -> Nat -> Type
-Pos h w = (Fin h, Fin w)
+Board h w = Grid h w Char
 
 
 public export
@@ -27,19 +25,10 @@ directions = [U, UR, R, DR, D, DL, L, UL]
 
 export
 parseInput : String -> Maybe (h ** w ** Board h w)
-parseInput inp =
-  let ls@(row :: _) = unpack <$> lines inp
-        | [] => Just (0 ** 0 ** [])
-      width = length row
-  in map (\l => (length l ** width ** fromList l))
-       (traverse (toVect width) ls)
+parseInput = parseGrid
 
 --- DATA
 
-export
-index : Pos h w -> Board h w -> Char
-index (i, j) = index j . index i
-
 predFin : Fin n -> Maybe (Fin n)
 predFin FZ = Nothing
 predFin (FS x) = Just $ weaken x
diff --git a/src/Day4/Part2.idr b/src/Day4/Part2.idr
index b8fd9a8..aa95510 100644
--- a/src/Day4/Part2.idr
+++ b/src/Day4/Part2.idr
@@ -4,6 +4,7 @@ import Data.String
 import Data.Vect
 
 import Day4.Part1
+import Utils
 
 %default total
 
diff --git a/src/Utils.idr b/src/Utils.idr
index 71811a4..d9b51e5 100644
--- a/src/Utils.idr
+++ b/src/Utils.idr
@@ -3,6 +3,7 @@ module Utils
 import Data.Maybe
 import Data.String
 import Data.String.Parser
+import Data.Vect
 
 %default total
 
@@ -28,3 +29,25 @@ scan p = until p *> p
 export covering
 scanWhile : Monad m => ParseT m a -> ParseT m b -> ParseT m b
 scanWhile w p = many (lookahead w *> requireFailure p *> skip (satisfy (const True))) *> p
+
+
+public export
+Grid : (h, w : Nat) -> Type -> Type
+Grid h w a = Vect h (Vect w a)
+
+public export
+Pos : (h, w : Nat) -> Type
+Pos h w = (Fin h, Fin w)
+
+export
+parseGrid : String -> Maybe (h ** w ** Grid h w Char)
+parseGrid str =
+  let ls@(row :: _) = unpack <$> lines str
+        | [] => Just (0 ** 0 ** [])
+      width = length row
+  in map (\l => (length l ** width ** fromList l))
+       (traverse (toVect width) ls)
+
+export
+index : Pos h w -> Grid h w a -> a
+index (i, j) = index j . index i