diff options
Diffstat (limited to 'Day12.lean')
| -rw-r--r-- | Day12.lean | 49 |
1 files changed, 42 insertions, 7 deletions
@@ -4,19 +4,19 @@ namespace Day12 ------------------------------------------------------------------------------------ -inductive SpringMask +inductive SpringState | operational | damaged | unknown structure SpringArrangement where - Mask : List SpringMask + Mask : List SpringState DamagedGroups : List Nat inductive ParsingError | unknownSymbolInLeftBlock : Char → ParsingError -| unknownSymbolInRightBlock : Char → ParsingError -| missingBlockSeparator : ParsingError +| nonNumericSymbolInRightBlock : Substring → ParsingError +| invalidNumberOfBlockSeparators : Nat → ParsingError | noInput : ParsingError | missingLeftBlock : ParsingError | missingRightBlock : ParsingError @@ -24,8 +24,8 @@ inductive 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)." + | .nonNumericSymbolInRightBlock s => s!"The right block contained an unknown symbol. Expected ',' or numeric digits. Found {s}" + | .invalidNumberOfBlockSeparators n => s!"An input line has an unexpected number of whitespace characters. Expected 1, found {n}." | .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." @@ -33,4 +33,39 @@ instance : ToString ParsingError where def parse (input : String) : Except ParsingError SpringArrangement := - sorry + let input := input.toSubstring.trim + let lines := input.splitOn "\n" + let lines := lines.filterMap λx ↦ + let r : Substring := x.trim + (Function.const Unit r) <$> Option.ofBool !r.isEmpty + if lines.isEmpty then + Except.error ParsingError.noInput + else + let splitLines := lines.map (·.splitOn " ") + let invalidLines := splitLines.map List.length |> List.filter (· ≠ 2) + if h : !invalidLines.isEmpty then + Except.error $ ParsingError.invalidNumberOfBlockSeparators $ invalidLines.head (List.not_empty_iff_size_gt_zero.mp ((Bool.not_eq_true' _).mp h) |> List.ne_nil_of_length_pos) + else + --splitLines.mapM + sorry +where + parseLeftBlock : Substring → List SpringState → Except ParsingError (List SpringState) := λs p ↦ + if s.isEmpty then + Except.ok p.reverse + else + match parseMaskChar s.front with + | .error e => .error e + | .ok v => parseLeftBlock (s.drop 1) $ v :: p + termination_by s => s.bsize + decreasing_by + simp_wf + rename_i h₁ + apply Substring.drop_bsize_dec _ _ h₁ Nat.one_ne_zero + parseMaskChar : Char → Except ParsingError SpringState := λ + | '#' => .ok .damaged + | '?' => .ok .unknown + | '.' => .ok .operational + | c => Except.error $ .unknownSymbolInLeftBlock c + parseRightBlock : Substring → Except ParsingError (List Nat) := λs ↦ + s.splitOn "," + |> List.mapM λs ↦ (Substring.toNat? s).toExcept (ParsingError.nonNumericSymbolInRightBlock s) |