From 85e7e293fc47a6aaed53b27c018c2c7256aab3ff Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 3 Dec 2023 22:43:50 +0100
Subject: Day 3, minor cleanup

---
 Day3.lean | 43 ++++++++++++-------------------------------
 1 file changed, 12 insertions(+), 31 deletions(-)

diff --git a/Day3.lean b/Day3.lean
index 81eb5b8..1cf1774 100644
--- a/Day3.lean
+++ b/Day3.lean
@@ -59,7 +59,7 @@ private def extractParts : List (Coordinate × Char) → List Part :=
   (List.map (uncurry $ flip Part.mk)) ∘ (List.filter $ not ∘ λ (sc : Coordinate × Char) ↦ sc.snd.isWhitespace || sc.snd.isDigit || sc.snd == '.')
 
 private def extractPartNumbers (input : List (Coordinate × Char)) : List PartNumber :=
-  let rec helper : (List (Coordinate × Char)) → Option PartNumber → List PartNumber := λ
+  let rec helper := λ
   | [], none => []
   | [], some acc => [acc] -- if we are still accumulating a number at the end, commit
   | a :: as, none =>
@@ -92,28 +92,25 @@ def parse (schematic : String) : Option Schematic := do
 def part1 (schematic : Schematic) : Nat :=
   -- fast lookup: We need to know if a part is at a given coordinate
   open Lean(HashSet) in
-  let partCoordinates : HashSet Coordinate :=
-    HashSet.insertMany HashSet.empty $ schematic.parts.map Part.position
-  let partNumbers := schematic.numbers.filter λ number ↦
-    number.positions.any λ position ↦
+  let partCoordinates := HashSet.insertMany HashSet.empty $ schematic.parts.map Part.position
+  let partNumbers := schematic.numbers.filter λnumber ↦
+    number.positions.any λposition ↦
       position.adjacents.any partCoordinates.contains
-  partNumbers.foldl (. + PartNumber.value .) 0
+  partNumbers.foldl (· + PartNumber.value ·) 0
 
 def part2 (schematic : Schematic) : Nat :=
-  -- and now it is obvous that keeping the parsed input free of opinions was a good idea.
+  -- and now it is obvious that keeping the parsed input free of opinions was a good idea.
   -- because here we need quick lookup for the numbers, not the parts.
   open Lean(HashMap) in
   let numberCoordinates : HashMap Coordinate PartNumber :=
-    Lean.HashMap.ofList $ schematic.numbers.bind $ λ pn ↦
-     pn.positions.map λ pos ↦
-      (pos, pn)
-  let gearSymbols := schematic.parts.filter (Part.symbol . == '*')
+    Lean.HashMap.ofList $ schematic.numbers.bind $ λ pn ↦ pn.positions.map (·, pn)
+  let gearSymbols := schematic.parts.filter (Part.symbol · == '*')
   -- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers
-  let numbersNextGearSymbols := List.dedup <$> gearSymbols.map λ gs ↦
+  let numbersNextGearSymbols := List.dedup <$> gearSymbols.map λgs ↦
     gs.position.adjacents.filterMap numberCoordinates.find?
-  let gearSymbols := numbersNextGearSymbols.filter (List.length . == 2)
-  let gearRatios : List Nat := gearSymbols.map λ l ↦ l.map PartNumber.value |> List.foldl (.*.) 1
-  gearRatios.foldl (.+.) 0
+  let gearSymbols := numbersNextGearSymbols.filter (List.length · == 2)
+  let gearRatios : List Nat := gearSymbols.map $ List.foldl (· * PartNumber.value ·) 1
+  gearRatios.foldl (· + ·) 0
 
 open DayPart
 
@@ -125,19 +122,3 @@ instance : DayPart.Part ⟨3,_⟩ Parts.One (ι := Schematic) (ρ := Nat) where
 
 instance : DayPart.Part ⟨3,_⟩ Parts.Two (ι := Schematic) (ρ := Nat) where
   run := some ∘ part2
-
-private def testInput := "467..114..
-...*......
-..35..633.
-......#...
-617*......
-.....+.58.
-..592.....
-......755.
-...$.*....
-.664.598..
-"
-
-#eval parse testInput
-
-#eval part1 <$> parse testInput
-- 
cgit v1.2.3