From fda8a5b06d63aaa6b7db2ca7b2a7c0bd321bd16e Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 23 Sep 2024 10:46:14 +0200
Subject: Begin Day12

---
 Day12.lean | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 Day12.lean

(limited to 'Day12.lean')

diff --git a/Day12.lean b/Day12.lean
new file mode 100644
index 0000000..a929c2f
--- /dev/null
+++ b/Day12.lean
@@ -0,0 +1,36 @@
+import «Common»
+
+namespace Day12
+
+------------------------------------------------------------------------------------
+
+inductive SpringMask
+| operational
+| damaged
+| unknown
+
+structure SpringArrangement where
+  Mask : List SpringMask
+  DamagedGroups : List Nat
+
+inductive ParsingError
+| unknownSymbolInLeftBlock : Char → ParsingError
+| unknownSymbolInRightBlock : Char → ParsingError
+| missingBlockSeparator : ParsingError
+| noInput : ParsingError
+| missingLeftBlock : ParsingError
+| missingRightBlock : ParsingError
+
+instance : ToString ParsingError where
+  toString := λ
+  | .unknownSymbolInLeftBlock c => s!"Unkown character in left part of input: '{c}'. Expected '#', '.' or '?'."
+  | .unknownSymbolInRightBlock c => s!"Unknown character in right part of input. '{c}'. Expected either a numeric digit, or ','."
+  | .missingBlockSeparator => "An input line is missing a block separator (whitespace)."
+  | .noInput => "The input file is empty."
+  | .missingLeftBlock => "The left block, which should contain a map of operational ('.') or damaged ('#') springs, or the question mark ('?') is empty."
+  | .missingRightBlock => "The right block, which should contain a comma-separted list of numbers, is empty."
+
+
+
+def parse (input : String) : Except ParsingError SpringArrangement :=
+  sorry
-- 
cgit v1.2.3

