day 4 part 1

Aoc2024/Day04/Examples.lean

@@ -0,0 +1,18 @@
+def exampleInput1 :=
+"..X...
+.SAMX.
+.A..A.
+XMAS.S
+.X...."
+
+def exampleInput2 :=
+"MMMSXXMASM
+MSAMXMSMSA
+AMXSXMAAMM
+MSAMASMSMX
+XMASAMXAMM
+XXAMMXXAMA
+SMSMSASXSS
+SAXAMASAAA
+MAMMMXMMMM
+MXMXAXMASX"

Aoc2024/Day04/Main.lean

@@ -0,0 +1,15 @@
+import Aoc2024.Day04.Solve
+import Aoc2024.CustomMonadLift
+
+def main : IO Unit := do
+  IO.println "Day 04"
+  IO.println ""
+  IO.println "Part 1"
+  let exampleInput <- IO.FS.readFile "Aoc2024/Day04/inputs/example.txt"
+  let puzzleInput <- IO.FS.readFile "Aoc2024/Day04/inputs/input.txt"
+  IO.println s!"Example: {solvePart1 exampleInput}"
+  IO.println s!"Puzzle: {solvePart1 puzzleInput}" --
+  IO.println ""
+  IO.println "Part 2"
+  IO.println s!"Example: {solvePart2 exampleInput}"
+  IO.println s!"Puzzle: {solvePart2 puzzleInput}" --

Aoc2024/Day04/Parser.lean

@@ -0,0 +1,8 @@
+import Aoc2024.Day04.Examples
+import Aoc2024.Day04.Types
+import Aoc2024.Utils
+import Std
+
+def parseGrid (s : String) : Grid := s.lines.map (·.toList)
+
+-- #guard parseReports exampleInput == Except.ok 42

Aoc2024/Day04/Solve.lean

@@ -0,0 +1,76 @@
+import Aoc2024.Utils
+import Aoc2024.Day04.Examples
+import Aoc2024.Day04.Parser
+import Batteries
+
+private def countXmasOccurrencesInRow : List Char -> Int
+  | [] => 0
+  | 'X' :: 'M' :: 'A' :: 'S' :: rest => 1 + countXmasOccurrencesInRow rest
+  | _ :: rest => countXmasOccurrencesInRow rest
+
+#guard countXmasOccurrencesInRow "ABXMASXMASXMA".toList == 2
+
+private def countXmasOccurrencesInRows (grid : Grid): Int :=
+  grid.sumBy countXmasOccurrencesInRow
+
+private def gridToString (g : Grid) : String := g.map List.asString |> String.intercalate "\n"
+
+#guard gridToString [['A', 'B', 'C'], ['D', 'E', 'F']] = "ABC\nDEF"
+
+private def flipHorizontal (grid : Grid) : Grid := grid.map (·.reverse)
+
+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,
+  flipHorizontal,
+  List.transpose,
+  flipHorizontal ∘ List.transpose,
+  diagonals,
+  diagonals ∘ List.transpose,
+  diagonals ∘ flipHorizontal,
+  diagonals ∘ List.transpose ∘ flipHorizontal,
+]
+
+-- def g := parseGrid exampleInput1
+-- #eval g |> id
+-- #eval g |> flipHorizontal
+-- #eval g |> List.transpose
+-- #eval g |> List.transpose |> flipHorizontal
+-- #eval g |> diagonals
+-- #eval g |> List.transpose |> diagonals
+-- #eval g |> flipHorizontal |> diagonals
+-- #eval g |> flipHorizontal |> List.transpose |> diagonals
+
+def solvePart1 (s : String): Int :=
+  let grid := parseGrid s
+  allGridTransformations.sumBy (λ transformation => transformation grid |> countXmasOccurrencesInRows)
+
+#guard solvePart1 exampleInput1 = 4
+#guard solvePart1 exampleInput2 = 18
+
+def solvePart2 (things : s) : Int := sorry
+
+-- def parseAndSolvePart2 (s : String): Except String Int := parseGrid s |>.map solvePart2
+
+-- #guard parseAndSolvePart2 exampleInput == Except.ok 4

Aoc2024/Day04/Types.lean

@@ -0,0 +1 @@
+abbrev Grid := List (List Char)

Aoc2024/Day04/inputs/example.txt

@@ -0,0 +1,10 @@
+MMMSXXMASM
+MSAMXMSMSA
+AMXSXMAAMM
+MSAMASMSMX
+XMASAMXAMM
+XXAMMXXAMA
+SMSMSASXSS
+SAXAMASAAA
+MAMMMXMMMM
+MXMXAXMASX

Aoc2024/Utils.lean

@@ -77,3 +77,9 @@ end Std.HashSet
 
 #guard [1, 3].toSet.isSubsetOf [1, 2, 3].toSet == true
 #guard [1, 2, 3].toSet.isSubsetOf [1, 3].toSet == false
+
+namespace String
+  def lines (s : String) : List String := s.splitOn "\n"
+end String
+
+#guard "1\n2\n3".lines == ["1", "2", "3"]

DayXX/Main.lean

@@ -0,0 +1,15 @@
+import Aoc2024.DayXX.Solve
+import Aoc2024.CustomMonadLift
+
+def main : IO Unit := do
+  IO.println "Day XX"
+  IO.println ""
+  IO.println "Part 1"
+  let exampleInput <- IO.FS.readFile "Aoc2024/DayXX/inputs/example.txt"
+  let puzzleInput <- IO.FS.readFile "Aoc2024/DayXX/inputs/input.txt"
+  IO.println s!"Example: {parseAndSolvePart1 exampleInput}"
+  IO.println s!"Puzzle: {parseAndSolvePart1 puzzleInput}" --
+  IO.println ""
+  IO.println "Part 2"
+  IO.println s!"Example: {parseAndSolvePart2 exampleInput}"
+  IO.println s!"Puzzle: {parseAndSolvePart2 puzzleInput}" --

Aoc2024/DayXX/Parser.lean → DayXX/Parser.lean

@@ -1,4 +1,6 @@
 import Aoc2024.DayXX.Examples
+import Aoc2024.DayXX.Types
+import Aoc2024.Utils
 import Std
 open Std.Internal.Parsec.String
 open Std.Internal.Parsec

Taskfile.yml

@@ -25,4 +25,10 @@ tasks:
     deps: [build]
     cmds: 
       - .lake/build/bin/day3
+  day4:
+    desc: Run day 4
+    deps: [build]
+    cmds: 
+      - .lake/build/bin/day4
+
 

lakefile.toml

@@ -1,6 +1,6 @@
 name = "aoc2024"
 version = "0.1.0"
-defaultTargets = ["day1", "day2", "day3", "dayXX"]
+defaultTargets = ["day1", "day2", "day3", "day4"]
 
 [[lean_lib]]
 name = "Aoc2024"
@@ -18,8 +18,12 @@ name = "day3"
 root = "Aoc2024.Day03.Main"
 
 [[lean_exe]]
-name = "dayXX"
-root = "Aoc2024.DayXX.Main"
+name = "day4"
+root = "Aoc2024.Day04.Main"
+
+#[[lean_exe]]
+#name = "dayXX"
+#root = "Aoc2024.DayXX.Main"
 
 [[require]]
 name = "Regex"