From 2ceb539bf306992e726280c24ce8d7b69e4c8b5e Mon Sep 17 00:00:00 2001 From: Andreas Grois 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