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
|
import «Common»
import «Day1»
import «Day2»
open DayPart
def try_run_day_part (day : Days) (part : Parts) (data : String) : IO String :=
let impl : {ι : Type} → (d : Days) → (p : Parts) → String → [Parse d (ι := ι)] → [Part d p (ι := ι)] → IO String := λ day part data ↦ do
let instructions ← if let some instructions := Parse.parse day data then
pure instructions
else
throw $ IO.userError "Failed to parse input file."
if let some result := (Part.run day part instructions).map ToString.toString then
pure result
else
throw $ IO.userError "Failed to find a solution."
match day, part with
| ⟨1,_⟩, Parts.One => impl ⟨1,_⟩ Parts.One data
| ⟨1,_⟩, Parts.Two => impl ⟨1,_⟩ Parts.Two data
| ⟨2,_⟩, Parts.One => impl ⟨2,_⟩ Parts.One data
| ⟨2,_⟩, Parts.Two => impl ⟨2,_⟩ Parts.Two data
| _, _ => throw $ IO.userError "The requested combination of day/part has not been implemented yet."
def main (parameters : List String): IO Unit := do
try
let (day, part, file) ← match parameters with
| [day, part, file] => pure (day, part, file)
| _ => throw $ IO.userError "This program needs to be invoked with 3 parameters: Day (1-25), Part (1-2) and a filename."
let invalid_day := IO.userError "The first parameter has to be a day, namely a value between 1 and 25."
let day ← if let some day := day.toNat? then pure day else throw invalid_day
let (day : Days) ←
if p : day > 0 ∧ day <= 25 then
pure ⟨day, p⟩
else
throw invalid_day
let invalid_part := IO.userError "The second parameter must be a part, namely 1 or 2."
let part ← if let some part := part.toNat? then pure part else throw invalid_part
let part ← match part with
| 1 => pure Parts.One
| 2 => pure Parts.Two
| _ => throw invalid_part
let file ← IO.FS.readFile file
let result ← try_run_day_part day part file
IO.println s!"Result: {result}"
catch e =>
IO.eprintln e
|
