wip

Aoc2024/Day06/Examples.lean

@@ -0,0 +1,11 @@
+def exampleInput :=
+"....#.....
+.........#
+..........
+..#.......
+.......#..
+..........
+.#..^.....
+........#.
+#.........
+......#..."

Aoc2024/Day06/Main.lean

@@ -0,0 +1,19 @@
+import Aoc2024.Day06.Solve
+import Aoc2024.CustomMonadLift
+
+def main : IO Unit := do
+  IO.println "Day 06"
+  IO.println ""
+  IO.println "Part 1"
+  let exampleInput <- IO.FS.readFile "Aoc2024/Day06/inputs/example.txt"
+  let puzzleInput <- IO.FS.readFile "Aoc2024/Day06/inputs/input.txt"
+  IO.println s!"Example: {<- parseAndSolvePart1 exampleInput}"
+  let answerPart1 <- parseAndSolvePart1 puzzleInput
+  IO.println s!"Puzzle: {answerPart1}"
+  assert! (answerPart1 == -1)
+  IO.println ""
+  IO.println "Part 2"
+  IO.println s!"Example: {<- parseAndSolvePart2 exampleInput}"
+  let answerPart2 <- parseAndSolvePart2 puzzleInput
+  IO.println s!"Puzzle: {answerPart2}"
+  assert! (answerPart2 == -1)

Aoc2024/Day06/Parser.lean

@@ -0,0 +1,25 @@
+import Aoc2024.Day06.Examples
+import Aoc2024.Day06.Types
+import Aoc2024.Utils
+import Std
+open Std.Internal.Parsec.String
+open Std.Internal.Parsec
+open Std (HashSet)
+
+-- private def inputParser : Parser (List Int) := sorry
+
+private def decorateWithCoordinates (s: String): List (Point × Char) :=
+  s.splitOn "\n" |>.enum |>.bind (λ ⟨y, line⟩ =>
+    line.toList.enum.map (λ ⟨x, c⟩ => (⟨x, y⟩, c))
+  )
+
+def parseInput (s: String): Except String PuzzleInput := do
+  let decoratedChars := decorateWithCoordinates s
+  let obstacles := decoratedChars.filterMap (λ ⟨p, c⟩ => (c == '#').toOption p) |>.toSet
+  let start <- decoratedChars.filterMap (λ ⟨p, c⟩ => (c == '^').toOption p) |>.head? |>.getOrThrow "no start found"
+  let (xs, ys) := decoratedChars.map (·.1.toPair) |>.unzip
+  let width <- xs.toArray.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input"
+  let height <- ys.toArray.max?.map (· + 1 |>.toNat) |>.getOrThrow "empty input"
+  pure { obstacles, start, width, height }
+
+-- #guard parseReports exampleInput == Except.ok 42

Aoc2024/Day06/Solve.lean

@@ -0,0 +1,15 @@
+import Aoc2024.Utils
+import Aoc2024.Day06.Examples
+import Aoc2024.Day06.Parser
+
+private def solvePart1 (input : PuzzleInput) : Int := sorry
+
+def parseAndSolvePart1 (s : String): Except String Int := parseInput s |>.map solvePart1
+
+-- #guard parseAndSolvePart1 exampleInput == Except.ok 41
+
+private def solvePart2 (input : PuzzleInput) : Int := sorry
+
+def parseAndSolvePart2 (s : String): Except String Int := parseInput s |>.map solvePart2
+
+-- #guard parseAndSolvePart2 exampleInput == Except.ok -1

Aoc2024/Day06/Types.lean

@@ -0,0 +1,22 @@
+import Std
+open Std (HashSet)
+
+structure Point where
+  x : Int
+  y : Int
+deriving BEq, Hashable, Repr
+
+def Point.toPair (p : Point) : (Int × Int) := (p.x, p.y)
+
+inductive Direction where
+  | Up
+  | Right
+  | Down
+  | Left
+
+structure PuzzleInput where
+  obstacles : HashSet Point
+  width : Nat
+  height : Nat
+  start : Point
+deriving Repr

Aoc2024/Day06/inputs/example.txt

@@ -0,0 +1,10 @@
+....#.....
+.........#
+..........
+..#.......
+.......#..
+..........
+.#..^.....
+........#.
+#.........
+......#...

Aoc2024/Utils.lean

@@ -148,3 +148,18 @@ def iterate (n : Nat) (f : α -> α) (x : α) : α :=
   match n with
   | 0 => x
   | n + 1 => iterate n f (f x)
+
+namespace Bool
+  def toOption (x : Bool) (y : α) : Option α := if x then some y else none
+
+  #guard true.toOption 42 == some 42
+  #guard false.toOption 42 == none
+end Bool
+
+namespace Option
+  def getOrThrow (message : String) : Option α -> Except String α
+    | some x => pure x
+    | none => throw message
+  #guard (some 42).getOrThrow "Error" == Except.ok 42
+  #guard (none : Option Int).getOrThrow "Error" == Except.error "Error"
+end Option

DayXX/Solve.lean

@@ -6,10 +6,10 @@ private def solvePart1 (things : List Int) : Int := sorry
 
 def parseAndSolvePart1 (s : String): Except String Int := parseThings s |>.map solvePart1
 
--- #guard parseAndSolvePart1 exampleInput == Except.ok 2
+-- #guard parseAndSolvePart1 exampleInput == Except.ok -1
 
 private def solvePart2 (things : List Int) : Int := sorry
 
 def parseAndSolvePart2 (s : String): Except String Int := parseThings s |>.map solvePart2
 
--- #guard parseAndSolvePart2 exampleInput == Except.ok 4
+-- #guard parseAndSolvePart2 exampleInput == Except.ok -1

Taskfile.yml

@@ -35,5 +35,8 @@ tasks:
     deps: [build]
     cmds: 
       - .lake/build/bin/day5
-
-
+  day6:
+    desc: Run day 6
+    deps: [build]
+    cmds: 
+      - .lake/build/bin/day6

lakefile.toml

@@ -1,6 +1,6 @@
 name = "aoc2024"
 version = "0.1.0"
-defaultTargets = ["day1", "day2", "day3", "day4", "day5"]
+defaultTargets = ["day1", "day2", "day3", "day4", "day5", "day6"]
 
 [[lean_lib]]
 name = "Aoc2024"
@@ -25,6 +25,10 @@ root = "Aoc2024.Day04.Main"
 name = "day5"
 root = "Aoc2024.Day05.Main"
 
+[[lean_exe]]
+name = "day6"
+root = "Aoc2024.Day06.Main"
+
 [[require]]
 name = "Regex"
 git = "https://github.com/bergmannjg/regex"