From 24d7fab85b2eb1b7996fd0ceccdd0377f1ce087b Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 1 Dec 2023 23:21:14 +0100
Subject: Day 1

---
 Main.lean | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 Main.lean

(limited to 'Main.lean')

diff --git a/Main.lean b/Main.lean
new file mode 100644
index 0000000..0739d43
--- /dev/null
+++ b/Main.lean
@@ -0,0 +1,46 @@
+import «Common»
+import «Day1»
+
+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
+  | _, _ => 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
-- 
cgit v1.2.3