From 2c1f2362c69ab20b10b61bdbebf8e5121eca38b1 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Wed, 18 Sep 2024 19:42:46 +0200
Subject: Continue Day11/Parsing

---
 Common/List.lean    |  5 +++++
 Common/Parsing.lean | 32 ++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/Common/List.lean b/Common/List.lean
index 0e8285e..b34f1e2 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -49,3 +49,8 @@ def compare {α : Type} [Ord α] (a b : List α) := match a, b with
 
 instance {α : Type} [Ord α] : Ord (List α) where
   compare := compare
+
+def not_empty_iff_size_gt_zero {list : List α} : list.isEmpty = false ↔ list.length > 0 :=
+  match list with
+  | [] => ⟨nofun, nofun⟩
+  | l :: ls => ⟨λ_ ↦ (List.length_cons l ls).substr (Nat.succ_pos ls.length), λ_ => rfl⟩
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index a89d785..4967385 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -1,5 +1,7 @@
 /- This file contains various parsing helpers. Started _after_ Day10. -/
 
+import Common.List
+
 namespace Parsing
 
 structure RectangularGrid (Element : Type) where
@@ -44,3 +46,33 @@ def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coor
 
 instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where
   getElem := λ g c h ↦ g.Get (h▸c)
+
+inductive RectangularGrid.ParseError (ParseCharError : Type)
+| NoInput : RectangularGrid.ParseError ParseCharError
+| NotRectangular : RectangularGrid.ParseError ParseCharError
+| CharacterParsingError : ParseCharError → RectangularGrid.ParseError ParseCharError
+
+instance [ToString ParseCharError] : ToString (RectangularGrid.ParseError ParseCharError) where
+  toString := λ
+  | .NoInput => "No input provided."
+  | .NotRectangular => "Input is not rectangular."
+  | .CharacterParsingError e => ToString.toString e
+
+def RectangularGrid.parseSingleLine (parseCharacter : Char → Except ParseCharError Element) (alreadyParsed : Array Element) (remainingLine : Substring) : Except (RectangularGrid.ParseError ParseCharError) (Array Element × Nat) :=
+  sorry
+
+def RectangularGrid.parseLines (parseCharacter : Char → Except ParseCharError Element) (alreadyParsed : Array Element) (remainingLines : List Substring) : Except (RectangularGrid.ParseError ParseCharError) (Array Element × Nat × Nat) :=
+  sorry
+
+def RectangularGrid.ofSubstring (parseCharacter : Char → Except ParseCharError Element) (input : Substring) : Except (RectangularGrid.ParseError ParseCharError) (RectangularGrid Element) :=
+  let input := input.trim
+  let lines := input.splitOn "\n"
+  if h₁ : lines.isEmpty then
+    throw RectangularGrid.ParseError.NoInput
+  else
+    --let height := lines.length
+    --let width := lines[0]'(List.not_empty_iff_size_gt_zero.mp $ (Bool.not_eq_true _).mp h₁)
+  sorry
+
+def RectangularGrid.ofString (parseCharacter : Char → Except ParseCharError Element) (input : String) : Except (RectangularGrid.ParseError ParseCharError) (RectangularGrid Element) :=
+  ofSubstring parseCharacter input.toSubstring
-- 
cgit v1.2.3