From 8d6efb1c1fdddc1fbad167510ce25e56be684130 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 7 Dec 2023 20:26:51 +0100
Subject: Allow error messages in parsing (for debugging)

And fix an off-by-one in day 5
---
 Day6.lean | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 Day6.lean

(limited to 'Day6.lean')

diff --git a/Day6.lean b/Day6.lean
new file mode 100644
index 0000000..54464ea
--- /dev/null
+++ b/Day6.lean
@@ -0,0 +1,27 @@
+import Common.Option
+import Common.Helpers
+
+structure Race where
+  timeLimit : Nat
+  recordDistance : Nat
+
+private def parseLine (header : String) (input : String) : Option (List Nat) := do
+  if not $ input.startsWith header then
+    failure
+  let input := input.drop header.length |> String.trim
+  let numbers := input.split Char.isWhitespace
+    |> List.map String.trim
+    |> List.filter String.isEmpty
+  numbers.mapM String.toNat?
+
+def parse (input : String) : Option (List Race) := do
+  let lines := input.splitOn "\n"
+    |> List.map String.trim
+    |> List.filter String.isEmpty
+  let (times, distances) ← match lines with
+    | [times, distances] => Option.zip (parseLine "Time:" times) (parseLine "Distance:" distances)
+    | _ => none
+  if times.length != distances.length then
+    failure
+  let pairs := times.zip distances
+  return pairs.map $ uncurry Race.mk
-- 
cgit v1.2.3