From 2ceb539bf306992e726280c24ce8d7b69e4c8b5e Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 19 Sep 2024 00:14:18 +0200
Subject: Day 11 Parsing

---
 Day11.lean | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

(limited to 'Day11.lean')

diff --git a/Day11.lean b/Day11.lean
index d061e96..da36989 100644
--- a/Day11.lean
+++ b/Day11.lean
@@ -1,3 +1,39 @@
 import «Common»
 
 namespace Day11
+
+inductive Pixel
+| void
+| galaxy
+
+instance : ToString Pixel where
+  toString := λ
+  | .void => "."
+  | .galaxy => "#"
+
+structure ParseCharError where
+  foundChar : Char
+
+instance : ToString ParseCharError where
+  toString := λx ↦ s!"Invalid character. Expected '#' or '.', but found {x.foundChar}"
+
+def parseCharacter : Char → Except ParseCharError Pixel
+| '.' => Except.ok Pixel.void
+| '#' => Except.ok Pixel.galaxy
+| foundChar => Except.error {foundChar}
+
+------------------------------------------------------------------------------------------
+
+private def testData := "...#......
+.......#..
+#.........
+..........
+......#...
+.#........
+.........#
+..........
+.......#..
+#...#.....
+"
+
+#eval Parsing.RectangularGrid.ofString parseCharacter testData
-- 
cgit v1.2.3

