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