diff --git a/08/Main.idr b/08/Main.idr index a564f09..c0f873b 100644 --- a/08/Main.idr +++ b/08/Main.idr @@ -64,6 +64,34 @@ checkVisible x@(FS _) y@(FS _) xs = compValue = index z xs in all (< compValue) before || all (< compValue) after +takeWhilePlus: Ord a => (a -> Bool) -> List a -> List a +takeWhilePlus f [] = [] +takeWhilePlus f (x :: []) = [x] +takeWhilePlus f (x :: rest) = + if f x + then x :: takeWhilePlus f rest + else [x] + +senicScore : {m : Nat} -> {n : Nat} -> (x: Fin m) -> (y: Fin n) -> Vect m (Vect n Nat) -> Nat +senicScore FZ y xs = 0 +senicScore x FZ xs = 0 +senicScore x@(FS _) y@(FS _) xs = + if x == last || y == last + then 0 + else let horizontal = index x xs + vertical = index y (transpose xs) + in scoreLinear y horizontal * scoreLinear x vertical + where scoreLinear : {o : Nat} -> (z: Fin o) -> Vect o Nat -> Nat + scoreLinear FZ xs = 0 + scoreLinear z@(FS _) xs = + let before = reverse . toList . takeFin z $ xs + after = drop 1 (toList (dropFin z xs)) + compValue = index z xs + beforeVisible = length (takeWhilePlus (< compValue) before) + afterVisible = length (takeWhilePlus (< compValue) after) + in beforeVisible * afterVisible + + showGrid : Vect n (Vect m Nat) -> String showGrid xs = let lines = map (concatMap show) xs @@ -100,6 +128,32 @@ testPart1 = putStrLn $ "Coordinate: " ++ show (x,y) ++ " Value: " ++ show val ++ " Expected Visible: " ++ show result putStrLn $ "Calculated Visible: " ++ show (checkVisible x y grid) ++ "\n" +testPart2 : IO () +testPart2 = + case parseGrid simple of + Nothing => putStrLn "Failed to parse grid" + Just (m ** n ** grid) => + do putStrLn "Grid: " + putStrLn (showGrid grid) + putStrLn "" + case coords m n of + Nothing => putStrLn "Hardcoded coords were invalid" + Just cordList => do let testingFn = singleTest m n grid + traverse_ testingFn cordList + printLn "Tests Done" + where coords : (m : Nat) -> (n : Nat) -> Maybe (List ((Fin m, Fin n), Nat)) + coords m n = + let raw : List ((Nat, Nat), Nat) + raw = [((1, 2), 4), ((3, 2), 8)] + in traverse (\(x, y) => map (\z => (z, y)) (finPair m n x)) raw + singleTest : (m : Nat) -> (n : Nat) -> Vect m (Vect n Nat) -> ((Fin m, Fin n), Nat) -> IO () + singleTest m n grid ((x, y), result) = + do let row = index x grid + let val = index y row + putStrLn $ "Coordinate: " ++ show (x,y) ++ " Value: " ++ show val ++ " Expected Score: " ++ show result + putStrLn $ "Calculated Visible: " ++ show (senicScore x y grid) ++ "\n" + + finRange : {n : Nat} -> List (Fin n) finRange {n = 0} = [] finRange {n = (S k)} = forget (allFins k) @@ -111,6 +165,12 @@ part1 {m} {n} grid = pairs = concatMap (\x => map (\y => (x, y)) cols) rows in length . Prelude.List.filter (\(x,y) => checkVisible x y grid) $ pairs +part2 : {m : Nat} -> {n: Nat} -> Vect m (Vect n Nat) -> Nat +part2 {m} {n} grid = + let rows = finRange {n=m} + cols = finRange {n=n} + pairs = concatMap (\x => map (\y => (x, y)) cols) rows + in foldl max 0 . map (\(x, y) => senicScore x y grid) $ pairs partial main : IO () main = @@ -122,3 +182,4 @@ main = Nothing => putStrLn "Failed to parse grid" Just (m ** n ** grid) => do putStrLn $ "Part 1: " ++ show (part1 grid) + putStrLn $ "Part 2: " ++ show (part2 grid)