Day 8 cleanup

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)