diff --git a/src/AllDays.idr b/src/AllDays.idr index e441f4c..884de46 100644 --- a/src/AllDays.idr +++ b/src/AllDays.idr @@ -14,3 +14,4 @@ import public Day6.Part1 import public Day6.Part2 import public Day7.Part1 import public Day7.Part2 +import public Day8.Part1 diff --git a/src/Day8/Part1.idr b/src/Day8/Part1.idr new file mode 100644 index 0000000..864e239 --- /dev/null +++ b/src/Day8/Part1.idr @@ -0,0 +1,54 @@ +module Day8.Part1 + +import Data.List +import Data.Vect + +import Utils + +%default total + +--- TYPES + +Map : (h, w : Nat) -> Type +Map h w = Grid h w (Maybe Char) + +--- PARSING + +parseInput : String -> Maybe (h ** w ** Map h w) +parseInput inp = do + (h ** w ** grid) <- parseGrid inp + pure (h ** w ** map (map (filter (/='.') . Just)) grid) + +--- DATA + +frequencies : Map h w -> List Char +frequencies mp = nub $ do + row <- toList mp + Just c <- toList row + | Nothing => empty + pure c + +antinodePos : {h, w : _} -> (a, b : Pos h w) -> Maybe (Pos h w) +antinodePos (x, y) (x', y') = + (,) <$> integerToFin (cast x * 2 - cast x') h + <*> integerToFin (cast y * 2 - cast y') w + +antinodes : {h, w : _} -> Map h w -> Char -> List (Pos h w) +antinodes mp c = do + let poss = do + i <- allFins h + j <- allFins w + guard (index (i, j) mp == Just c) + pure (i, j) + p1 <- poss + p2 <- poss + guard (p1 /= p2) + toList (antinodePos p1 p2) <|> toList (antinodePos p2 p1) + +--- SOLUTION + +export +solution : String -> Maybe Nat +solution inp = do + (h ** w ** mp) <- parseInput inp + pure $ length $ nub $ frequencies mp >>= antinodes mp diff --git a/src/Main.idr b/src/Main.idr index 65448ab..3f1f3e8 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 7 Part2 +latest = Pr 8 Part1 solMap : SortedMap Problem (String -> String)