From 3e9ab8b679faa68bf41addedae1ec0f963ee466a Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 1 Dec 2024 16:12:52 +0100
Subject: Day15, Part1

---
 Day15.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 Day15.lean

(limited to 'Day15.lean')

diff --git a/Day15.lean b/Day15.lean
new file mode 100644
index 0000000..dcc5f3b
--- /dev/null
+++ b/Day15.lean
@@ -0,0 +1,29 @@
+import Common
+
+namespace Day15
+------------------------------------------------------------------------------------
+
+def parse (input : String) : List Substring := input.toSubstring.trim.splitOn ","
+
+------------------------------------------------------------------------------------
+
+private def holidayAsciiStringHelper (currentValue : UInt8) (input : Substring) : UInt8 :=
+  input.foldl (λ(v : UInt8) (c : Char) ↦ 17*(c.toUInt8 + v)) currentValue
+
+def part1 (input : List Substring) : Nat :=
+  input.foldl (λc v ↦ c + (holidayAsciiStringHelper 0 v).toNat) 0
+
+------------------------------------------------------------------------------------
+
+open DayPart
+instance : Parse ⟨15, by simp⟩ (ι := List Substring) where
+  parse := Except.ok ∘ parse
+
+instance : Part ⟨15,_⟩ Parts.One (ι := List Substring) (ρ := Nat) where
+  run := some ∘ part1
+
+------------------------------------------------------------------------------------
+
+private def testInput := "rn=1,cm-,qp=3,cm=2,qp-,pc=4,ot=9,ab=5,pc-,pc=6,ot=7"
+
+#eval parse testInput |> part1
-- 
cgit v1.2.3

