Year 2015 Day 1

Pretty simple, basic warmup problem, nothing really novel is on display here except the effectful part computations.

Solver Functions

This one implements the entirety of the logic for part 1, in a simple tail recursive manner, pattern matching on each character in the input string.

We include a case for a non-paren character for totality's sake, but since we kinda trust the input here we just don't do anything in that branch.

trackFloor : (start : Integer) -> (xs : List Char) -> Integer
trackFloor start [] = start
trackFloor start ('(' :: xs) = trackFloor (start + 1) xs
trackFloor start (')' :: xs) = trackFloor (start - 1) xs
trackFloor start (x :: xs) = trackFloor start xs

This one is slightly more complicated, ultimately very similar to the above, but with two accumulators, one for the position in the input string in addition to the one for the current floor.

findBasement : (position : Nat) -> (currentFloor : Integer) -> (xs : List Char)
  -> Nat
findBasement position currentFloor [] = position
findBasement position currentFloor ('(' :: xs) =
  findBasement (position + 1) (currentFloor + 1) xs
findBasement position currentFloor (')' :: xs) =
  if currentFloor <= 0
    then position
    else findBasement (position + 1) (currentFloor - 1) xs
findBasement position currentFloor (x :: xs) =
  findBasement (position + 1) currentFloor xs

Part Functions

Both this parts are simple application of one of our solver functions

Part 1

Very uneventful, the only thing novel here is pulling the input out of the ReaderL "input" String, which will become very boring very quickly.

part1 : Eff (PartEff String) (Integer, ())
part1 = do
  input <- map unpack $ askAt "input"
  let output = trackFloor 0 input
  pure (output, ())

Part 2

We have to be careful to start the position accumulator at 1, since the problem specifies that the input string is 1-index.

part2 : () -> Eff (PartEff String) Nat
part2 x = do
  input <- map unpack $ askAt "input"
  pure $ findBasement 1 0 input