From fbfc13d252df50acf8ca6a58d0dec93e2dbe281f Mon Sep 17 00:00:00 2001 From: Matt Russell Date: Sun, 8 Dec 2024 19:49:07 +0000 Subject: [PATCH] wip --- Aoc2024/Day08/Parser.lean | 11 +++-------- Aoc2024/Day08/Solve.lean | 28 ++++++++-------------------- Aoc2024/Day08/Types.lean | 16 ++++++++++++---- Aoc2024/Utils.lean | 12 ++++++++++-- 4 files changed, 33 insertions(+), 34 deletions(-) diff --git a/Aoc2024/Day08/Parser.lean b/Aoc2024/Day08/Parser.lean index afb218e..4cecc79 100644 --- a/Aoc2024/Day08/Parser.lean +++ b/Aoc2024/Day08/Parser.lean @@ -2,20 +2,15 @@ import Aoc2024.Day08.Examples import Aoc2024.Day08.Types import Aoc2024.Utils import Std -open Std.Internal.Parsec.String -open Std.Internal.Parsec -instance : Bind List where bind := List.bind -instance : Pure List where pure := List.pure - -private def decorateWithCoordinates (s: String): List (Point × Char) := do +private def decorateWithCoordinates (s: String): List PointAndChar := do let (y, line) <- s.splitOn "\n" |> .enum let (x, c) <- line.toList.enum - pure (⟨x, y⟩, c) + pure ⟨⟨x, y⟩, c⟩ def parseInput (s : String): PuzzleInput := let decoratedChars := decorateWithCoordinates s - let (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip + 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 } diff --git a/Aoc2024/Day08/Solve.lean b/Aoc2024/Day08/Solve.lean index dca931b..34f6b6f 100644 --- a/Aoc2024/Day08/Solve.lean +++ b/Aoc2024/Day08/Solve.lean @@ -7,32 +7,20 @@ open Std (HashMap) -- Part 1 -private def groupByChar (decoratedChars : List (Point × Char)) : List (Char × List Point) := - decoratedChars.groupBy (λ (_, c1) (_, c2) => c1 == c2) |>.map (λ l => (l.head!.2, l.map (·.1))) +private def removeDots (decoratedChars : List PointAndChar) : List PointAndChar := decoratedChars.filter (·.char != '.') -#guard groupByChar [(⟨0, 0⟩, 'a'), (⟨1, 0⟩, 'a'), (⟨0, 1⟩, 'b'), (⟨1, 1⟩, 'b')] == [ - ('a', [⟨0, 0⟩, ⟨1, 0⟩]), - ('b', [⟨0, 1⟩, ⟨1, 1⟩]) -] - -private instance hashableChar: Hashable Char where hash c := c.toNat |> hash - -private def removeDots (decoratedChars : List (Point × Char)) : List (Point × Char) := - decoratedChars.filter (λ (_, c) => c != '.') +private def getAntennaeGroups (input : PuzzleInput) : List (List Point) := + input.decoratedChars |> removeDots |>.groupByAndTransformValues (·.char) (·.point) |>.values private def findAntinodes (antennaGroup : List Point) : List Point := do let antenna1 <- antennaGroup let antenna2 <- antennaGroup if antenna1 != antenna2 then return antenna2.add (antenna1.vectorTo antenna2) - else - [] - -private def getAntennaeGroups (input : PuzzleInput) : List (List Point) := - input.decoratedChars |> removeDots |>.toArray.groupByKey (·.2) |>.map (λ _ v => v.map (·.1) |>.toList) |>.values + [] private def solvePart1 (input : PuzzleInput) : Int := - getAntennaeGroups input |>.bind findAntinodes |>.filter (input.bounds.contains) |>.toSet.size + getAntennaeGroups input |>.flatMap findAntinodes |>.filter (input.bounds.contains) |>.toSet.size def parseAndSolvePart1 (s : String): Int := parseInput s |> solvePart1 @@ -44,15 +32,15 @@ private def combinationPairs [BEq α] (xs : List α) : List (α × α) := do let [x1, x2] <- xs.combinations 2 | [] return (x1, x2) -private def isInLineWith (pair : (Point × Point)) (point : Point) : Bool := +private def Point.isColinearWith (point : Point) (pair : (Point × Point)) : Bool := let (p1, p2) := pair let v1 := p1.vectorTo p2 let v2 := p1.vectorTo point v1.x * v2.y == v1.y * v2.x private def solvePart2 (input : PuzzleInput) : Int := - let antennaePairs := getAntennaeGroups input |>.bind combinationPairs - let isAntinode (point : Point) : Bool := antennaePairs.any (λ pair => isInLineWith pair point) + let antennaePairs := getAntennaeGroups input |>.flatMap combinationPairs + let isAntinode (point : Point) : Bool := antennaePairs.any point.isColinearWith -- exploiting special property of the input input.bounds.allPoints.countP isAntinode def parseAndSolvePart2 (s : String): Int := parseInput s |> solvePart2 diff --git a/Aoc2024/Day08/Types.lean b/Aoc2024/Day08/Types.lean index ce8636a..385ef96 100644 --- a/Aoc2024/Day08/Types.lean +++ b/Aoc2024/Day08/Types.lean @@ -32,15 +32,23 @@ 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 } +#guard !Rectangle.contains { topLeft := Point.origin, width := 2, height := 2 } { x := 2, y := 2 } + def Rectangle.allPoints (r : Rectangle) : List Point := do let x <- intRange r.topLeft.x (r.topLeft.x + r.width) let y <- intRange r.topLeft.y (r.topLeft.y + r.height) return { x := x, y := y } -#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 } +#guard Rectangle.allPoints { topLeft := Point.origin, width := 2, height := 2 } == + [{ x := 0, y := 0 }, { x := 0, y := 1 }, { x := 1, y := 0 }, { x := 1, y := 1 }] + +structure PointAndChar where + point: Point + char: Char +deriving Repr, Inhabited, BEq, Hashable structure PuzzleInput where bounds : Rectangle - decoratedChars : List (Point × Char) -deriving Repr, Inhabited, BEq + decoratedChars : List PointAndChar +deriving Repr, Inhabited, BEq, Hashable diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean index 2ddc037..9d7cfa6 100644 --- a/Aoc2024/Utils.lean +++ b/Aoc2024/Utils.lean @@ -2,7 +2,7 @@ import Std import Batteries open Std.Internal.Parsec.String open Std.Internal.Parsec -open Std (HashSet) +open Std (HashSet HashMap) -- https://brandonrozek.com/blog/writing-unit-tests-lean-4/ def Except.deq [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by @@ -166,7 +166,13 @@ namespace List #guard [1, 2, 3].combinations 4 == [] #guard [1, 2, 3, 4].combinations 2 == [[1, 2], [1, 3], [1, 4], [2, 3], [2, 4], [3, 4]] - -- xs.bind (λ x => (xs.filter (· != x)).combinations n.map (x :: ·)) + def groupByKey [BEq α] [Hashable α] (key : β → α) (xs : List β): HashMap α (List β) := + xs.toArray.groupByKey key |>.map (λ _ v => v.toList) + + def groupByAndTransformValues [BEq α] [Hashable α] (key : β → α) (f : β → γ) (xs : List β): HashMap α (List γ) := + xs.groupByKey key |>.map (λ _ v => v.map f) + + def flatMap {α : Type u} {β : Type v} (a : List α) (b : α → List β) : List β := join (map b a) end List @@ -217,3 +223,5 @@ def intRange (m n : Int) : List Int := #guard intRange 0 3 == [0, 1, 2] #guard intRange (-3) 2 == [-3, -2, -1, 0, 1] #guard intRange 1 1 == [] + +instance hashableChar: Hashable Char where hash c := c.toNat |> hash