blob: da36989f6360f8c2f44d9b48e07454a184774c1a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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
|
