misc

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

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