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
144
145
146
147
148
149
150
151
|
import Common
namespace Day15
------------------------------------------------------------------------------------
inductive InvalidInput
| MissingSeparator
| InvalidFocalLength
| DeleteWithExtraData
instance : ToString InvalidInput where
toString := λ
| InvalidInput.MissingSeparator => "Each input step needs to contain either '-' xor '=' exactly once."
| InvalidInput.InvalidFocalLength => "Focal Length has to be an integer in the range [0-9]."
| InvalidInput.DeleteWithExtraData => "The Delete instruction must be at the end of the command."
private inductive Instruction (α β : Type)
| Remove (label : α) : Instruction α β
| Insert (label : α) (value : β) : Instruction α β
structure Command where
raw : Substring
instruction : Instruction Substring (Fin 10)
private def parseCommand (input : Substring) : Except InvalidInput Command :=
if let [l,v] := input.splitOn "=" then
if let some v := v.toNat? then
if h : v < 10 then
Except.ok $ {raw := input, instruction := Instruction.Insert l ⟨v,h⟩}
else
Except.error InvalidInput.InvalidFocalLength
else
Except.error InvalidInput.InvalidFocalLength
else if let [l,v] := input.splitOn "-" then
if v.isEmpty then
Except.ok $ {raw := input, instruction := Instruction.Remove l}
else
Except.error InvalidInput.DeleteWithExtraData
else
Except.error InvalidInput.MissingSeparator
/- Adjusted after part one. For part one this was just the first line and retunred List Substring-/
def parse (input : String) : Except InvalidInput (List Command) :=
let substrings := input.toSubstring.trim.splitOn ","
substrings.mapM parseCommand
------------------------------------------------------------------------------------
private def holidayAsciiStringHelper (currentValue : UInt8) (input : Substring) : UInt8 :=
input.foldl (λ(v : UInt8) (c : Char) ↦ 17*(c.toUInt8 + v)) currentValue
def part1 (input : List Command) : Nat :=
input.foldl (λc v ↦ c + (holidayAsciiStringHelper 0 v.raw).toNat) 0
------------------------------------------------------------------------------------
/- Feels a bit weird to implement a HashMap myself now, given that I've used one on previous days... -/
private class HolidayAsciiStringHelperAble (α : Type) where
holidayAsciiStringHelper : α → UInt8
private structure HolidayAsciiStringHelperManualArrangementProcedure (α β : Type) where
boxes : Array (List (α × β))
valid : boxes.size = UInt8.size
private def HolidayAsciiStringHelperManualArrangementProcedure.empty (α β : Type) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
{
boxes := Array.mkArray UInt8.size [],
valid := Array.size_mkArray _ _
}
private def HolidayAsciiStringHelperManualArrangementProcedure.insert {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (data : β) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label
let index := Fin.cast old.valid.symm h.toFin
let box := old.boxes[index]
let box := updateOrAppend box []
{
boxes := old.boxes.set index box
valid := (Array.size_set old.boxes index box index.isLt).substr old.valid
}
where
updateOrAppend (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) :=
match box with
| [] => ((label, data) :: accumulator).reverse
| b :: bs =>
if b.fst == label then
accumulator.reverse ++ (label, data) :: bs
else
updateOrAppend bs (b::accumulator)
private def HolidayAsciiStringHelperManualArrangementProcedure.remove {α β : Type} [HolidayAsciiStringHelperAble α] [BEq α] (label : α) (old : HolidayAsciiStringHelperManualArrangementProcedure α β) : HolidayAsciiStringHelperManualArrangementProcedure α β :=
let h := HolidayAsciiStringHelperAble.holidayAsciiStringHelper label
let index := Fin.cast old.valid.symm h.toFin
let box := old.boxes[index]
let box := tryRemove box []
{
boxes := old.boxes.set index box
valid := (Array.size_set old.boxes index box index.isLt).substr old.valid
}
where
tryRemove (box : List (α × β)) (accumulator : List (α × β)) : List (α × β) :=
match box with
| [] => accumulator.reverse
| b :: bs =>
if b.fst == label then
tryRemove bs accumulator
else
tryRemove bs (b :: accumulator)
/- Funny, by the way, that the riddle only needs insert/remove, but not find... -/
private def focussingPower (hashMap : HolidayAsciiStringHelperManualArrangementProcedure Substring (Fin 10)) : Nat :=
Prod.fst $
hashMap.boxes.foldl (
λ(totalPower, boxIndex) box ↦
let totalPower := Prod.fst $ box.foldl
(λ(totalPower, lensIndex) lens ↦ (totalPower + boxIndex * lensIndex * lens.snd.val, lensIndex + 1))
(totalPower, 1)
(totalPower, boxIndex + 1)
)
(0,1)
private instance : HolidayAsciiStringHelperAble Substring where
holidayAsciiStringHelper := holidayAsciiStringHelper 0
def part2 (input : List Command) : Nat := Id.run do
let mut map := HolidayAsciiStringHelperManualArrangementProcedure.empty Substring (Fin 10)
for command in input do
map := match command.instruction with
| Instruction.Insert label value => map.insert label value
| Instruction.Remove label => map.remove label
focussingPower map
------------------------------------------------------------------------------------
open DayPart
instance : Parse ⟨15, by simp⟩ (ι := List Command) where
parse := (Except.mapError ToString.toString) ∘ parse
instance : Part ⟨15,_⟩ Parts.One (ι := List Command) (ρ := Nat) where
run := λc ↦ some (part1 c)
instance : Part ⟨15,_⟩ Parts.Two (ι := List Command) (ρ := Nat) where
run := λc ↦ some (part2 c)
------------------------------------------------------------------------------------
private def testInput := "rn=1,cm-,qp=3,cm=2,qp-,pc=4,ot=9,ab=5,pc-,pc=6,ot=7"
#eval part2 <$> parse testInput
|
