move to parser

Author: mdr

Aoc2024/Day08/Parser.lean

@@ -8,10 +8,12 @@ private def decorateWithCoordinates (s: String): List PointAndChar := do
   let (x, c) <- line.toList.enum
   pure ⟨⟨x, y⟩, c⟩
 
+private def removeDots (decoratedChars : List PointAndChar) : List PointAndChar := decoratedChars.filter (·.char != '.')
+
 def parseInput (s : String): PuzzleInput :=
   let decoratedChars := decorateWithCoordinates s
   let (xs, ys) := decoratedChars.map (·.point.toPair) |>.unzip
   let width := xs.max?.map (· + 1 |>.toNat) |>.getD 0
   let height := ys.max?.map (· + 1 |>.toNat) |>.getD 0
   let bounds: Rectangle := { topLeft := Point.origin, width, height }
-  { bounds, decoratedChars }
+  { bounds, decoratedChars := removeDots decoratedChars }

Aoc2024/Day08/Solve.lean

@@ -7,10 +7,8 @@ open Std (HashMap)
 
 -- Part 1
 
-private def removeDots (decoratedChars : List PointAndChar) : List PointAndChar := decoratedChars.filter (·.char != '.')
-
 private def getAntennaeGroups (input : PuzzleInput) : List (List Point) :=
-  input.decoratedChars |> removeDots |>.groupByAndTransformValues (·.char) (·.point) |>.values
+  input.decoratedChars |>.groupByAndTransformValues (·.char) (·.point) |>.values
 
 private def findAntinodes (antennaGroup : List Point) : List Point := do
   let antenna1 <- antennaGroup

Aoc2024/Utils.lean

@@ -28,13 +28,6 @@ instance [BEq α] [BEq β] : BEq (Except α β) where
     | Except.error x, Except.error y => x == y
     | _, _ => false
 
-def getOrThrow (message : String) : Option α -> Except String α
-  | some x => pure x
-  | none => throw message
-
-#guard (getOrThrow "Error" (some 42) == Except.ok 42)
-#guard (getOrThrow "Error" (none : Option Int) == Except.error "Error")
-
 def sepBy (p : Parser α) (sep : Parser β) : Parser (List α) :=
   (do
     let x ← p