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
---
 Day3.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Day3.lean')

diff --git a/Day3.lean b/Day3.lean
index 76c06be..e15e205 100644
--- a/Day3.lean
+++ b/Day3.lean
@@ -78,10 +78,10 @@ private def extractPartNumbers (input : List (Coordinate × Char)) : List PartNu
       acc :: helper as none
   helper input none
 
-def parse (schematic : String) : Option Schematic := do
+def parse (schematic : String) : Except String Schematic := do
   -- I think this one is easier if we don't split the input in lines. Because:
   let charsWithCoordinates ← match schematic.toList with
-    | [] => none
+    | [] => throw "Could not pare input: Empty"
     | c :: cs => pure $ cs.scan (λ s c ↦ (uncurry Coordinate.nextByChar s, c)) (Coordinate.default, c)
   -- Whitespaces are **intentionally** left in. This makes extracting the numbers easier.
   pure $ {
-- 
cgit v1.2.3