Day 11 Parsing

5 files changed, 276 insertions, 24 deletions

diff --git a/Common.lean b/Common.lean
index 1382714..177ae97 100644
--- a/Common.lean
+++ b/Common.lean
@@ -7,3 +7,4 @@ import Common.Char
 import Common.Euclid
 import Common.NonEmptyList
 import Common.Parsing
+import Common.Nat
diff --git a/Common/Nat.lean b/Common/Nat.lean
new file mode 100644
index 0000000..4c25315
--- /dev/null
+++ b/Common/Nat.lean
@@ -0,0 +1,13 @@
+namespace Nat
+
+theorem two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ : y < h) : x + w*y < w*h :=
+  Nat.le_pred_of_lt h₂
+  |> Nat.mul_le_mul_left w
+  |> Nat.add_le_add_iff_right.mpr
+  |> (Nat.mul_pred w h).subst (motive :=λx↦w * y + w ≤ x + w)
+  |> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right w (Nat.zero_lt_of_lt h₂))).subst
+  |> (Nat.add_comm _ _).subst (motive := λx↦x ≤ w*h)
+  |> Nat.le_sub_of_add_le
+  |> Nat.lt_of_lt_of_le h₁
+  |> λx↦(Nat.add_lt_add_right) x (w * y)
+  |> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt h₁)).mpr h₂))).subst
diff --git a/Common/Parsing.lean b/Common/Parsing.lean
index 4967385..d0e9427 100644
--- a/Common/Parsing.lean
+++ b/Common/Parsing.lean
@@ -1,31 +1,28 @@
 /- This file contains various parsing helpers. Started _after_ Day10. -/
 
 import Common.List
+import Common.Nat
 
 namespace Parsing
 
-structure RectangularGrid (Element : Type) where
+structure MaybeEmptyRectangularGrid (Element : Type) where
   width : Nat
   height : Nat
   elements : Array Element
