1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
import «Common»
import Lean.Data.HashSet
import Lean.Data.HashMap
namespace Day3
structure Coordinate : Type 0 where
x : Nat
y : Nat
deriving Repr, BEq, Ord, Hashable
def Coordinate.default : Coordinate := {x := 0, y := 0}
/--Returns the adjacent fields, row-major order (this is important)-/
def Coordinate.adjacents : Coordinate → List Coordinate
| { x := 0, y := 0} => [
.mk 1 0,
.mk 1 1, .mk 0 1
]
| { x := 0, y := y} => [
.mk 0 y.pred, .mk 1 y.pred,
.mk 1 y,
.mk 0 y.succ, .mk 1 y.succ
]
| { x := x, y := 0} => [
.mk x.pred 0, .mk x.succ 0,
.mk x.pred 1, .mk x 1, .mk x.succ 1
]
| { x := x, y := y} => [
.mk x.pred y.pred, .mk x y.pred, .mk x.succ y.pred,
.mk x.pred y, .mk x.succ y,
.mk x.pred y.succ, .mk x y.succ, .mk x.succ y.succ
]
structure Part : Type 0 where
symbol : Char
position : Coordinate
deriving Repr
structure PartNumber : Type 0 where
value : Nat
positions : List Coordinate
deriving Repr, BEq
-- Schematic is just using lists, because at this point it's not clear what kind of lookup
-- is needed in part 2... Probably some kind of HashMap Coordinate Whatever, but that's
-- guesswork for now...
-- Parts can refine the data further, anyhow.
structure Schematic : Type 0 where
parts : List Part
numbers : List PartNumber
deriving Repr
/-- nextByChar gives the coordinate of the **next** character. -/
private def Coordinate.nextByChar : Coordinate → Char → Coordinate
| {x := _, y := oldY}, '\n' => { x := 0, y := oldY + 1 }
| {x := oldX, y := oldY}, _ => { x := oldX + 1, y := oldY }
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 := λ
| [], none => []
| [], some acc => [acc] -- if we are still accumulating a number at the end, commit
| a :: as, none =>
if p: a.snd.isDigit then
--start accumulating a PartNumber
helper as $ some {value := a.snd.asDigit p, positions := [a.fst]}
else
--not accumulating, not a digit, not of interest.
helper as none
| a :: as, some acc =>
if p: a.snd.isDigit then
--keep accumulating
helper as $ some {value := acc.value * 10 + a.snd.asDigit p, positions := a.fst :: acc.positions }
else
-- we were accumulating, aren't on a number any more -> commit
acc :: helper as none
helper input none
def parse (schematic : String) : Option Schematic := do
-- I think this one is easier if we don't split the input in lines. Because:
let charsWithCoordinates ← match schematic.toList with
| [] => none
| c :: cs => pure $ cs.scan (λ s c ↦ (uncurry Coordinate.nextByChar s, c)) (Coordinate.default, c)
-- Whitespaces are **intentionally** left in. This makes extracting the numbers easier.
pure $ {
parts := extractParts charsWithCoordinates
numbers := extractPartNumbers charsWithCoordinates
}
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 ↦
position.adjacents.any partCoordinates.contains
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.
-- 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 . == '*')
-- but the symbols aren't enough, they need to be adjacent to **exactly** 2 numbers
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
open DayPart
instance : Parse ⟨3, by simp⟩ (ι := Schematic) where
parse := parse
instance : DayPart.Part ⟨3,_⟩ Parts.One (ι := Schematic) (ρ := Nat) where
run := some ∘ part1
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
|
