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