Begin Day12

2 files changed, 37 insertions, 0 deletions

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
diff --git a/lakefile.lean b/lakefile.lean
index 5698911..d902aa3 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,6 +14,7 @@ lean_lib «Day8» where
 lean_lib «Day9» where
 lean_lib «Day10» where
 lean_lib «Day11» where
+lean_lib «Day12» where
 
 lean_lib «Common» where