wip

Aoc2024/Day06/Main.lean

@@ -10,7 +10,7 @@ def main : IO Unit := do
   IO.println s!"Example: {<- parseAndSolvePart1 exampleInput}"
   let answerPart1 <- parseAndSolvePart1 puzzleInput
   IO.println s!"Puzzle: {answerPart1}"
-  assert! (answerPart1 == -1)
+  assert! (answerPart1 == 4967)
   IO.println ""
   IO.println "Part 2"
   IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"

Aoc2024/Day06/Parser.lean

@@ -16,8 +16,9 @@ private def decorateWithCoordinates (s: String): List (Point × Char) := do
 
 def parseInput (s: String): Except String PuzzleInput := do
   let decoratedChars := decorateWithCoordinates s
-  let obstacles := decoratedChars.filterMap (λ ⟨p, c⟩ => (c == '#').toOption p) |>.toSet
-  let start <- decoratedChars.filterMap (λ ⟨p, c⟩ => (c == '^').toOption p) |>.head? |>.getOrThrow "no start found"
+  let findPoints (c: Char) := decoratedChars.filterMap (λ ⟨p, c'⟩ => (c == c').toOption p)
+  let obstacles := findPoints '#' |>.toSet
+  let start <- findPoints '^' |>.head? |>.getOrThrow "no start found"
   let (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip
   let width <- xs.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input"
   let height <- ys.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input"

Aoc2024/Day06/Solve.lean

@@ -1,15 +1,62 @@
 import Aoc2024.Utils
 import Aoc2024.Day06.Examples
 import Aoc2024.Day06.Parser
+import Std
+open Std (HashSet)
 
-private def solvePart1 (input : PuzzleInput) : Int := sorry
+private structure PatrolState where
+  position : Point
+  direction : Direction := Direction.Up
+  obstacles : HashSet Point
+  bounds : Rectangle
+  visited : HashSet Point
+deriving Repr
+
+private def PatrolState.hasObstacle (s : PatrolState) (p : Point): Bool := s.obstacles.contains p
+
+private def PatrolState.initial (input : PuzzleInput) : PatrolState :=
+  { position := input.start, obstacles := input.obstacles, bounds := input.bounds, visited := singleton input.start }
+
+private def PatrolState.positionAhead (s : PatrolState) : Point := s.position.step s.direction
+
+private def PatrolState.turnRight (s : PatrolState) : PatrolState := { s with direction := s.direction.turnRight }
+
+private def PatrolState.stepForward (s : PatrolState) : PatrolState :=
+  let newPosition := s.position.step s.direction
+  { s with position := newPosition, visited := s.visited.insert newPosition }
+
+-- returns whether the guard has left the area
+private def stepGuard : StateM PatrolState Bool := do
+  let state ← get
+  let ahead := state.positionAhead
+  if state.hasObstacle ahead then
+    modify PatrolState.turnRight *> return false
+  else if state.bounds.contains ahead then
+    modify PatrolState.stepForward *> return false
+  else
+    return true
+
+-- returns true if simulation has ended early by running out of fuel
+private def simulatePatrol : Nat -> StateM PatrolState Bool
+  | 0 => return true
+  | fuel + 1 => do
+    let hasLeftArea <- stepGuard
+    if (hasLeftArea) then
+      return false
+    else
+      simulatePatrol fuel
+
+private def solvePart1 (input : PuzzleInput) : Int :=
+  let initialState := PatrolState.initial input
+  let (simulationEndedEarly, finalState) := (simulatePatrol 100000).run initialState
+  if simulationEndedEarly then -1 else finalState.visited.size
 
 def parseAndSolvePart1 (s : String): Except String Int := parseInput s |>.map solvePart1
 
--- #guard parseAndSolvePart1 exampleInput == Except.ok 41
+#guard parseAndSolvePart1 exampleInput == Except.ok 41
 
 private def solvePart2 (input : PuzzleInput) : Int := sorry
 
 def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok -1
+-- #guard parseAndSolvePart2 exampleInput == Except.ok 6

Aoc2024/Day06/Types.lean

@@ -13,6 +13,7 @@ inductive Direction where
   | Right
   | Down
   | Left
+deriving BEq, Repr, Inhabited, Hashable
 
 def Direction.turnRight : Direction -> Direction
   | Direction.Up => Direction.Right
@@ -40,6 +41,7 @@ def Rectangle.contains (r : Rectangle) (p : Point) : Bool :=
     r.topLeft.y ≤ p.y && p.y < r.topLeft.y + r.height
 
 #guard Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 1, y := 1 }
+#guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 }
 
 structure PuzzleInput where
   obstacles : HashSet Point