# \[Year 2015 Day 6\](https://adventofcode.com/2015/day/ 6. Introduction to the advent of code classic 2d grid problem. ```idris import Util import Data.List.Lazy import Data.List1 import Data.Vect import Data.Fin import Data.String import Data.IORef ``` ## Parsing and data structures ### Grid structure Since this is our first 2d grid problem, we'll keep it simple and use a `Vect` of `Vect`s to store our problem state, we'll revisit a more complicated but more efficient structure for storing a 2d `Grid` in a later problem. This alias adds 1 to each of its arguments to ensure non-emptyness. ```idris Grid : (rows, cols : Nat) -> Type -> Type Grid rows cols e = Vect (S rows) (Vect (S cols) e) ``` We also provide a type alias for the coordinates in this grid, a simple pair of `Fin`s. ```idris Coord : (rows, cols : Nat) -> Type Coord rows cols = (Fin (S rows), Fin (S cols)) ``` #### Range extraction helpers Convert a `Vect` to a lazy list ```idris vectToLazy : Vect n e -> LazyList e vectToLazy [] = [] vectToLazy (x :: xs) = x :: vectToLazy xs ``` Extract an inclusive range of indexes from a `Vect` as a lazy list ```idris extractSegment : (start, end : Fin n) -> Vect n e -> LazyList e extractSegment start end xs = let xs = take (1 + finToNat end) . vectToLazy $ xs in drop (finToNat start) xs ``` ### Command data structures The three types of action that can be performed on a light. ```idris data Action = On | Off | Toggle ``` The range of coordinates that a command affects ```idris record Range (rows, cols : Nat) where constructor MkRange top_left, bottom_right : Coord rows cols ``` Helper function to extract a range of values from our Grid. First extracts the range of rows this `Range` touches, then maps a an extractor for the range of columns it touches across them, before lazily concatenating the resulting lists. ```idris extractRange : Range rows cols -> Grid rows cols e -> LazyList e extractRange (MkRange (x_start, y_start) (x_end, y_end)) xs = let rs = extractSegment x_start x_end xs cs = map (extractSegment y_start y_end) rs in foldrLazy (\e, acc => e ++ acc) [] cs ``` An action and its associated range ```idris record Command (rows, cols : Nat) where constructor MkCmd action : Action range : Range rows cols ``` ### Parsing Pattern match on the action string, throwing an error if the action was invalid ```idris parseAction : Has (Except String) fs => (input : String) -> Eff fs Action parseAction "on" = pure On parseAction "off" = pure Off parseAction "toggle" = pure Toggle parseAction str = throw "Invalid action: \{str}" ``` Attempt to split the string into two parts on the comma, and then attempt to parse the parts as `Fin`s, throwing an appropriate error if anything goes wrong ```idris parseCoord : Has (Except String) fs => {rows, cols : Nat} -> (input : String) -> Eff fs (Coord rows cols) parseCoord input = case split (== ',') input of head ::: [] => throw "Pair only had one component: \{input}" head ::: [tail] => do x <- note "Invalid x coordinate: \{head}" $ parsePositive head y <- note "Invalid y coordinate: \{tail}" $ parsePositive tail pure (x, y) head ::: xs => throw "Pair had \{show $ 1 + length xs} components: \{input}" ``` Parse two pairs together into a range ```idris parseRange : Has (Except String) fs => {rows, cols : Nat} -> (pair1, pair2 : String) -> Eff fs (Range rows cols) parseRange pair1 pair2 = do top_left <- parseCoord pair1 bottom_right <- parseCoord pair2 pure $ MkRange top_left bottom_right ``` Split a string into a list of parts, pattern matching those parts to attempt to extract a `Command`. ```idris parseCommand : Has (Except String) fs => Has Logger fs => {rows, cols : Nat} -> (input : String) -> Eff fs (Command rows cols) parseCommand input = do trace "Parsing command: \{input}" case split (== ' ') input of "toggle" ::: [pair1, "through", pair2] => do range <- parseRange pair1 pair2 let cmd = MkCmd Toggle range debug "Parsed \{show cmd} from: \{input}" pure cmd "turn" ::: [action, pair1, "through", pair2] => do action <- parseAction action range <- parseRange pair1 pair2 let cmd = MkCmd action range debug "Parsed \{show cmd} from: \{input}" pure cmd _ => throw "Improper command: \{input}" ``` ## Problem structure Since we are dealing with a million slots here, we'll want some level of true mutability. The actual structure containing the slots doesn't need to be modified once its setup, so we'll make the mutability interior to the slots and keep a `Grid` of `IORef`s. We'll setup a helper function to initialize our grid based on a seed value. ```idris ioGrid : Has IO fs => (rows, cols : Nat) -> (seed : e) -> Eff fs $ Grid rows cols (IORef e) ioGrid rows cols seed = let grid : Grid rows cols _ = replicate _ (replicate _ (newIORef seed)) in traverse (traverse id) grid ``` Convert a `Grid` of `IORef`s into a `Grid` of pure values by traversing the `readIORef` operation over our `Grid`. ```idris purify : Has IO fs => {rows, cols : Nat} -> Grid rows cols (IORef e) -> Eff fs $ Grid rows cols e purify grid = traverse (traverse readIORef) grid ``` ## Solver Functions ### Part 1 Variants ```idris namespace Part1 ``` Apply a given command to our `Grid` of `IORef`s. Use our `extractRange` function to extract all the `IORef`s in the grid cells touched by our `Range` and then traverse an appropriate mutating action over them. ```idris applyCommand : Has IO fs => {rows, cols : Nat} -> Grid rows cols (IORef Bool) -> Command rows cols -> Eff fs () applyCommand xs (MkCmd action range) = let cells = extractRange range xs in case action of On => Lazy.traverse_ (`writeIORef` True) cells Off => Lazy.traverse_ (`writeIORef` False) cells Toggle => Lazy.traverse_ (`modifyIORef` not) cells ``` Apply a list of commands to our `Grid` of `IORef`s, doing some debug logging along the way. ```idris export applyCommands : Has IO fs => Has Logger fs => {rows, cols : Nat} -> Grid rows cols (IORef Bool) -> List (Command rows cols) -> Eff fs () applyCommands grid xs = applyCommands' 0 (length xs) xs where applyCommands' : (idx, len : Nat) -> List (Command rows cols) -> Eff fs () applyCommands' idx len [] = pure () applyCommands' idx len (x :: xs) = do debug "Part 1 - Applying command \{show idx}/\{show len}: \{show x}" applyCommand grid x applyCommands' (S idx) len xs ``` ### Part 2 Variants ```idris namespace Part2 ``` Much the same as above, but instead we apply the part 2 rules to a `Grid` of `Nat`. ```idris applyCommand : Has IO fs => {rows, cols : Nat} -> Grid rows cols (IORef Nat) -> Command rows cols -> Eff fs () applyCommand xs (MkCmd action range) = let cells = extractRange range xs in case action of On => Lazy.traverse_ (`modifyIORef` (+ 1)) cells Off => Lazy.traverse_ (`modifyIORef` (`minus` 1)) cells Toggle => Lazy.traverse_ (`modifyIORef` (+ 2)) cells ``` Identical to above, except for using our part 2 `applyCommand`. We can use the same name here because we have the two variants behind namespaces and Idris can disambiguate via the types. ```idris export applyCommands : Has IO fs => Has Logger fs => {rows, cols : Nat} -> Grid rows cols (IORef Nat) -> List (Command rows cols) -> Eff fs () applyCommands grid xs = applyCommands' 0 (length xs) xs where applyCommands' : (idx, len : Nat) -> List (Command rows cols) -> Eff fs () applyCommands' idx len [] = pure () applyCommands' idx len (x :: xs) = do debug "Part 2 - Applying command \{show idx}/\{show len}: \{show x}" applyCommand grid x applyCommands' (S idx) len xs ``` ## Day functions ### Part 1 Parse our commands, generate our initial `Grid` with all the lights turned off (represented by `False`), apply our commands to it, purify it, and count the lights that are turned on. Pass out our list of parsed commands as the context for reuse in part 2. ```idris part1 : Eff (PartEff String) (Nat, List (Command 999 999)) part1 = do input <- map (lines . trim) $ askAt "input" commands <- traverse parseCommand input grid <- ioGrid 999 999 False applyCommands grid commands grid <- purify grid let lights_on = sum . map (count id) $ grid pure $ (lights_on, commands) ``` ### Part 2 This time, use an initial `Grid` with all brightness values at 0, apply our list of preparsed commands using our part 2 `applyCommands` function (selected via the type signature), and then add up the brightnesses. ```idris part2 : List (Command 999 999) -> Eff (PartEff String) Nat part2 commands = do grid <- ioGrid 999 999 (the Nat 0) applyCommands grid commands grid <- purify grid let brightness = sum . map sum $ grid pure brightness ```