diff --git a/Aoc2024/Day06/Parser.lean b/Aoc2024/Day06/Parser.lean index 3587f60..a57c903 100644 --- a/Aoc2024/Day06/Parser.lean +++ b/Aoc2024/Day06/Parser.lean @@ -6,20 +6,25 @@ open Std.Internal.Parsec.String open Std.Internal.Parsec open Std (HashSet) --- private def inputParser : Parser (List Int) := sorry +instance : Bind List where bind := List.bind +instance : Pure List where pure := List.pure -private def decorateWithCoordinates (s: String): List (Point × Char) := - s.splitOn "\n" |>.enum |>.bind (λ ⟨y, line⟩ => - line.toList.enum.map (λ ⟨x, c⟩ => (⟨x, y⟩, c)) - ) +private def decorateWithCoordinates (s: String): List (Point × Char) := do + let (y, line) <- s.splitOn "\n" |> .enum + let (x, c) <- line.toList.enum + pure (⟨x, y⟩, c) 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 (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip - let width <- xs.toArray.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input" - let height <- ys.toArray.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input" - pure { obstacles, start, width, height } + let width <- xs.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input" + let height <- ys.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input" + let bounds: Rectangle := { topLeft := Point.origin, width, height } + pure { obstacles, start, bounds } --- #guard parseReports exampleInput == Except.ok 42 +private def examplePuzzleInput := parseInput exampleInput +#guard (examplePuzzleInput.map (·.bounds)) == Except.ok (Rectangle.mk Point.origin 10 10) +#guard (examplePuzzleInput.map (·.start)) == Except.ok ⟨4, 6⟩ +#guard (examplePuzzleInput.map (·.obstacles.size)) == Except.ok 8 diff --git a/Aoc2024/Day06/Types.lean b/Aoc2024/Day06/Types.lean index f2a7b3c..a931f6e 100644 --- a/Aoc2024/Day06/Types.lean +++ b/Aoc2024/Day06/Types.lean @@ -4,7 +4,7 @@ open Std (HashSet) structure Point where x : Int y : Int -deriving BEq, Hashable, Repr +deriving BEq, Hashable, Repr, Inhabited def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y) @@ -14,9 +14,35 @@ inductive Direction where | Down | Left +def Direction.turnRight : Direction -> Direction + | Direction.Up => Direction.Right + | Direction.Right => Direction.Down + | Direction.Down => Direction.Left + | Direction.Left => Direction.Up + +def Point.step (p : Point) (d : Direction) : Point := + match d with + | Direction.Up => { p with y := p.y - 1 } + | Direction.Right => { p with x := p.x + 1 } + | Direction.Down => { p with y := p.y + 1 } + | Direction.Left => { p with x := p.x - 1 } + +def Point.origin : Point := { x := 0, y := 0 } + +structure Rectangle where + topLeft : Point + width: Nat + height: Nat +deriving Repr, BEq, Hashable, Inhabited + +def Rectangle.contains (r : Rectangle) (p : Point) : Bool := + r.topLeft.x ≤ p.x && p.x < r.topLeft.x + r.width && + 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 } + structure PuzzleInput where obstacles : HashSet Point - width : Nat - height : Nat + bounds : Rectangle start : Point deriving Repr