wip

Aoc2024/Day06/Main.lean

@@ -16,4 +16,4 @@ def main : IO Unit := do
   IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"
   let answerPart2 <- parseAndSolvePart2 puzzleInput
   IO.println s!"Puzzle: {answerPart2}"
-  assert! (answerPart2 == -1)
+  assert! (answerPart2 == 1789)

Aoc2024/Day06/Solve.lean

@@ -4,12 +4,15 @@ import Aoc2024.Day06.Parser
 import Std
 open Std (HashSet)
 
+-- Part 1
+
 private structure PatrolState where
   position : Point
   direction : Direction := Direction.Up
   obstacles : HashSet Point
   bounds : Rectangle
   visited : HashSet Point
+  hasLooped : Bool := false
 deriving Repr
 
 private def PatrolState.hasObstacle (s : PatrolState) (p : Point): Bool := s.obstacles.contains p
@@ -23,9 +26,13 @@ private def PatrolState.turnRight (s : PatrolState) : PatrolState := { s with di
 
 private def PatrolState.stepForward (s : PatrolState) : PatrolState :=
   let newPosition := s.position.step s.direction
-  { s with position := newPosition, visited := s.visited.insert newPosition }
+  let hasLooped := s.visited.contains newPosition
+  { s with position := newPosition, visited := s.visited.insert newPosition, hasLooped }
+
+private def PatrolState.addObstacle (s : PatrolState) (p : Point) : PatrolState :=
+  { s with obstacles := s.obstacles.insert p }
 
--- returns whether the guard has left the area
+-- returns true iff the guard has left the area
 private def stepGuard : StateM PatrolState Bool := do
   let state ← get
   let ahead := state.positionAhead
@@ -36,7 +43,7 @@ private def stepGuard : StateM PatrolState Bool := do
   else
     return true
 
--- returns true if simulation has ended early by running out of fuel
+-- returns true iff simulation has ended early by running out of fuel
 private def simulatePatrol : Nat -> StateM PatrolState Bool
   | 0 => return true
   | fuel + 1 => do
@@ -54,18 +61,22 @@ private def solvePart1 (input : PuzzleInput) : Option Int :=
   if simulationEndedEarly then none else some finalState.visited.size
 
 def parseAndSolvePart1 (s : String): Except String Int := do
-  let input <- parseInput s
-  let maybeSolution := solvePart1 input
-  maybeSolution.getOrThrow "simulation ended early"
+  solvePart1 (<- parseInput s) |>.getOrThrow "simulation ended early"
 
 #guard parseAndSolvePart1 exampleInput == Except.ok 41
 
+-- Part 2
+
+private def doesPatrolLoop (initialState: PatrolState): Bool :=
+  let (_, finalState) := (simulatePatrol MAX_FUEL).run initialState
+  finalState.hasLooped
+
 private def solvePart2 (input : PuzzleInput) : Int :=
   let initialState := PatrolState.initial input
   let (simulationEndedEarly, finalState) := (simulatePatrol MAX_FUEL).run initialState
-  sorry
-
+  let candidateObstacles := finalState.visited.erase input.start
+  candidateObstacles.toList.countP (doesPatrolLoop ∘ initialState.addObstacle)
 
 def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok 6
+#guard parseAndSolvePart2 exampleInput == Except.ok 6

DayXX/Parser.lean

@@ -7,6 +7,6 @@ open Std.Internal.Parsec
 
 private def inputParser : Parser (List Int) := sorry
 
-def parseThings : String -> Except String (List Int) := inputParser.run
+def parseInput : String -> Except String (List Int) := inputParser.run
 
--- #guard parseReports exampleInput == Except.ok 42
+-- #guard parseInput exampleInput == Except.ok 42

DayXX/Solve.lean

@@ -2,14 +2,18 @@ import Aoc2024.Utils
 import Aoc2024.DayXX.Examples
 import Aoc2024.DayXX.Parser
 
-private def solvePart1 (things : List Int) : Int := sorry
+-- Part 1
 
-def parseAndSolvePart1 (s : String): Except String Int := parseThings s |>.map solvePart1
+private def solvePart1 (input : List Int) : Int := sorry
+
+def parseAndSolvePart1 (s : String): Except String Int := parseInput s |>.map solvePart1
 
 -- #guard parseAndSolvePart1 exampleInput == Except.ok -1
 
-private def solvePart2 (things : List Int) : Int := sorry
+-- Part 2
+
+private def solvePart2 (input : List Int) : Int := sorry
 
-def parseAndSolvePart2 (s : String): Except String Int := parseThings s |>.map solvePart2
+def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
 
 -- #guard parseAndSolvePart2 exampleInput == Except.ok -1