Year 2015 Day 6 Part 1

README.md

@@ -23,3 +23,4 @@ The goal of this project is to get all 500 currently available stars in the form
   - [Day 3](src/Years/Y2015/Day3.md)
   - [Day 4](src/Years/Y2015/Day4.md)
   - [Day 5](src/Years/Y2015/Day5.md)
+  - [Day 6](src/Years/Y2015/Day6.md)

src/Years/Y2015.md

@@ -11,6 +11,7 @@ import Years.Y2015.Day2
 import Years.Y2015.Day3
 import Years.Y2015.Day4
 import Years.Y2015.Day5
+import Years.Y2015.Day6
 -->
 
 # Days
@@ -51,6 +52,12 @@ y2015 = MkYear 2015 [
   , day5
 ```
 
+## [Day 6](Y2015/Day6.md)
+
+```idris
+  , day6
+```
+
 ```idris
   ]
 ```

src/Years/Y2015/Day6.md

@@ -0,0 +1,261 @@
+# Day 6
+
+<!-- idris
+module Years.Y2015.Day6
+
+import Control.Eff
+
+import Runner
+-->
+
+```idris
+import Util
+
+import Data.List.Lazy
+import Data.List1
+import Data.Vect
+import Data.Fin
+import Data.String
+import Data.IORef
+```
+
+<!-- idris
+%default total
+-->
+
+## 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
+```
+
+<!-- idris
+Show Action where
+  show On = "on"
+  show Off = "off"
+  show Toggle = "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
+```
+
+<!-- idris
+Show (Range rows cols) where
+  show (MkRange top_left bottom_right) = 
+    "\{show top_left} -> \{show bottom_right}"
+-->
+
+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
+```
+
+<!-- idris
+Show (Command rows cols) where
+  show (MkCmd action range) = 
+    "{\{show action}: \{show range}}"
+-->
+
+### 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
+
+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
+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 "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)
+```
+
+<!-- idris
+public export
+day6 : Day
+day6 = First 6 part1
+-->