From 5d08e39abca75b775bb7636973bb9c9a3bb908ac Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 23 Sep 2024 21:31:41 +0200
Subject: Continue Day12

---
 Day12.lean | 49 ++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 42 insertions(+), 7 deletions(-)

(limited to 'Day12.lean')

diff --git a/Day12.lean b/Day12.lean
index a929c2f..69d2c9c 100644
--- a/Day12.lean
+++ b/Day12.lean
@@ -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)
-- 
cgit v1.2.3