diff --git a/Aoc2024/Day06/Main.lean b/Aoc2024/Day06/Main.lean index 2b7f4a2..7817a43 100644 --- a/Aoc2024/Day06/Main.lean +++ b/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}" diff --git a/Aoc2024/Day06/Parser.lean b/Aoc2024/Day06/Parser.lean index a57c903..4ad9234 100644 --- a/Aoc2024/Day06/Parser.lean +++ b/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" diff --git a/Aoc2024/Day06/Solve.lean b/Aoc2024/Day06/Solve.lean index 9811c74..a39659a 100644 --- a/Aoc2024/Day06/Solve.lean +++ b/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 diff --git a/Aoc2024/Day06/Types.lean b/Aoc2024/Day06/Types.lean index a931f6e..38d64bf 100644 --- a/Aoc2024/Day06/Types.lean +++ b/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