diff --git a/08/Main.idr b/08/Main.idr index c0f873b..43dd71d 100644 --- a/08/Main.idr +++ b/08/Main.idr @@ -8,14 +8,6 @@ import Debug.Trace %default total -simple = """ - 30373 - 25512 - 65332 - 33549 - 35390 - """ - -- Parse a grid of numbers from a string parseGrid : String -> Maybe (n ** m ** Vect n (Vect m Nat)) parseGrid input = @@ -41,10 +33,6 @@ dropLast : {n : Nat} -> Vect (S n) a -> Vect n a dropLast {n = 0} (x :: xs) = xs dropLast {n = (S k)} (x :: xs) = x :: dropLast xs -tagTrace : Show a => String -> a -> a -tagTrace str = - traceValBy (\x => str ++ ": " ++ show x) - -- Check if a tree is visible from the edge of the grid checkVisible : {n: Nat} -> {m: Nat} -> (x: Fin n) -> (y: Fin m) -> Vect n (Vect m Nat) -> Bool -- If either of the coordinates are zero or the maximum then the tree is on an edge and thus visible @@ -91,69 +79,6 @@ senicScore x@(FS _) y@(FS _) xs = afterVisible = length (takeWhilePlus (< compValue) after) in beforeVisible * afterVisible - -showGrid : Vect n (Vect m Nat) -> String -showGrid xs = - let lines = map (concatMap show) xs - in joinBy "\n" (toList lines) - -finPair : (m : Nat) -> (n : Nat) -> (Nat, Nat) -> Maybe (Fin m, Fin n) -finPair m n (x,y) = - do a <- natToFin x m - b <- natToFin y n - Just (a, b) - -testPart1 : IO () -testPart1 = - 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), Bool)) - coords m n = - let raw : List ((Nat, Nat), Bool) - raw = [((1,1), True), ((1, 2), True), ((1, 3), False), ((2, 1), True), ((2, 2), False), ((2, 3), True)] - 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), Bool) -> 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 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)