Year 2015 Day 6

Introduction to the advent of code classic 2d grid problem.

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 Vects 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.

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 Fins.

Coord : (rows, cols : Nat) -> Type
Coord rows cols = (Fin (S rows), Fin (S cols))

Range extraction helpers

Convert a Vect to a lazy list

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

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.

data Action = On | Off | Toggle

The range of coordinates that a command affects

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.

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

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

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 Fins, throwing an appropriate error if anything goes wrong

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

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.

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 IORefs.

We'll setup a helper function to initialize our grid based on a seed value.

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 IORefs into a Grid of pure values by traversing the readIORef operation over our Grid.

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

namespace Part1

Apply a given command to our Grid of IORefs.

Use our extractRange function to extract all the IORefs in the grid cells touched by our Range and then traverse an appropriate mutating action over them.

  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 IORefs, doing some debug logging along the way.

  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

namespace Part2

Much the same as above, but instead we apply the part 2 rules to a Grid of Nat.

  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.

  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.

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.

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