refactor: factor out grid code into Utils

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)
+Board h w = Grid h w Char
-
-public export
-Pos : Nat -> Nat -> Type
-Pos h w = (Fin h, Fin w)
 
 
 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 =
+parseInput = parseGrid
-  let ls@(row :: _) = unpack <$> lines inp
-        | [] => Just (0 ** 0 ** [])
-      width = length row
-  in map (\l => (length l ** width ** fromList l))
-       (traverse (toVect width) ls)
 
 --- 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

src/Day4/Part2.idr

@@ -4,6 +4,7 @@ import Data.String
 import Data.Vect
 
 import Day4.Part1
+import Utils
 
 %default total
 

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