src/AllDays.idr

@@ -14,5 +14,3 @@ import public Day6.Part1
 import public Day6.Part2
 import public Day7.Part1
 import public Day7.Part2
-import public Day8.Part1
-import public Day8.Part2

src/Day4/Part1.idr

@@ -1,6 +1,5 @@
 module Day4.Part1
 
-import Data.List
 import Data.String
 import Data.Vect
 
@@ -60,8 +59,8 @@ checkString board str = go (unpack str)
 export
 findChar : {h, w : _} -> Board h w -> Char -> List (Pos h w)
 findChar board c = do
-  i <- allFins h
-  j <- allFins w
+  i <- toList $ range {len=h}
+  j <- toList $ range {len=w}
   guard (index (i, j) board == c)
   pure (i, j)
 

src/Day6/Part2.idr

@@ -38,8 +38,8 @@ covering
 loopPos : {h, w : _} -> (Pos h w, Direction) -> Map h w
           -> List (Pos h w)
 loopPos g mp = do
-  i <- allFins h
-  j <- allFins w
+  i <- toList $ range {len=h}
+  j <- toList $ range {len=w}
   let obs = (i,j)
   guard (obs /= fst g && not (index obs mp)) -- must be empty space
   let cols = getCollisions g $ insertObs obs mp

src/Day8/Part1.idr

@@ -1,57 +0,0 @@
-module Day8.Part1
-
-import Data.List
-import Data.Vect
-
-import Utils
-
-%default total
-
---- TYPES
-
-public export
-Map : (h, w : Nat) -> Type
-Map h w = Grid h w (Maybe Char)
-
---- PARSING
-
-export
-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
-
-export
-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

src/Day8/Part2.idr

@@ -1,49 +0,0 @@
-module Day8.Part2
-
-import Data.List
-import Data.Vect
-
-import Day8.Part1
-import Utils
-
-%default total
-
---- DATA
-
-antinodePos : {h, w : _} -> (a, b : Pos h w) -> List (Pos h w)
-antinodePos (x, y) (x', y') = do
-  let dx = cast x' - cast x
-      dy = cast y' - cast y
-      (dx', dy') = reduce (dx, dy)
-  n <- [-(cast $ max h w)..(cast $ max h w)]
-  toList $
-    (,) <$> integerToFin (cast x + dx' * n) h
-        <*> integerToFin (cast y + dy' * n) w
-  where
-    reduce : (Integer, Integer) -> (Integer, Integer)
-    reduce (a, b) with (cast {to=Nat} $ abs a) | (cast {to=Nat} $ abs b)
-      _ | Z | _ = (a, b)
-      _ | _ | Z = (a, b)
-      _ | a'@(S _) | b'@(S _) =
-        let g = assert_total $ gcd a' b'
-        in (a `div` cast g, b `div` cast g)
-
-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)
-  antinodePos p1 p2
-
---- SOLUTION
-
-export
-solution : String -> Maybe Nat
-solution inp = do
-  (h ** w ** mp) <- parseInput inp
-  pure $ length $ nub $ frequencies mp >>= antinodes mp

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 8 Part2
+latest = Pr 7 Part2
 
 
 solMap : SortedMap Problem (String -> String)