From 4d9df6824b81fd15fad2934efe1335a43a295e82 Mon Sep 17 00:00:00 2001
From: Matt Russell <MattRussellUK@gmail.com>
Date: Wed, 4 Dec 2024 19:04:35 +0000
Subject: [PATCH] tidying

---
 Aoc2024/Day04/Solve.lean | 30 +++--------------------
 Aoc2024/Utils.lean       | 53 ++++++++++++++++++++++++++++------------
 2 files changed, 41 insertions(+), 42 deletions(-)

diff --git a/Aoc2024/Day04/Solve.lean b/Aoc2024/Day04/Solve.lean
index d175be7..bfe86d4 100644
--- a/Aoc2024/Day04/Solve.lean
+++ b/Aoc2024/Day04/Solve.lean
@@ -13,8 +13,7 @@ private def countXmasOccurrencesInRow : List Char -> Int
 
 #guard countXmasOccurrencesInRow "ABXMASXMASXMA".toList == 2
 
-private def countXmasOccurrencesInRows (grid : Grid): Int :=
-  grid.sumBy countXmasOccurrencesInRow
+private def countXmasOccurrencesInRows (grid : Grid): Int := grid.sumBy countXmasOccurrencesInRow
 
 private def gridToString (g : Grid) : String := g.map List.asString |> String.intercalate "\n"
 
@@ -22,34 +21,11 @@ private def gridToString (g : Grid) : String := g.map List.asString |> String.in
 
 private def flipHorizontal (grid : Grid) : Grid := grid.map (·.reverse)
 
--- ported from https://hackage.haskell.org/package/universe-base-1.1.4/docs/src/Data.Universe.Helpers.html#diagonals
-private def diagonals (grid : List (List α)) : List (List α) :=
-  let rec go (b : List (List α)) (es : List (List α)) : List (List α) :=
-    let diagonal := b.filterMap List.head?
-    let ts := b.filterMap List.tail?
-    diagonal :: match es with
-      | [] => ts.transpose
-      | e :: es' => go (e :: ts) es'
-  (go [] grid).tail!
-
-#guard diagonals [
-  ["A", "B", "C", "D"],
-  ["E", "F", "G", "H"],
-  ["I", "J", "K", "L"],
-] == [
-  ["A"],
-  ["E", "B"],
-  ["I", "F", "C"],
-  ["J", "G", "D"],
-  ["K", "H"],
-  ["L"],
-]
-
 private def allGridTransformations : List (Grid -> Grid) := [
   id,
   List.transpose,
-  diagonals,
-  diagonals ∘ flipHorizontal,
+  List.diagonals,
+  List.diagonals ∘ flipHorizontal,
 ]
 
 private def transformGridInAllWays (grid : Grid) : List Grid := allGridTransformations.map (· grid)
diff --git a/Aoc2024/Utils.lean b/Aoc2024/Utils.lean
index 50b9370..97a5a32 100644
--- a/Aoc2024/Utils.lean
+++ b/Aoc2024/Utils.lean
@@ -1,4 +1,5 @@
 import Std
+import Batteries
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec
 open Std (HashSet)
@@ -49,14 +50,23 @@ namespace List
 
   def sum (xs: List Int) : Int := xs.foldl .add 0
 
+  #guard [].sum = 0
+  #guard [1, 2, 3].sum = 6
+
   def sumBy (f : α → Int) (xs : List α) : Int := xs.foldl (λ acc x => acc + f x) 0
 
+  #guard [1, 2, 3].sumBy (λ x => x * x) = 14
+
   def toSet {α:Type} [BEq α] [Hashable α] (xs: List α) : HashSet α :=
     HashSet.ofList xs
 
   def differences (xs: List Int) : List Int :=
     xs.zip xs.tail |>.map (λ (a, b) => b - a)
 
+  #guard [].differences == []
+  #guard [1].differences == []
+  #guard [1, 2, 3, 2, 5].differences == [1, 1, -1, 3]
+
   def slidingWindows (n : Nat) (xs : List α) : List (List α) :=
     match xs with
       | [] => []
@@ -65,23 +75,36 @@ namespace List
         if window.length < n then []
         else window :: slidingWindows n xs
 
+  #guard [1, 2, 3, 4, 5].slidingWindows 2 = [[1, 2], [2, 3], [3, 4], [4, 5]]
+  #guard [1, 2, 3, 4, 5].slidingWindows 1 = [[1], [2], [3], [4], [5]]
+  #guard [1, 2, 3, 4, 5].slidingWindows 0 = [[1], [2], [3], [4], [5]]
+  #guard [1].slidingWindows 2 = []
+  #guard ([]: List Nat).slidingWindows 2 = []
+
+  -- ported from https://hackage.haskell.org/package/universe-base-1.1.4/docs/src/Data.Universe.Helpers.html#diagonals
+  def diagonals (grid : List (List α)) : List (List α) :=
+    let rec go (b : List (List α)) (es : List (List α)) : List (List α) :=
+      let diagonal := b.filterMap List.head?
+      let ts := b.filterMap List.tail?
+      diagonal :: match es with
+        | [] => ts.transpose
+        | e :: es' => go (e :: ts) es'
+    (go [] grid).tail!
+
+  #guard [
+    ["A", "B", "C", "D"],
+    ["E", "F", "G", "H"],
+    ["I", "J", "K", "L"],
+  ].diagonals = [
+    ["A"],
+    ["E", "B"],
+    ["I", "F", "C"],
+    ["J", "G", "D"],
+    ["K", "H"],
+    ["L"],
+  ]
 end List
 
-#guard [].sum = 0
-#guard [1, 2, 3].sum = 6
-
-#guard [1, 2, 3].sumBy (λ x => x * x) = 14
-
-#guard [].differences == []
-#guard [1].differences == []
-#guard [1, 2, 3, 2, 5].differences == [1, 1, -1, 3]
-
-#guard [1, 2, 3, 4, 5].slidingWindows 2 = [[1, 2], [2, 3], [3, 4], [4, 5]]
-#guard [1, 2, 3, 4, 5].slidingWindows 1 = [[1], [2], [3], [4], [5]]
-#guard [1, 2, 3, 4, 5].slidingWindows 0 = [[1], [2], [3], [4], [5]]
-#guard [1].slidingWindows 2 = []
-#guard ([]: List Nat).slidingWindows 2 = []
-
 namespace Std.HashSet
 
   def isSubsetOf [Hashable α] [BEq α] (xs: HashSet α) (ys: HashSet α) : Bool :=