-  valid : elements.size = width * height
+  size_valid : elements.size = width * height
+
+instance : Inhabited (MaybeEmptyRectangularGrid Element) where
+  default := { width := 0, height := 0, elements := Array.empty, size_valid := rfl}
+
+structure RectangularGrid (Element : Type) extends MaybeEmptyRectangularGrid Element where
+  not_empty : width > 0 ∧ height > 0
 
 structure RectangularGrid.Coordinate (grid : RectangularGrid Element) where
   x : Fin grid.width
   y : Fin grid.height
 
 private def RectangularGrid.Coordinate.toIndex {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Fin (grid.width * grid.height) :=
-  ⟨coordinate.x + grid.width * coordinate.y,
-    Nat.le_pred_of_lt coordinate.y.isLt
-    |> Nat.mul_le_mul_left grid.width
-    |> Nat.add_le_add_iff_right.mpr
-    |> (Nat.mul_pred grid.width grid.height).subst (motive :=λx↦grid.width * coordinate.y.val + grid.width ≤ x + grid.width)
-    |> (Nat.sub_add_cancel (Nat.le_mul_of_pos_right grid.width (Nat.zero_lt_of_lt coordinate.y.isLt))).subst
-    |> (Nat.add_comm _ _).subst (motive := λx↦x ≤ grid.width*grid.height)
-    |> Nat.le_sub_of_add_le
-    |> Nat.lt_of_lt_of_le coordinate.x.isLt
-    |> λx↦(Nat.add_lt_add_right) x (grid.width * coordinate.y.val)
-    |> (Nat.sub_add_cancel (Nat.le_of_lt ((Nat.mul_lt_mul_left (Nat.zero_lt_of_lt coordinate.x.isLt)).mpr coordinate.y.isLt))).subst⟩
+  ⟨coordinate.x + grid.width * coordinate.y, Nat.two_d_coordinate_to_index_lt_size coordinate.x.isLt coordinate.y.isLt⟩
 
 private def RectangularGrid.Coordinate.ofIndex (grid : RectangularGrid Element) (index : Fin (grid.width * grid.height)) : grid.Coordinate :=
   have : grid.width > 0 :=
@@ -42,11 +39,27 @@ theorem Coordinate.toIndex_inv_fromIndex {grid : RectangularGrid Element} (index
   simp only [RectangularGrid.Coordinate.toIndex, RectangularGrid.Coordinate.ofIndex, Nat.mod_add_div, Fin.eta]
 
 def RectangularGrid.Get {grid : RectangularGrid Element} (coordinate : grid.Coordinate) : Element :=
-  grid.elements[coordinate.toIndex]'(grid.valid.substr coordinate.toIndex.isLt)
+  grid.elements[coordinate.toIndex]'(grid.size_valid.substr coordinate.toIndex.isLt)
 
 instance : GetElem (RectangularGrid Element) (RectangularGrid.Coordinate grid) Element (λg _ ↦ g = grid) where
   getElem := λ g c h ↦ g.Get (h▸c)
 
+instance [ToString Element] : ToString (MaybeEmptyRectangularGrid Element) where
+  toString := λe ↦ Id.run do
+    let mut r := s!"Width: {e.width}, Height: {e.height}"
+    for h₂ : y in [0:e.height] do
+      r := r.push '\n'
+      for h₁ : x in [0:e.width] do
+        have : x + e.width *y < e.elements.size := by
+          simp[Membership.mem, inferInstance, Std.instMembershipNatRange] at h₁ h₂
+          rw[e.size_valid]
+          exact Nat.two_d_coordinate_to_index_lt_size h₁ h₂
+        r := r ++ (ToString.toString e.elements[x+e.width*y])
+    r
+
+instance [ToString Element] : ToString (RectangularGrid Element) where
+  toString := ToString.toString ∘ RectangularGrid.toMaybeEmptyRectangularGrid
+
 inductive RectangularGrid.ParseError (ParseCharError : Type)
 | NoInput : RectangularGrid.ParseError ParseCharError
 | NotRectangular : RectangularGrid.ParseError ParseCharError
@@ -58,21 +71,70 @@ instance [ToString ParseCharError] : ToString (RectangularGrid.ParseError ParseC
   | .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
+/-- Internal helper. Not private so it's usable in proofs. You probably want ofSubstring instead. -/
+protected def RectangularGrid.parseSingleLine (parseCharacter : Char → Except ParseCharError Element) (alreadyParsed : Array Element) (remainingLine : Substring) : Except (RectangularGrid.ParseError ParseCharError) (Array Element) :=
+  if _h₁ : remainingLine.isEmpty then
+    Except.ok alreadyParsed
+  else
+    let c := remainingLine.front
+    match parseCharacter c with
+    | Except.error e => Except.error $ RectangularGrid.ParseError.CharacterParsingError e
+    | Except.ok element =>
+      RectangularGrid.parseSingleLine parseCharacter (alreadyParsed.push element) (remainingLine.drop 1)
+termination_by remainingLine.bsize
+decreasing_by
+  simp_wf
+  simp only [Substring.isEmpty, Substring.bsize, Nat.sub_eq, beq_iff_eq] at _h₁
+  simp only [Substring.drop, Substring.bsize, Substring.nextn, Substring.next, String.Pos.add_byteIdx, Nat.sub_eq]
+  split
+  case isTrue h₂ =>
+    simp[←(congrArg String.Pos.byteIdx h₂)] at _h₁
+  case isFalse h₂ =>
+    simp[String.next, Char.utf8Size]
+    split <;> try split <;> try split
+    all_goals omega
 
-def RectangularGrid.parseLines (parseCharacter : Char → Except ParseCharError Element) (alreadyParsed : Array Element) (remainingLines : List Substring) : Except (RectangularGrid.ParseError ParseCharError) (Array Element × Nat × Nat) :=
-  sorry
+/-- Internal helper. Not private so it's usable in proofs. You probably want ofSubstring instead. -/
+protected def RectangularGrid.parseLines (parseCharacter : Char → Except ParseCharError Element) (alreadyParsed : MaybeEmptyRectangularGrid Element) (remainingLines : List Substring) : Except (RectangularGrid.ParseError ParseCharError) (RectangularGrid Element) :=
+  match remainingLines with
+  | [] =>
+    if h₁ : alreadyParsed.width = 0 ∨ alreadyParsed.height = 0 then
+      Except.error RectangularGrid.ParseError.NoInput
+    else
+      Except.ok {alreadyParsed with not_empty := ⟨Nat.pos_of_ne_zero (not_or.mp h₁).left, Nat.pos_of_ne_zero (not_or.mp h₁).right⟩}
+  | l :: ls =>
+    let currentSize := alreadyParsed.elements.size
+    match RectangularGrid.parseSingleLine parseCharacter alreadyParsed.elements l with
+    | Except.error e =>
+      Except.error e
+    | Except.ok elements =>
+      let newSize := elements.size
+      if alreadyParsed.height = 0 then -- first line
+        RectangularGrid.parseLines parseCharacter {
+          width := newSize
+          height := 1
+          elements
+          size_valid := (Nat.mul_one _).substr rfl
+        } ls
+      else
+        if h₂ : newSize = currentSize + alreadyParsed.width then
+          RectangularGrid.parseLines parseCharacter {
+            width := alreadyParsed.width
+            height := alreadyParsed.height + 1
+            elements
+            size_valid :=
+              alreadyParsed.size_valid.subst (motive := λx↦_=x+_) h₂
+              |> (Nat.mul_succ (alreadyParsed.width) (alreadyParsed.height)).substr
+          } ls
+        else
+          Except.error RectangularGrid.ParseError.NotRectangular
 
 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
+  let lines := lines.map Substring.trim
+  let lines := lines.filter $ not ∘ Substring.isEmpty
+  RectangularGrid.parseLines parseCharacter Inhabited.default lines
 
 def RectangularGrid.ofString (parseCharacter : Char → Except ParseCharError Element) (input : String) : Except (RectangularGrid.ParseError ParseCharError) (RectangularGrid Element) :=
   ofSubstring parseCharacter input.toSubstring
diff --git a/Day11.lean b/Day11.lean
index d061e96..da36989 100644
--- a/Day11.lean
+++ b/Day11.lean
@@ -1,3 +1,39 @@
 import «Common»
 
 namespace Day11
+
+inductive Pixel
+| void
+| galaxy
+
+instance : ToString Pixel where
+  toString := λ
+  | .void => "."
+  | .galaxy => "#"
+
+structure ParseCharError where
+  foundChar : Char
+
+instance : ToString ParseCharError where
+  toString := λx ↦ s!"Invalid character. Expected '#' or '.', but found {x.foundChar}"
+
+def parseCharacter : Char → Except ParseCharError Pixel
+| '.' => Except.ok Pixel.void
+| '#' => Except.ok Pixel.galaxy
+| foundChar => Except.error {foundChar}
+
+------------------------------------------------------------------------------------------
+
+private def testData := "...#......
+.......#..
+#.........
+..........
+......#...
+.#........
+.........#
+..........
+.......#..
+#...#.....
+"
+
+#eval Parsing.RectangularGrid.ofString parseCharacter testData
diff --git a/inputs/day11.input b/inputs/day11.input
new file mode 100644
index 0000000..bf6403e
--- /dev/null
+++ b/inputs/day11.input
@@ -0,0 +1,140 @@
+........#..........................#...............#.....#..................................#..........................#....................
+..............................................................................#.........................................................#...
+............#..............................#....................#.........................................#.................................
+................................#...........................................................................................................
+....................................................................................................#........................#..............
+..................#.....#.............................#..............................................................#......................
+.....................................#..............................#......#....................#.......#...................................
+...................................................................................#................................................#.......
+.......#.....................#..................................#.............................................#.............................
+..........................................................#............................#....................................................
+#............................................#.....#.......................................................................#................
+..................................#...........................................#.................................................#.........#.
+........................#........................................................................#..........................................
+....#.........#..........................................................................#..........................#.......................
+..............................#...........#......................#..........................................................................
+..................#.................#.......................................................................................................
+...........#................................................................................................................................
+......................................................#...................#...................#...................................#........#
+............................#...............#...............................................................................................
+....#................................................................................................#...............#........#.............
+.....................................#...........#...........#...............#..........#..............................................#....
+..............#......................................................#......................................#............#..................
+.........#.....................................................................................#............................................
+........................................................................................................#...................................
+............................................................................................................................................
+...#...........................................#..........................#.................................................................
+.................................................................................................#..........................................
+.............................#........................................................#....................#........#...........#...........
+............#......#.....................#.........#................#.......................................................................
+......................................................................................................#..................................#..
+..............................................................#.............................................................................
+.#........................#..............................................................#..................................................
+.........#.........................................................................#...............#...............#...............#........
+..................................#......................................#..................................................................
+............................................#............#.......#.............................#............................................
+............................#.......................#..........................................................#.......#.......#..........#.
+.....#..................................................................................#...................................................
+.................#.....................................................#..............................#.....................................
+.........................................#.....#............#......................................................................#........
+..........................................................................................................#.................................
+.................................................................#.............#............................................................
+.......................#.....#......................#......................................................................#................
+.#...........#.........................#.....................................................#.........#.........................#..........
+..................................................................................#..............................#..........................
+.......#...................................................................#................................................................
+................#..............#......................................................#...........#.....................#.............#.....
+.........................#...................#.............................................................#...............................#
+............................................................................................................................................
+........................................#.....................................................................................#.............
+....................#...............................................#........#........................#.....................................
+......#....................#................................#...............................#.....................#.........................
+.#..........................................................................................................................................
+............................................................................................................................................
+................#.............#...........#..........#............#....................................................#........#.....#.....
+.....................................#...................................................#........#...........#.............................
+....................#.........................................#............#................................................................
+#.................................................#..................................#.....................................#................
+............................................#................................................#.....................#........................
+..................................#.................................................................................................#.......
+.........#...............#..............#........................#............#..............................#..............................
+..............................#.........................#.......................................#.....#.....................................
+...............................................#.......................#....................................................................
+.....................#......................................................................................................................
+...............#...........................................................................................#................................
+..#...................................#....................................#........................#............#.............#............
+............................................#............................................#.............................................#....
+...............................................................#............................................................................
+........#.......................................................................................#..........................#................
+..........................#.......#......................#....................#.............................................................
+....#...........#.....................................................................................................#.....................
+...................................................................#..............#...................#..........................#..........
+..............................#..................................................................................#..........................
+.............#......#........................................#.........#..........................#.........................................
+.................................................#...................................#......................#............................#..
+........#..............................................#....................................................................................
+......................................#...................................#...................................................#.............
+............................................................................................................................................
+........................#.......................................................#.......................#...................................
+........................................................................................................................#.........#.........
+.......#....................................................................................................................................
+.............................................................#.....#........................#......................#.......................#
+#...........#.........................................................................#.....................................................
+...................................................#............................................#..........................#.........#......
+...................#................#....................................................................#.....#............................
+............................................................................................................................................
+..........................#............................#.......#.............................#..............................................
+....#...................................#........#......................#.....#.............................................................
+.....................................................................................................#.................#....................
+............................................#................................................................#.....................#........
+.........#.......................................................#...................#......................................................
+............................................................................................................................................
+................................#........................#.................#................................................................
+..........................#.........................................#.......................................................#..............#
+.#.................................................#.........#..............................................................................
+..................#.................#.............................................#.........#...........#............#......................
+.......................................................................................................................................#....
+.........#..................#...............................................................................................................
+............................................#........................................#.............................................#........
+........................................................................#...................................................................
+.#.................................................#..............#...........#............................#................................
+....................#.................#.........................................................#.........................................#.
+.............#.............................................................................#......................#........#................
+...............................#......................................................................#..........................#..........
+............................................................................................................................................
+........................#................................................#..............#...................................................
+........#.........................#......#.........#.........#..............................................................................
+..................................................................#................#............................#...........................
+..............................................................................................#.....#.......................................
+.....#......................................................................#...............................................................
+...................#.........................#........................................#..............................#..................#...
+.#.........................#.............................#.......................................#................................#.........
+............................................................................................................................................
+................................................#........................#...................................................#..............
+...........#............#.............................................................................#.....................................
+..................................#................................#...........#....................................#.......................
+#.........................................#....................................................#...............#............................
+.............................#...........................................................................................................#..
+.....#.......#.................................#.......................................#...........................................#........
+........................................................................................................#...................#...............
+...................................#.........................#..............................................................................
+.........#...........................................................#.............#..............................#.........................
+..................#........#.......................#....................................................................#......#........#...
+........................................................................................#...........#.......................................
+.................................#.......#..................................................................#...............................
+.............#......................................................................................................................#.......
+#.............................................................................#..................#..........................................
+....................#................#.......................#.............................#............#...................................
+....................................................................#...........................................#..........#.....#..........
+...............................#.......................#...............................................................................#....
+........#.......#...........................................................................................#...............................
+........................#..................................................................................................................#
+............................................................................................................................................
+..............................................................................................#......................................#......
+..........................................#..............................#...........#............................#.........................
+............#.............#..................................#..........................................#.................#.................
+........................................................................................................................................#...
+...................#.......................................................................#................................................
+#.................................#..................#.......................#..............................................................
+.............................#......................................................................#.....#.....#...................#.......
+......#........#.................................#............#......#......................................................................