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